let n be Nat; :: thesis: ( not 5 divides n iff ex k being Nat st

( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) )

consider K being Nat such that

A1: ( n = 5 * K or n = (5 * K) + 1 or n = (5 * K) + 2 or n = (5 * K) + 3 or n = (5 * K) + 4 ) by Th25;

thus ( not 5 divides n implies ex k being Nat st

( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) ) by A1; :: thesis: ( ex k being Nat st

( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) implies not 5 divides n )

given k being Nat such that A2: ( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) ; :: thesis: not 5 divides n

given t being Nat such that A3: n = 5 * t ; :: according to NAT_D:def 3 :: thesis: contradiction

( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) )

consider K being Nat such that

A1: ( n = 5 * K or n = (5 * K) + 1 or n = (5 * K) + 2 or n = (5 * K) + 3 or n = (5 * K) + 4 ) by Th25;

thus ( not 5 divides n implies ex k being Nat st

( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) ) by A1; :: thesis: ( ex k being Nat st

( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) implies not 5 divides n )

given k being Nat such that A2: ( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) ; :: thesis: not 5 divides n

given t being Nat such that A3: n = 5 * t ; :: according to NAT_D:def 3 :: thesis: contradiction

per cases
( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 )
by A2;

end;