not 3 divides 5

proof

hence
not 5 / 3 is integer
by WSIERP_1:17; :: thesis: verum
assume
3 divides 5
; :: thesis: contradiction

then A1: 5 mod 3 = 0 by PEPIN:6;

5 = (3 * 1) + 2 ;

hence contradiction by A1, NAT_D:def 2; :: thesis: verum

end;then A1: 5 mod 3 = 0 by PEPIN:6;

5 = (3 * 1) + 2 ;

hence contradiction by A1, NAT_D:def 2; :: thesis: verum