set A = { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 } ;
set B = { ((6 * k) + 1) where k is Nat : verum } ;
set C = { ((6 * k) + 2) where k is Nat : verum } ;
2 |^ 6 = ((((2 * 2) * 2) * 2) * 2) * 2 by NUMBER02:2;
then A1: (2 |^ 6) mod 3 = ((3 * 21) + 1) mod 3
.= 1 mod 3 by NAT_D:21 ;
thus { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 } c= { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } :: according to XBOOLE_0:def 10 :: thesis: { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } c= { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 } or x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } )
assume x in { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 } ; :: thesis: x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum }
then consider n being positive Nat such that
A2: x = n and
A3: 3 divides (n * (2 |^ n)) + 1 ;
A4: ((n * (2 |^ n)) + 1) mod 3 = (((n * (2 |^ n)) mod 3) + (1 mod 3)) mod 3 by NAT_D:66;
A5: (n * (2 |^ n)) mod 3 = ((n mod 3) * ((2 |^ n) mod 3)) mod 3 by NAT_D:67;
A6: n mod 3 <> 0 by Lm1, A5, A4, A3, INT_1:62;
consider k being Nat such that
A7: ( n = 6 * k or n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) by NUMBER02:26;
A8: ((2 |^ 6) |^ k) mod 3 = (1 |^ k) mod 3 by Lm1, A1, PEPIN:12
.= 1 by NAT_D:24 ;

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

suppose n = 3 * (2 * k) ; :: thesis: x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum }

hence x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } by A6, NAT_D:13; :: thesis: verum

end;

suppose n = (6 * k) + 1 ; :: thesis: x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum }

then n in { ((6 * k) + 1) where k is Nat : verum } ;
hence x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } by A2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose n = (6 * k) + 2 ; :: thesis: x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum }

then n in { ((6 * k) + 2) where k is Nat : verum } ;
hence x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } by A2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose n = 3 * ((2 * k) + 1) ; :: thesis: x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum }

hence x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } by A6, NAT_D:13; :: thesis: verum

end;

suppose A9: n = (6 * k) + 4 ; :: thesis: x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum }

then A10: n mod 3 = ((3 * ((2 * k) + 1)) + 1) mod 3
.= 1 mod 3 by NAT_D:21 ;
2 |^ (((6 * k) + 3) + 1) = (2 |^ (((6 * k) + 2) + 1)) * 2 by NEWTON:6
.= ((2 |^ (((6 * k) + 1) + 1)) * 2) * 2 by NEWTON:6
.= (((2 |^ ((6 * k) + 1)) * 2) * 2) * 2 by NEWTON:6
.= ((((2 |^ (6 * k)) * 2) * 2) * 2) * 2 by NEWTON:6
.= (2 |^ (6 * k)) * (((2 * 2) * 2) * 2)
.= ((2 |^ 6) |^ k) * 16 by NEWTON:9 ;
then A11: (2 |^ n) mod 3 = (1 * 1) mod 3 by A8, Lm4, A9, NAT_D:67;
((n * (2 |^ n)) + 1) mod 3 = (((n * (2 |^ n)) mod 3) + (1 mod 3)) mod 3 by NAT_D:66
.= (1 + 1) mod 3 by A11, Lm1, A10, NAT_D:67
.= 2 by NAT_D:24 ;
hence x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } by A3, INT_1:62; :: thesis: verum

end;

suppose A12: n = (6 * k) + 5 ; :: thesis: x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum }

