not 3 divides 5
proof
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;
hence not 5 / 3 is integer by WSIERP_1:17; :: thesis: verum