for n being Nat holds
( not n divides 3 or n = 1 or n = 3 )
proof
let n be Nat; :: thesis: ( not n divides 3 or n = 1 or n = 3 )
assume A1: n divides 3 ; :: thesis: ( n = 1 or n = 3 )
A2: n <> 2
proof
A3: 3 mod 2 = ((2 * 1) + 1) mod 2
.= 1 mod 2 by NAT_D:21
.= 1 by NAT_D:24 ;
assume n = 2 ; :: thesis: contradiction
hence contradiction by A1, A3, Th6; :: thesis: verum
end;
n <= 3 by A1, NAT_D:7;
then ( n < 2 + 1 or n = 3 ) by XXREAL_0:1;
then ( n <= 2 or n = 3 ) by NAT_1:13;
then ( n < 1 + 1 or n = 2 or n = 3 ) by XXREAL_0:1;
then ( n <= 1 or n = 2 or n = 3 ) by NAT_1:13;
then A4: ( n < 1 or n = 1 or n = 2 or n = 3 ) by XXREAL_0:1;
n <> 0 by A1;
hence ( n = 1 or n = 3 ) by A4, A2, NAT_1:14; :: thesis: verum
end;
hence 3 is prime by INT_2:def 4; :: thesis: verum