let a be Nat; :: thesis: for k being Integer st k <> 1 holds
ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite )
let k be Integer; :: thesis: ( k <> 1 implies ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite ) )
assume A1: k <> 1 ; :: thesis: ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite )
k - 1 <> 0 by A1;
then consider s being Nat, h being odd Integer such that
A2: k - 1 = h * (2 |^ s) by Th26;
consider m being positive Nat such that
A3: 2 |^ (2 |^ m) > a - k by Th25;
consider L being positive Nat such that
A4: 2 |^ (2 |^ L) > (- k) + 2 by Th25;
set l = max ((max (s,m)),L);
reconsider l = max ((max (s,m)),L) as positive Nat ;
set p = (2 |^ (2 |^ l)) + k;
m <= l by XXREAL_0:25, XXREAL_0:30;
then A5: 2 |^ m <= 2 |^ l by PREPOWER:93;
A6: (2 |^ (2 |^ L)) + k > ((- k) + 2) + k by A4, XREAL_1:8;
2 |^ L <= 2 |^ l by PREPOWER:93, XXREAL_0:25;
then A7: (2 |^ (2 |^ L)) + k <= (2 |^ (2 |^ l)) + k by XREAL_1:6, PREPOWER:93;
then A8: (2 |^ (2 |^ l)) + k > 2 by A6, XXREAL_0:2;
A9: (2 |^ (2 |^ m)) + k > (a - k) + k by A3, XREAL_1:8;

per cases ( (2 |^ (2 |^ l)) + k is composite or not (2 |^ (2 |^ l)) + k is composite ) ;

suppose A10: (2 |^ (2 |^ l)) + k is composite ; :: thesis: ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite )

take l ; :: thesis: ( a < (2 |^ (2 |^ l)) + k & (2 |^ (2 |^ l)) + k is composite )
(2 |^ (2 |^ m)) + k <= (2 |^ (2 |^ l)) + k by A5, XREAL_1:6, PREPOWER:93;
hence a < (2 |^ (2 |^ l)) + k by A9, XXREAL_0:2; :: thesis: (2 |^ (2 |^ l)) + k is composite
thus (2 |^ (2 |^ l)) + k is composite by A10; :: thesis: verum

end;

suppose not (2 |^ (2 |^ l)) + k is composite ; :: thesis: ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite )

then reconsider p = (2 |^ (2 |^ l)) + k as Prime by A6, A7, XXREAL_0:2, NUMBER02:def 1;
A11: s <= l by XXREAL_0:25, XXREAL_0:30;
l < 2 |^ l by NAT_3:2;
then consider N being Nat such that
A12: 2 |^ l = s + N by A11, XXREAL_0:2, NAT_1:10;
A13: (2 |^ (2 |^ l)) + ((2 |^ s) * h) = ((2 |^ s) * (2 |^ N)) + ((2 |^ s) * h) by A12, NEWTON:8
.= (2 |^ s) * ((2 |^ N) + h) ;
then 2 |^ s divides p - 1 by A2;
then consider h1 being Nat such that
A14: p - 1 = (2 |^ s) * h1 by NAT_D:def 3;
A15: h1 > 0 by A14;
h1 is odd

proof

assume h1 is even ; :: thesis: contradiction
then consider c, d being Nat such that
d is odd and
A16: c > 0 and
A17: h1 = (2 |^ c) * d by A15, NAT_5:2;
N > 0

proof

assume N <= 0 ; :: thesis: contradiction
then N = 0 ;
hence contradiction by A11, A12, NAT_3:2; :: thesis: verum

end;

hence contradiction by A2, A13, A14, A16, A17, XCMPLX_1:5; :: thesis: verum

end;

then reconsider h1 = h1 as odd Nat ;
A18: Euler p = p - 1 by EULER_1:20;
A19: p > 1 by INT_2:def 4;
(2 |^ (2 |^ m)) + k <= (2 |^ (2 |^ l)) + k by A5, PREPOWER:93, XREAL_1:6;
then A20: a < (2 |^ (2 |^ l)) + k by A9, XXREAL_0:2;
A21: 2 |^ 1,p are_coprime by A8, PEPIN:17, NAT_5:3;
A22: (2 |^ (2 |^ l)) + k, 0 are_congruent_mod p ;

per cases ( h1 = 1 or h1 <> 1 ) ;

suppose A23: h1 = 1 ; :: thesis: ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite )

