set P = 6n+1_Primes ;
assume A1: 6n+1_Primes is finite ; :: thesis: contradiction
set N = 6 * (Product (Sgm 6n+1_Primes));
A2: Sgm 6n+1_Primes is positive-yielding
proof
let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in proj2 (Sgm 6n+1_Primes) or not r <= 0 )
assume A3: r in rng (Sgm 6n+1_Primes) ; :: thesis: not r <= 0
6n+1_Primes is included_in_Seg by A1;
then r in 6n+1_Primes by A3, FINSEQ_1:def 14;
hence not r <= 0 ; :: thesis: verum
end;
then A4: 6 * (Product (Sgm 6n+1_Primes)) >= 6 * 1 by Th2, XREAL_1:64;
A5: now :: thesis: not ((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes))) < 1
assume ((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes))) < 1 ; :: thesis: contradiction
then (6 * (Product (Sgm 6n+1_Primes))) * ((6 * (Product (Sgm 6n+1_Primes))) - 1) = 0 by A2, NAT_1:14;
then ( 6 * (Product (Sgm 6n+1_Primes)) = 0 or (6 * (Product (Sgm 6n+1_Primes))) - 1 = 0 ) ;
hence contradiction by A4; :: thesis: verum
end;
then reconsider M = (((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes)))) + 1 as Element of NAT by INT_1:3;
(((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes)))) + 1 >= 1 + 1 by A5, XREAL_1:6;
then consider p being Element of NAT such that
A6: p is prime and
A7: p divides M by INT_2:31;
reconsider p = p as Prime by A6;
A8: ((6 * (Product (Sgm 6n+1_Primes))) * (6 * (Product (Sgm 6n+1_Primes)))) * (6 * (Product (Sgm 6n+1_Primes))) = (6 * (Product (Sgm 6n+1_Primes))) |^ 3 by POLYEQ_5:2;
A9: ((6 * (Product (Sgm 6n+1_Primes))) |^ 3) * ((6 * (Product (Sgm 6n+1_Primes))) |^ 3) = (6 * (Product (Sgm 6n+1_Primes))) |^ (3 + 3) by NEWTON:8;
A10: p > 1 by INT_2:def 4;
A11: now :: thesis: not p divides 6 * (Product (Sgm 6n+1_Primes))
assume A12: p divides 6 * (Product (Sgm 6n+1_Primes)) ; :: thesis: contradiction
6 * (Product (Sgm 6n+1_Primes)) divides (6 * (Product (Sgm 6n+1_Primes))) ^2 ;
then p divides (6 * (Product (Sgm 6n+1_Primes))) ^2 by A12, INT_2:9;
then p divides ((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes))) by A12, INT_5:1;
then p divides M - (((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes)))) by A7, INT_5:1;
hence contradiction by INT_2:def 4, NAT_D:7; :: thesis: verum
end;
then A13: 6 * (Product (Sgm 6n+1_Primes)),p are_coprime by Th4;
then A14: ((6 * (Product (Sgm 6n+1_Primes))) |^ (order ((6 * (Product (Sgm 6n+1_Primes))),p))) mod p = 1 by A10, PEPIN:def 2;
A15: (- 1) mod p = p - 1 by Th5;
A16: p -' 1 = p - 1 by XREAL_0:def 2;
(((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes)))) + 1 divides ((((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes)))) + 1) * ((6 * (Product (Sgm 6n+1_Primes))) + 1) ;
then p divides ((((6 * (Product (Sgm 6n+1_Primes))) ^2) - (6 * (Product (Sgm 6n+1_Primes)))) + 1) * ((6 * (Product (Sgm 6n+1_Primes))) + 1) by A7, INT_2:9;
then p divides ((6 * (Product (Sgm 6n+1_Primes))) |^ 3) - (- 1) by A8;
then A17: (6 * (Product (Sgm 6n+1_Primes))) |^ 3, - 1 are_congruent_mod p ;
then A18: ((6 * (Product (Sgm 6n+1_Primes))) |^ 3) mod p = (- 1) mod p by NAT_D:64
.= p - 1 by Th5 ;
A19: 1 mod p = 1 by INT_2:def 4, NAT_D:24;
A20: now :: thesis: not 6 * (Product (Sgm 6n+1_Primes)),1 are_congruent_mod p
assume 6 * (Product (Sgm 6n+1_Primes)),1 are_congruent_mod p ; :: thesis: contradiction
then A21: ((6 * (Product (Sgm 6n+1_Primes))) |^ 3) mod p = 1 |^ 3 by A10, NAT_6:12, GR_CY_3:34;
6 * (Product (Sgm 6n+1_Primes)) = 2 * (3 * (Product (Sgm 6n+1_Primes))) ;
hence contradiction by A18, A21, NAT_2:21; :: thesis: verum
end;
A22: now :: thesis: ( not p = 2 & not p = 3 )
assume A23: ( p = 2 or p = 3 ) ; :: thesis: contradiction
( 2 divides 2 * (3 * (Product (Sgm 6n+1_Primes))) & 3 divides 3 * (2 * (Product (Sgm 6n+1_Primes))) ) ;
hence contradiction by A11, A23; :: thesis: verum
end;
((6 * (Product (Sgm 6n+1_Primes))) |^ 3) * ((6 * (Product (Sgm 6n+1_Primes))) |^ 3),(- 1) * (- 1) are_congruent_mod p by A17, INT_1:18;
then ((6 * (Product (Sgm 6n+1_Primes))) |^ 6) mod p = 1 by A9, INT_2:def 4, NAT_6:12;
then order ((6 * (Product (Sgm 6n+1_Primes))),p) divides 6 by A10, A11, Th4, PEPIN:47;
per cases then ( order ((6 * (Product (Sgm 6n+1_Primes))),p) = 1 or order ((6 * (Product (Sgm 6n+1_Primes))),p) = 2 or order ((6 * (Product (Sgm 6n+1_Primes))),p) = 3 or order ((6 * (Product (Sgm 6n+1_Primes))),p) = 6 ) by NUMBER07:10;
suppose order ((6 * (Product (Sgm 6n+1_Primes))),p) = 1 ; :: thesis: contradiction
hence contradiction by A14, A19, A20, NAT_D:64; :: thesis: verum
end;
suppose order ((6 * (Product (Sgm 6n+1_Primes))),p) = 2 ; :: thesis: contradiction
then 6 * (Product (Sgm 6n+1_Primes)), - 1 are_congruent_mod p by A14, A19, A20, NAT_D:64, NAT_6:18;
then A24: p divides ((6 * (Product (Sgm 6n+1_Primes))) + 1) gcd M by A7, INT_2:def 2;
M - 3 = ((6 * (Product (Sgm 6n+1_Primes))) + 1) * ((6 * (Product (Sgm 6n+1_Primes))) - 2) ;
then M,3 are_congruent_mod (6 * (Product (Sgm 6n+1_Primes))) + 1 ;
then A25: ((6 * (Product (Sgm 6n+1_Primes))) + 1) gcd M = ((6 * (Product (Sgm 6n+1_Primes))) + 1) gcd 3 by WSIERP_1:43;
A26: ((6 * (Product (Sgm 6n+1_Primes))) + 1) gcd 3 <= 3 by NUMBER03:13;
hence contradiction by A24, A25, NAT_D:7; :: thesis: verum
end;
suppose A27: order ((6 * (Product (Sgm 6n+1_Primes))),p) = 3 ; :: thesis: contradiction
then (- 1) mod p = 1 by A14, A17, NAT_D:64;
hence contradiction by A13, A15, A16, A27, PEPIN:49, NAT_D:7; :: thesis: verum
end;
suppose A28: order ((6 * (Product (Sgm 6n+1_Primes))),p) = 6 ; :: thesis: contradiction
Euler p = p - 1 by EULER_1:20;
then 6 divides p - 1 by A10, A11, A28, Th4, INT_8:9;
then consider i being Integer such that
A29: p - 1 = 6 * i ;
i >= 0 by A29;
then reconsider i = i as Element of NAT by INT_1:3;
p = (6 * i) + 1 by A29;
then p in 6n+1_Primes ;
then A30: p divides Product (Sgm 6n+1_Primes) by A1, NUMBER09:16;
Product (Sgm 6n+1_Primes) divides 6 * (Product (Sgm 6n+1_Primes)) ;
hence contradiction by A11, A30, INT_2:9; :: thesis: verum
end;
end;