let n be Nat; :: thesis: ( 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; :: thesis: ( 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 ) ; :: thesis: not 9 divides n
given t being Nat such that A3: n = 9 * t ; :: according to NAT_D:def 3 :: thesis: 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;

suppose n = (9 * k) + 1 ; :: thesis: contradiction

then 1 / 9 = t - k by A3;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose n = (9 * k) + 2 ; :: thesis: contradiction

then 2 / 9 = t - k by A3;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose n = (9 * k) + 3 ; :: thesis: contradiction

then 3 / 9 = t - k by A3;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose n = (9 * k) + 4 ; :: thesis: contradiction

then 4 / 9 = t - k by A3;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose n = (9 * k) + 5 ; :: thesis: contradiction

then 5 / 9 = t - k by A3;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose n = (9 * k) + 6 ; :: thesis: contradiction

then 6 / 9 = t - k by A3;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose n = (9 * k) + 7 ; :: thesis: contradiction

then 7 / 9 = t - k by A3;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose n = (9 * k) + 8 ; :: thesis: contradiction

then 8 / 9 = t - k by A3;
hence contradiction by NAT_D:33; :: thesis: verum

end;

end;