let k be Nat; :: thesis: ( k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 & k, - 1 are_congruent_mod 6700417 & k > 6700417 implies for n being positive Nat holds
( k + (2 |^ n) is composite & ( not not Fermat 0 divides k + (2 |^ n) & ... & not Fermat 4 divides k + (2 |^ n) or 641 divides k + (2 |^ n) or 6700417 divides k + (2 |^ n) ) ) )
assume that
A1: k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 and
A2: k, - 1 are_congruent_mod 6700417 and
A3: k > 6700417 ; :: thesis: for n being positive Nat holds
( k + (2 |^ n) is composite & ( not not Fermat 0 divides k + (2 |^ n) & ... & not Fermat 4 divides k + (2 |^ n) or 641 divides k + (2 |^ n) or 6700417 divides k + (2 |^ n) ) )
set Q = (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5);
let n be positive Nat; :: thesis: ( k + (2 |^ n) is composite & ( not not Fermat 0 divides k + (2 |^ n) & ... & not Fermat 4 divides k + (2 |^ n) or 641 divides k + (2 |^ n) or 6700417 divides k + (2 |^ n) ) )
A4: 2,(((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) are_coprime

proof

consider k being Nat such that
A5: (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = (2 * k) + 1 by ABIAN:9;
1,2 are_coprime ;
hence 2,(((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) are_coprime by A5, NUMBER04:64; :: thesis: verum

end;

( 2 < Fermat 5 & 1 <= ((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4) ) by NAT_1:14, Th28;
then ( 1 + 1 = 1 * 2 & 1 * 2 <= (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) ) by XREAL_1:66;
then A6: (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) > 1 by NAT_1:13;
set e = n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1);
Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) > 1

proof

(((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = (Fermat 0) * (((((Fermat 1) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) ;
then Fermat 0 divides (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) ;
then ( 3 - 1 = Euler (3 |^ 1) & Euler (3 |^ 1) <= Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) ) by Th34, PEPIN:41, PEPIN:50, EULER_1:20;
hence Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) > 1 by XXREAL_0:2; :: thesis: verum

end;

then A7: ( (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1 = (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) - 1 & (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) - 1 > 1 - 1 ) by XREAL_1:14, XREAL_1:233;
then ( ( (k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1 is composite & not not Fermat 0 divides (k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1 & ... & not Fermat 4 divides (k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1 ) or 641 divides (k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1 or 6700417 divides (k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1 ) by A1, A2, A3, Th30;
then consider q being Nat such that
A8: q divides (k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1 and
A9: ( q = Fermat 0 or q = Fermat 1 or q = Fermat 2 or q = Fermat 3 or q = Fermat 4 or q = 641 or q = 6700417 ) ;
A10: (k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1, 0 are_congruent_mod q by A8;
2 |^ n,2 |^ n are_congruent_mod q by INT_1:11;
then A11: ((k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1) * (2 |^ n),0 * (2 |^ n) are_congruent_mod q by A10, INT_1:18;
A12: ((k * (2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)))) + 1) * (2 |^ n) = (k * ((2 |^ (n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1))) * (2 |^ n))) + (2 |^ n)
.= (k * (2 |^ ((n * ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) -' 1)) + n))) + (2 |^ n) by NEWTON:8
.= (k * (2 |^ (n * (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)))))) + (2 |^ n) by A7 ;
A13: k,k are_congruent_mod q by INT_1:11;
A14: ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 )

proof

A15: Fermat 5 = 641 * 6700417 by Th28;
( (2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)))) mod ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) = 1 & 1 = 1 mod ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) ) by A6, A4, EULER_2:18, NAT_D:14;
then A16: 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) by NAT_D:64;

per cases ( q = Fermat 0 or q = Fermat 1 or q = Fermat 2 or q = Fermat 3 or q = Fermat 4 or q = 641 or q = 6700417 ) by A9;

suppose A17: q = Fermat 0 ; :: thesis: ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 )

then (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = q * (((((Fermat 1) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) ;
hence ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 ) by A17, A3, A16, INT_1:20, PEPIN:50, XXREAL_0:2; :: thesis: verum

end;

suppose A18: q = Fermat 1 ; :: thesis: ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 )

then (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = q * (((((Fermat 0) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) ;
hence ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 ) by A16, INT_1:20, A18, A3, PEPIN:51, XXREAL_0:2; :: thesis: verum

end;

suppose A19: q = Fermat 2 ; :: thesis: ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 )

then (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = q * (((((Fermat 0) * (Fermat 1)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)) ;
hence ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 ) by A16, INT_1:20, A19, A3, PEPIN:52, XXREAL_0:2; :: thesis: verum

end;

suppose A20: q = Fermat 3 ; :: thesis: ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 )

then (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = q * (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 4)) * (Fermat 5)) ;
hence ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 ) by A20, A3, A16, INT_1:20, PEPIN:53, XXREAL_0:2; :: thesis: verum

end;

suppose A21: q = Fermat 4 ; :: thesis: ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 )

then (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = q * (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 5)) ;
hence ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 ) by A21, A3, A16, INT_1:20, PEPIN:54, XXREAL_0:2; :: thesis: verum

end;

suppose A22: q = 641 ; :: thesis: ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 )

then (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = q * (((((6700417 * (Fermat 0)) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) by A15;
hence ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 ) by A22, A3, A16, INT_1:20, XXREAL_0:2; :: thesis: verum

end;

suppose A23: q = 6700417 ; :: thesis: ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 )

then (((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5) = q * (((((641 * (Fermat 0)) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) by A15;
hence ( 2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))),1 are_congruent_mod q & k > q & q > 1 ) by A16, INT_1:20, A23, A3; :: thesis: verum

end;

end;

end;

then (2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)))) |^ n,1 |^ n are_congruent_mod q by GR_CY_3:34;
then k * ((2 |^ (Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5)))) |^ n),k * 1 are_congruent_mod q by A13, INT_1:18;
then k * (2 |^ ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) * n)),k are_congruent_mod q by NEWTON:9;
then A24: (k * (2 |^ ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) * n))) + (2 |^ n),k + (2 |^ n) are_congruent_mod q ;
0 ,(k * (2 |^ ((Euler ((((((Fermat 0) * (Fermat 1)) * (Fermat 2)) * (Fermat 3)) * (Fermat 4)) * (Fermat 5))) * n))) + (2 |^ n) are_congruent_mod q by A11, A12, INT_1:14;
then 0 ,k + (2 |^ n) are_congruent_mod q by A24, INT_1:15;
then A25: k + (2 |^ n), 0 are_congruent_mod q by INT_1:14;
q + 0 < k + (2 |^ n) by A14, XREAL_1:8;
then A26: ( not k + (2 |^ n) is prime & k + (2 |^ n) > 1 ) by A14, A25, XXREAL_0:2;
then k + (2 |^ n) >= 1 + 1 by NAT_1:13;
hence ( k + (2 |^ n) is composite & ( not not Fermat 0 divides k + (2 |^ n) & ... & not Fermat 4 divides k + (2 |^ n) or 641 divides k + (2 |^ n) or 6700417 divides k + (2 |^ n) ) ) by A25, A9, A26, NUMBER02:def 1; :: thesis: verum