then A13: n mod 3 = ((3 * ((2 * k) + 1)) + 2) mod 3
.= 2 mod 3 by NAT_D:21 ;
2 |^ (((6 * k) + 4) + 1) = (2 |^ (((6 * k) + 3) + 1)) * 2 by NEWTON:6
.= ((2 |^ (((6 * k) + 2) + 1)) * 2) * 2 by NEWTON:6
.= (((2 |^ (((6 * k) + 1) + 1)) * 2) * 2) * 2 by NEWTON:6
.= ((((2 |^ ((6 * k) + 1)) * 2) * 2) * 2) * 2 by NEWTON:6
.= (((((2 |^ (6 * k)) * 2) * 2) * 2) * 2) * 2 by NEWTON:6
.= (2 |^ (6 * k)) * ((((2 * 2) * 2) * 2) * 2)
.= ((2 |^ 6) |^ k) * 32 by NEWTON:9 ;
then A14: (2 |^ n) mod 3 = ((((2 |^ 6) |^ k) mod 3) * (32 mod 3)) mod 3 by A12, NAT_D:67
.= (1 * 2) mod 3 by A8, Lm5 ;
((n * (2 |^ n)) + 1) mod 3 = (((n * (2 |^ n)) mod 3) + 1) mod 3 by Lm1, NAT_D:66
.= (((2 * 2) mod 3) + 1) mod 3 by Lm2, A14, A13, NAT_D:67
.= 2 by Lm1, Lm3, NAT_D:24 ;
hence x in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } by A3, INT_1:62; :: thesis: verum

end;

end;

end;

let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } or n in { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 } )
assume n in { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum } ; :: thesis: n in { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 }

per cases then ( n in { ((6 * k) + 1) where k is Nat : verum } or n in { ((6 * k) + 2) where k is Nat : verum } ) by XBOOLE_0:def 3;

suppose n in { ((6 * k) + 1) where k is Nat : verum } ; :: thesis: n in { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 }

then consider k being Nat such that
A15: n = (6 * k) + 1 ;
reconsider n = n as Nat by A15;
A16: ((2 |^ 6) |^ k) mod 3 = (1 |^ k) mod 3 by Lm1, A1, PEPIN:12
.= 1 by NAT_D:24 ;
A17: n mod 3 = ((3 * (2 * k)) + 1) mod 3 by A15
.= 1 mod 3 by NAT_D:21 ;
2 |^ ((6 * k) + 1) = (2 |^ (6 * k)) * 2 by NEWTON:6
.= ((2 |^ 6) |^ k) * 2 by NEWTON:9 ;
then A18: (2 |^ n) mod 3 = ((((2 |^ 6) |^ k) mod 3) * (2 mod 3)) mod 3 by A15, NAT_D:67
.= (1 * 2) mod 3 by A16 ;
((n * (2 |^ n)) + 1) mod 3 = (((n * (2 |^ n)) mod 3) + 1) mod 3 by Lm1, NAT_D:66
.= (2 + 1) mod 3 by Lm2, A18, Lm1, A17, NAT_D:67
.= 0 by INT_1:50 ;
then 3 divides (n * (2 |^ n)) + 1 by INT_1:62;
hence n in { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 } by A15; :: thesis: verum

end;

suppose n in { ((6 * k) + 2) where k is Nat : verum } ; :: thesis: n in { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 }

then consider k being Nat such that
A19: n = (6 * k) + 2 ;
reconsider n = n as Nat by A19;
A20: ((2 |^ 6) |^ k) mod 3 = (1 |^ k) mod 3 by Lm1, A1, PEPIN:12
.= 1 by NAT_D:24 ;
A21: n mod 3 = ((3 * (2 * k)) + 2) mod 3 by A19
.= 2 mod 3 by NAT_D:21 ;
2 |^ (((6 * k) + 1) + 1) = (2 |^ ((6 * k) + 1)) * 2 by NEWTON:6
.= ((2 |^ (6 * k)) * 2) * 2 by NEWTON:6
.= (2 |^ (6 * k)) * (2 * 2)
.= ((2 |^ 6) |^ k) * 4 by NEWTON:9 ;
then A22: (2 |^ n) mod 3 = (1 * 1) mod 3 by Lm3, A20, A19, NAT_D:67;
((n * (2 |^ n)) + 1) mod 3 = (((n * (2 |^ n)) mod 3) + 1) mod 3 by Lm1, NAT_D:66
.= ((((n mod 3) * ((2 |^ n) mod 3)) mod 3) + 1) mod 3 by NAT_D:67
.= 0 by Lm2, Lm1, A22, A21, INT_1:50 ;
then 3 divides (n * (2 |^ n)) + 1 by INT_1:62;
hence n in { n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 } by A19; :: thesis: verum

end;

end;