then reconsider h1 = 1 as odd Nat ;
take l + (Euler 1) ; :: thesis: ( a < (2 |^ (2 |^ (l + (Euler 1)))) + k & (2 |^ (2 |^ (l + (Euler 1)))) + k is composite )
2 |^ (s + (Euler 1)) = (2 |^ s) * (2 |^ (Euler 1)) by NEWTON:8;
then 2 |^ s,2 |^ (s + (Euler 1)) are_congruent_mod p - 1 by A14, A23, INT_4:10, INT_1:13;
then 2 |^ l,2 |^ (l + (Euler 1)) are_congruent_mod p - 1 by A11, Th29;
then 2 |^ (l + (Euler 1)),2 |^ l are_congruent_mod p - 1 by INT_1:14;
then 2 |^ (2 |^ (l + (Euler 1))),2 |^ (2 |^ l) are_congruent_mod p by A18, A21, Th69;
then (2 |^ (2 |^ (l + (Euler 1)))) + k,(2 |^ (2 |^ l)) + k are_congruent_mod p ;
then A24: (2 |^ (2 |^ (l + (Euler 1)))) + k, 0 are_congruent_mod p by A22, INT_1:15;
2 |^ l <= 2 |^ (l + (Euler 1)) by PREPOWER:93, NAT_1:11;
then 2 |^ (2 |^ l) <= 2 |^ (2 |^ (l + (Euler 1))) by PREPOWER:93;
then A25: (2 |^ (2 |^ l)) + k <= (2 |^ (2 |^ (l + (Euler 1)))) + k by XREAL_1:6;
hence a < (2 |^ (2 |^ (l + (Euler 1)))) + k by A20, XXREAL_0:2; :: thesis: (2 |^ (2 |^ (l + (Euler 1)))) + k is composite

now :: thesis: not (2 |^ (2 |^ (l + (Euler 1)))) + k is prime

assume (2 |^ (2 |^ (l + (Euler 1)))) + k is prime ; :: thesis: contradiction
then p = (2 |^ (2 |^ (l + (Euler 1)))) + k by A19, A24;
then 2 |^ l = 2 |^ (l + (Euler 1)) by PEPIN:30;
then l + 0 = l + (Euler 1) by PEPIN:30;
hence contradiction ; :: thesis: verum

end;

hence (2 |^ (2 |^ (l + (Euler 1)))) + k is composite by A8, A25, XXREAL_0:2, NUMBER02:def 1; :: thesis: verum

end;

suppose A26: h1 <> 1 ; :: thesis: ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite )

take l + (Euler h1) ; :: thesis: ( a < (2 |^ (2 |^ (l + (Euler h1)))) + k & (2 |^ (2 |^ (l + (Euler h1)))) + k is composite )
2 |^ 1,h1 are_coprime by NAT_5:3;
then A27: (2 |^ (Euler h1)) mod h1 = 1 by A26, EULER_2:18, NAT_1:25;
A28: 2 |^ (s + (Euler h1)) = (2 |^ s) * (2 |^ (Euler h1)) by NEWTON:8;
1 mod h1 = 1 by A26, NAT_D:14, NAT_1:25;
then (2 |^ (Euler h1)) * (2 |^ s),1 * (2 |^ s) are_congruent_mod h1 * (2 |^ s) by A27, NAT_D:64, INT_4:10;
then 2 |^ s,2 |^ (s + (Euler h1)) are_congruent_mod p - 1 by A14, A28, INT_1:14;
then 2 |^ l,2 |^ (l + (Euler h1)) are_congruent_mod p - 1 by A11, Th29;
then 2 |^ (l + (Euler h1)),2 |^ l are_congruent_mod p - 1 by INT_1:14;
then 2 |^ (2 |^ (l + (Euler h1))),2 |^ (2 |^ l) are_congruent_mod p by A18, A21, Th69;
then (2 |^ (2 |^ (l + (Euler h1)))) + k,(2 |^ (2 |^ l)) + k are_congruent_mod p ;
then A29: (2 |^ (2 |^ (l + (Euler h1)))) + k, 0 are_congruent_mod p by A22, INT_1:15;
2 |^ l <= 2 |^ (l + (Euler h1)) by PREPOWER:93, NAT_1:11;
then 2 |^ (2 |^ l) <= 2 |^ (2 |^ (l + (Euler h1))) by PREPOWER:93;
then A30: (2 |^ (2 |^ l)) + k <= (2 |^ (2 |^ (l + (Euler h1)))) + k by XREAL_1:6;
hence a < (2 |^ (2 |^ (l + (Euler h1)))) + k by A20, XXREAL_0:2; :: thesis: (2 |^ (2 |^ (l + (Euler h1)))) + k is composite

now :: thesis: not (2 |^ (2 |^ (l + (Euler h1)))) + k is prime

assume (2 |^ (2 |^ (l + (Euler h1)))) + k is prime ; :: thesis: contradiction
then p = (2 |^ (2 |^ (l + (Euler h1)))) + k by A19, A29;
then 2 |^ l = 2 |^ (l + (Euler h1)) by PEPIN:30;
then l + 0 = l + (Euler h1) by PEPIN:30;
hence contradiction ; :: thesis: verum

end;

hence (2 |^ (2 |^ (l + (Euler h1)))) + k is composite by A8, A30, XXREAL_0:2, NUMBER02:def 1; :: thesis: verum

end;

end;

end;

end;