let k be Nat; :: thesis:
assume A1: k = (((15 * 1000000000) * 1000000000) + (511380746 * 1000000000)) + 462593381 ; :: thesis:
thus k > 6700417 by A1; :: thesis:
k - 1 = 5634204 * (((2 |^ 32) - 1) * 641) by A1, Th28;
hence A2: k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 ; :: thesis:
k + 1 = ((2314 * 1000000000) + 987372646) * 6700417 by A1;
hence A3: k, - 1 are_congruent_mod 6700417 ; :: thesis:
k - 1 = ((((7 * 1000000000) * 1000000000) + (755690373 * 1000000000)) + 231296690) * 2 by A1;
hence k,1 are_congruent_mod 2 ; :: thesis:
A4: 2 |^ (1 + 1) = (2 |^ 1) * 2 by NEWTON:6;
then 2 |^ (2 + 1) = 4 * 2 by NEWTON:6;
then A5: 2 |^ (2 + 3) = 4 * 8 by A4, NEWTON:8;
k - 1 = ((((5 * 1000000000) * 1000000000) + (170460248 * 1000000000)) + 820864460) * 3 by A1;
then A6: k,1 are_congruent_mod 3 ;
(3 * 0) + 2 = 2 ;
then A7: not 3 divides 2 by NAT_4:9;
(2 |^ 32) - 1 = 3 * 1431655765 by Th28;
then 2 |^ 32,1 are_congruent_mod 3 ;
then k * (2 |^ 32),1 * 1 are_congruent_mod 3 by A6, INT_1:18;
then A8: (k * (2 |^ 32)) + 1,1 + 1 are_congruent_mod 3 ;
k - 1 = ((((3 * 1000000000) * 1000000000) + (102276149 * 1000000000)) + 292518676) * 5 by A1;
then A9: k,1 are_congruent_mod 5 ;
(5 * 0) + 2 = 2 ;
then A10: not 5 divides 2 by NAT_4:9;
(2 |^ 32) - 1 = 5 * 858993459 by Th28;
then 2 |^ 32,1 are_congruent_mod 5 ;
then k * (2 |^ 32),1 * 1 are_congruent_mod 5 by A9, INT_1:18;
then A11: (k * (2 |^ 32)) + 1,1 + 1 are_congruent_mod 5 ;
k - 1 = ((912434161 * 1000000000) + 556623140) * 17 by A1;
then A12: k,1 are_congruent_mod 17 ;
(17 * 0) + 2 = 2 ;
then A13: not 17 divides 2 by NAT_4:9;
(2 |^ 32) - 1 = 17 * 252645135 by Th28;
then 2 |^ 32,1 are_congruent_mod 17 ;
then k * (2 |^ 32),1 * 1 are_congruent_mod 17 by A12, INT_1:18;
then A14: (k * (2 |^ 32)) + 1,1 + 1 are_congruent_mod 17 ;
k - 1 = ((60355567 * 1000000000) + 106858340) * 257 by A1;
then A15: k,1 are_congruent_mod 257 ;
(257 * 0) + 2 = 2 ;
then A16: not 257 divides 2 by NAT_4:9;
(2 |^ 32) - 1 = 257 * 16711935 by Th28;
then 2 |^ 32,1 are_congruent_mod 257 ;
then k * (2 |^ 32),1 * 1 are_congruent_mod 257 by A15, INT_1:18;
then A17: (k * (2 |^ 32)) + 1,1 + 1 are_congruent_mod 257 ;
k - 1 = ((236681 * 1000000000) + 275408740) * 65537 by A1;
then A18: k,1 are_congruent_mod 65537 ;
(65537 * 0) + 2 = 2 ;
then A19: not 65537 divides 2 by NAT_4:9;
(2 |^ 32) - 1 = 65537 * 65535 by Th28;
then 2 |^ 32,1 are_congruent_mod 65537 ;
then k * (2 |^ 32),1 * 1 are_congruent_mod 65537 by A18, INT_1:18;
then A20: (k * (2 |^ 32)) + 1,1 + 1 are_congruent_mod 65537 ;
thus not Fermat 0 divides (k * (2 |^ (2 |^ 5))) + 1 & ... & not Fermat 4 divides (k * (2 |^ (2 |^ 5))) + 1 by A8, A7, PEPIN:50, PEPIN:51, PEPIN:52, PEPIN:54, A11, A5, A10, A14, A13, A17, A16, NUMBER14:19, PEPIN:53, A20, A19; :: thesis:
(6700417 * 0) + 2 = 2 ;
then A21: not 6700417 divides 2 by NAT_4:9;
2 |^ 32, - 1 are_congruent_mod 6700417 by Th28;
then k * (2 |^ 32),(- 1) * (- 1) are_congruent_mod 6700417 by A3, INT_1:18;
then (k * (2 |^ 32)) + 1,2 are_congruent_mod 6700417 ;
hence not 6700417 divides (k * (2 |^ (2 |^ 5))) + 1 by A5, A21, NUMBER14:19; :: thesis:
A22: k,1 are_congruent_mod 641 by A2, INT_1:20;
2 |^ 32, - 1 are_congruent_mod 641 by Th28;
then k * (2 |^ 32),(- 1) * 1 are_congruent_mod 641 by A22, INT_1:18;
hence 641 divides (k * (2 |^ (2 |^ 5))) + 1 by A5; :: thesis: