let n be Nat; ( not 9 divides n iff ex k being Nat st
( n = (9 * k) + 1 or n = (9 * k) + 2 or n = (9 * k) + 3 or n = (9 * k) + 4 or n = (9 * k) + 5 or n = (9 * k) + 6 or n = (9 * k) + 7 or n = (9 * k) + 8 ) )
consider K being Nat such that
A1:
( n = 9 * K or n = (9 * K) + 1 or n = (9 * K) + 2 or n = (9 * K) + 3 or n = (9 * K) + 4 or n = (9 * K) + 5 or n = (9 * K) + 6 or n = (9 * K) + 7 or n = (9 * K) + 8 )
by Th29;
thus
( not 9 divides n implies ex k being Nat st
( n = (9 * k) + 1 or n = (9 * k) + 2 or n = (9 * k) + 3 or n = (9 * k) + 4 or n = (9 * k) + 5 or n = (9 * k) + 6 or n = (9 * k) + 7 or n = (9 * k) + 8 ) )
by A1; ( ex k being Nat st
( n = (9 * k) + 1 or n = (9 * k) + 2 or n = (9 * k) + 3 or n = (9 * k) + 4 or n = (9 * k) + 5 or n = (9 * k) + 6 or n = (9 * k) + 7 or n = (9 * k) + 8 ) implies not 9 divides n )
given k being Nat such that A2:
( n = (9 * k) + 1 or n = (9 * k) + 2 or n = (9 * k) + 3 or n = (9 * k) + 4 or n = (9 * k) + 5 or n = (9 * k) + 6 or n = (9 * k) + 7 or n = (9 * k) + 8 )
; not 9 divides n
given t being Nat such that A3:
n = 9 * t
; NAT_D:def 3 contradiction
per cases
( n = (9 * k) + 1 or n = (9 * k) + 2 or n = (9 * k) + 3 or n = (9 * k) + 4 or n = (9 * k) + 5 or n = (9 * k) + 6 or n = (9 * k) + 7 or n = (9 * k) + 8 )
by A2;
end;