let l be 2 _or_greater Nat; :: thesis: for k being positive Nat st not 3 divides k & k <= (2 |^ l) - 1 holds
( (k * (2 |^ l)) + 1 is prime iff 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 )
let k be positive Nat; :: thesis: ( not 3 divides k & k <= (2 |^ l) - 1 implies ( (k * (2 |^ l)) + 1 is prime iff 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 ) )
assume A1: ( not 3 divides k & k <= (2 |^ l) - 1 ) ; :: thesis: ( (k * (2 |^ l)) + 1 is prime iff 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 )
set s = 2 |^ l;
set a = 3;
set n = (k * (2 |^ l)) + 1;
k >= 1 by NAT_1:14;
then k * (2 |^ l) >= 1 * (2 |^ l) by XREAL_1:66;
then A2: (k * (2 |^ l)) + 1 >= (2 |^ l) + 1 by XREAL_1:7;
A3: (2 |^ l) / 2 = (2 |^ ((l - 1) + 1)) * (2 ")
.= ((2 |^ (l - 1)) * 2) * (2 ") by NEWTON:6
.= (2 |^ (l - 1)) * 1 ;
A4: 2 * (k * (2 |^ (l - 1))) = k * (2 * (2 |^ (l - 1)))
.= k * (2 |^ ((l - 1) + 1)) by NEWTON:6 ;
A5: l >= 1 by NAT_1:14;
A6: l + 1 >= 1 + 1 by NAT_1:14, XREAL_1:6;
A7: 2 |^ l >= l + 1 by NEWTON:85;
then 2 |^ l >= 1 + 1 by A6, XXREAL_0:2;
then (2 |^ l) + 1 >= 2 + 1 by XREAL_1:7;
then (k * (2 |^ l)) + 1 >= 2 + 1 by A2, XXREAL_0:2;
then (k * (2 |^ l)) + 1 > 2 by NAT_1:13;
then reconsider n = (k * (2 |^ l)) + 1 as odd 2 _greater Nat by A4, Def1;
2 * (k * (2 |^ (l - 1))) = k * (2 * (2 |^ (l - 1)))
.= k * (2 |^ ((l - 1) + 1)) by NEWTON:6 ;
then reconsider k2 = (k * (2 |^ l)) / 2 as Nat ;
A8: 3 |^ ((n - 1) / 2) = 3 |^ (k * (2 |^ (l - 1))) by A3;

A9: now :: thesis: ( 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 implies (k * (2 |^ l)) + 1 is prime )

assume A10: 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 ; :: thesis: (k * (2 |^ l)) + 1 is prime
reconsider s = 2 |^ l as Divisor of n - 1 by INT_2:2, Def2;
( s <> 0 & s <> 1 ) by A7, A6, XXREAL_0:2;
then reconsider s = s as non trivial Divisor of n - 1 by NAT_2:def 1;
A11: (3 |^ (k * (2 |^ (l - 1)))) * (3 |^ (k * (2 |^ (l - 1)))),(- 1) * (- 1) are_congruent_mod n by A10, INT_1:18;
A12: (3 |^ (k * (2 |^ (l - 1)))) * (3 |^ (k * (2 |^ (l - 1)))) = 3 |^ ((k * (2 |^ (l - 1))) + (k * (2 |^ (l - 1)))) by NEWTON:8
.= 3 |^ (k * ((2 |^ (l - 1)) * 2))
.= 3 |^ (k * (2 |^ ((l - 1) + 1))) by NEWTON:6
.= 3 |^ (k * (2 |^ l)) ;
A13: k * (2 |^ l) <= ((2 |^ l) - 1) * (2 |^ l) by A1, XREAL_1:64;
A14: (((2 |^ l) - 1) * (2 |^ l)) + 1 = (((2 |^ l) * (2 |^ l)) - (2 |^ l)) + 1
.= ((2 |^ (l + l)) - (2 |^ l)) + 1 by NEWTON:8 ;
then n <= ((2 |^ (l + l)) - (2 |^ l)) + 1 by A13, XREAL_1:6;
then A15: n < (((2 |^ (l + l)) - (2 |^ l)) + 1) + 1 by A14, NAT_1:13;
A16: s > sqrt n

proof

per cases ( l >= 2 or l < 2 ) ;

suppose l >= 2 ; :: thesis: s > sqrt n

then A17: 2 |^ l >= 2 |^ 2 by Th1;
2 |^ (1 + 1) = (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 ;
then 2 |^ l > 2 by A17, XXREAL_0:2;
then 2 - (2 |^ l) < (2 |^ l) - (2 |^ l) by XREAL_1:9;
then (2 |^ (l + l)) + ((- (2 |^ l)) + 2) < (2 |^ (l + l)) + 0 by XREAL_1:6;
then A18: n < 2 |^ (2 * l) by A15, XXREAL_0:2;
(2 |^ l) ^2 = 2 |^ (l + l) by NEWTON:8;
then sqrt (2 |^ (2 * l)) = 2 |^ l by SQUARE_1:def 2;
hence s > sqrt n by A18, SQUARE_1:27; :: thesis: verum

end;

suppose l < 2 ; :: thesis: s > sqrt n

then l < 1 + 1 ;
then l <= 1 by NAT_1:13;
then A19: l = 1 by A5, XXREAL_0:1;
then A20: n = (k * 2) + 1 ;
A21: k <= 2 - 1 by A1, A19;
k >= 1 by NAT_1:14;
then k = 1 by A21, XXREAL_0:1;
hence s > sqrt n by A20, SQUARE_1:27, SQUARE_1:20; :: thesis: verum

end;

end;

end;

now :: thesis: for q being prime Divisor of s holds ((3 |^ ((n - 1) / q)) - 1) gcd n = 1

let q be prime Divisor of s; :: thesis: ((3 |^ ((n - 1) / q)) - 1) gcd n = 1
A22: 3 |^ ((n - 1) / q), - 1 are_congruent_mod n by A8, A10, Th8, INT_2:28, Def2;
1 * ((3 |^ ((n - 1) / q)) - 1) = (3 |^ ((n - 1) / q)) - 1 ;
then A23: 1 divides (3 |^ ((n - 1) / q)) - 1 ;
1 * n = n ;
then A24: 1 divides n ;

now :: thesis: for m being Integer st m divides (3 |^ ((n - 1) / q)) - 1 & m divides n holds
m divides 1

let m be Integer; :: thesis: ( m divides (3 |^ ((n - 1) / q)) - 1 & m divides n implies m divides 1 )
assume A25: ( m divides (3 |^ ((n - 1) / q)) - 1 & m divides n ) ; :: thesis: m divides 1
then A26: 3 |^ ((n - 1) / q),1 are_congruent_mod m ;
consider j being Integer such that
A27: m * j = n by A25;
3 |^ ((n - 1) / q), - 1 are_congruent_mod m by A22, A27, INT_1:20;
then (3 |^ ((n - 1) / q)) - (3 |^ ((n - 1) / q)),(- 1) - 1 are_congruent_mod m by A26, INT_1:17;
then 0 + 1,(- 2) + 1 are_congruent_mod m ;
then ( m = 2 or m = 1 or m = - 2 or m = - 1 ) by Th20, INT_1:14;
hence m divides 1 by A25, INT_2:10, ABIAN:def 1; :: thesis: verum

end;

hence ((3 |^ ((n - 1) / q)) - 1) gcd n = 1 by A23, A24, INT_2:def 2; :: thesis: verum

end;

hence (k * (2 |^ l)) + 1 is prime by A12, A11, A16, Th21; :: thesis: verum

end;

now :: thesis: ( n is prime implies 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 )

assume n is prime ; :: thesis: 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1
then reconsider n = n as 2 _greater Prime ;
reconsider two = 2 as Prime by INT_2:28;
reconsider three = 3 as 2 _greater Prime by Def1, PEPIN:41;
A28: (2 |^ l) + 1 >= (2 |^ 2) + 1 by XREAL_1:6, EC_PF_2:def 1;
2 |^ 2 = 2 |^ (1 + 1)
.= (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 ;
then A29: 3 <> n by A28, A2, XXREAL_0:2;
A30: not n, 0 are_congruent_mod 3 by A29, INT_2:def 4;

A31: now :: thesis: not n,1 are_congruent_mod 3

assume A32: n,1 are_congruent_mod 3 ; :: thesis: contradiction
not three divides 2 |^ l by Th8, INT_2:28;
then 3 gcd (2 |^ l) = 1 by Th6;
hence contradiction by A1, INT_2:25, A32, INT_2:def 3; :: thesis: verum

end;

not not n, 0 are_congruent_mod 3 & ... & not n,3 - 1 are_congruent_mod 3 by Th13;
then A33: not not n, 0 are_congruent_mod 3 & ... & not n,2 are_congruent_mod 3 ;
A34: 2,2 + 1 are_coprime by PEPIN:1;
not three divides n by A29, INT_2:def 4;
then A35: n gcd 3 = 1 by Th6;
A36: ((3 - 1) / 2) * ((n - 1) / 2) = 1 * ((n - 1) / 2) ;
(n - 1) / 2 = (k * (2 |^ ((l - 1) + 1))) / 2
.= (k * ((2 |^ (l - 1)) * 2)) / 2 by NEWTON:6
.= k * (2 |^ ((l - 2) + 1))
.= k * ((2 |^ (l - 2)) * 2) by NEWTON:6
.= (2 * k) * (2 |^ (l - 2)) ;
then A37: (- 1) |^ ((n - 1) / 2) = 1 ;
(Leg (three,n)) * (Leg (n,three)) = 1 by A36, A37, A29, Th30;
then ( ( Leg (three,n) = 1 & Leg (n,three) = 1 ) or ( Leg (three,n) = - 1 & Leg (n,three) = - 1 ) ) by INT_1:9;
then Leg (3,n) = Leg (two,three) by A35, A33, A30, A31, A34, Th28
.= - 1 by Th23, A34, Def4 ;
hence 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 by A8, A35, Th31; :: thesis: verum

end;

hence ( (k * (2 |^ l)) + 1 is prime iff 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 ) by A9; :: thesis: verum