let a be Nat; :: thesis: ( 1 < a & a <= 100 implies ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite ) )
assume that
A1: 1 < a and
A2: a <= 100 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
deffunc H1( Nat) -> set = a |^ (2 |^ $1);
deffunc H2( Nat) -> Element of omega = H1($1) + 1;
per cases ( a is odd or a = 2 or a = 4 or a = 6 or a = 8 or a = 10 or a = 12 or a = 14 or a = 16 or a = 18 or a = 20 or a = 22 or a = 24 or a = 26 or a = 28 or a = 30 or a = 32 or a = 34 or a = 36 or a = 38 or a = 40 or a = 42 or a = 44 or a = 46 or a = 48 or a = 50 or a = 52 or a = 54 or a = 56 or a = 58 or a = 60 or a = 62 or a = 64 or a = 66 or a = 68 or a = 70 or a = 72 or a = 74 or a = 76 or a = 78 or a = 80 or a = 82 or a = 84 or a = 86 or a = 88 or a = 90 or a = 92 or a = 94 or a = 96 or a = 98 or a = 100 ) by A1, A2, Lm28;
suppose A3: a is odd ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
0 + 1 <= H1(n) by A1, NAT_1:13;
then 1 + 1 <= H2(n) by XREAL_1:6;
hence 2 <= H2(n) ; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
A4: H2(n) is even by A3;
a |^ 2 = a * a by WSIERP_1:1;
then H2(n) <> 2 by A1, NAT_1:15;
hence not H2(n) is prime by A4; :: thesis: verum
end;
suppose A5: a = 2 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 5; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
thus 2 <= H2(n) by A5, Lm51, Lm50; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
thus not H2(n) is prime by A5, NAT_6:44; :: thesis: verum
end;
suppose A6: a = 4 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 4; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
thus 2 <= H2(n) by A6, Lm46, Lm51, Lm50; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
thus not H2(n) is prime by A6, Lm46, NAT_6:44; :: thesis: verum
end;
suppose A7: a = 6 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A8: 17 < H2(n) by A7, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 6) |^ (2 |^ 3)) + 1 by Th37;
hence not (a |^ (2 |^ n)) + 1 is prime by A7, A8; :: thesis: verum
end;
suppose A9: a = 8 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A10: 17 < H2(n) by A9, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 8) |^ (2 |^ 2)) + 1 by Th38;
hence not (a |^ (2 |^ n)) + 1 is prime by A9, A10; :: thesis: verum
end;
suppose A11: a = 10 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A12: 17 < H2(n) by A11, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 10) |^ (2 |^ 3)) + 1 by Th39;
hence not (a |^ (2 |^ n)) + 1 is prime by A11, A12; :: thesis: verum
end;
suppose A13: a = 12 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A14: 17 < H2(n) by A13, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 12) |^ (2 |^ 3)) + 1 by Th40;
hence not (a |^ (2 |^ n)) + 1 is prime by A13, A14; :: thesis: verum
end;
suppose A15: a = 14 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A16: 17 < H2(n) by A15, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 14) |^ (2 |^ 3)) + 1 by Th41;
hence not (a |^ (2 |^ n)) + 1 is prime by A15, A16; :: thesis: verum
end;
suppose A17: a = 16 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
thus 2 <= H2(n) by A17, Lm51, Lm50, Lm47; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
thus not H2(n) is prime by A17, Lm47, NAT_6:44; :: thesis: verum
end;
suppose A18: a = 18 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A19: H1(n) = 18 * 18 by A18, WSIERP_1:1;
hence 2 <= H2(n) ; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
325 = 5 * 65 ;
then 5 divides 325 ;
hence not H2(n) is prime by A19; :: thesis: verum
end;
suppose A20: a = 20 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A21: 17 < H2(n) by A20, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 20) |^ (2 |^ 3)) + 1 by Th42;
hence not (a |^ (2 |^ n)) + 1 is prime by A20, A21; :: thesis: verum
end;
suppose A22: a = 22 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A23: 17 < H2(n) by A22, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 22) |^ (2 |^ 3)) + 1 by Th43;
hence not (a |^ (2 |^ n)) + 1 is prime by A22, A23; :: thesis: verum
end;
suppose A24: a = 24 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A25: 17 < H2(n) by A24, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 24) |^ (2 |^ 3)) + 1 by Th44;
hence not (a |^ (2 |^ n)) + 1 is prime by A24, A25; :: thesis: verum
end;
suppose A26: a = 26 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A27: 17 < H2(n) by A26, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 26) |^ (2 |^ 2)) + 1 by Th45;
hence not (a |^ (2 |^ n)) + 1 is prime by A26, A27; :: thesis: verum
end;
suppose A28: a = 28 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A29: 17 < H2(n) by A28, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 28) |^ (2 |^ 3)) + 1 by Th46;
hence not (a |^ (2 |^ n)) + 1 is prime by A28, A29; :: thesis: verum
end;
suppose A30: a = 30 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A31: 17 < H2(n) by A30, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 30) |^ (2 |^ 1)) + 1 by Th47;
hence not (a |^ (2 |^ n)) + 1 is prime by A30, A31; :: thesis: verum
end;
suppose A32: a = 32 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A33: 17 < H2(n) by A32, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 0) + 32) |^ (2 |^ 2)) + 1 by Th48;
hence not (a |^ (2 |^ n)) + 1 is prime by A32, A33; :: thesis: verum
end;
suppose A34: a = 34 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A35: H1(n) = 34 * 34 by A34, WSIERP_1:1;
hence 2 <= H2(n) ; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
1157 = 13 * 89 ;
then 13 divides 1157 ;
hence not H2(n) is prime by A35; :: thesis: verum
end;
suppose A36: a = 36 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A37: 17 < H2(n) by A36, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 2) |^ (2 |^ 2)) + 1 by Th35;
hence not (a |^ (2 |^ n)) + 1 is prime by A36, A37; :: thesis: verum
end;
suppose A38: a = 38 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A39: 17 < H2(n) by A38, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 4) |^ (2 |^ 1)) + 1 by Th36;
hence not (a |^ (2 |^ n)) + 1 is prime by A38, A39; :: thesis: verum
end;
suppose A40: a = 40 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A41: 17 < H2(n) by A40, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 6) |^ (2 |^ 3)) + 1 by Th37;
hence not (a |^ (2 |^ n)) + 1 is prime by A40, A41; :: thesis: verum
end;
suppose A42: a = 42 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A43: 17 < H2(n) by A42, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 8) |^ (2 |^ 2)) + 1 by Th38;
hence not (a |^ (2 |^ n)) + 1 is prime by A42, A43; :: thesis: verum
end;
suppose A44: a = 44 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A45: 17 < H2(n) by A44, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 10) |^ (2 |^ 3)) + 1 by Th39;
hence not (a |^ (2 |^ n)) + 1 is prime by A44, A45; :: thesis: verum
end;
suppose A46: a = 46 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A47: 17 < H2(n) by A46, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 12) |^ (2 |^ 3)) + 1 by Th40;
hence not (a |^ (2 |^ n)) + 1 is prime by A46, A47; :: thesis: verum
end;
suppose A48: a = 48 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A49: 17 < H2(n) by A48, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 14) |^ (2 |^ 3)) + 1 by Th41;
hence not (a |^ (2 |^ n)) + 1 is prime by A48, A49; :: thesis: verum
end;
suppose A50: a = 50 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A51: H1(n) = 50 * 50 by A50, WSIERP_1:1;
hence 2 <= H2(n) ; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
2501 = 41 * 61 ;
then 41 divides 2501 ;
hence not H2(n) is prime by A51; :: thesis: verum
end;
suppose A52: a = 52 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A53: H1(n) = 52 * 52 by A52, WSIERP_1:1;
hence 2 <= H2(n) ; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
2705 = 5 * 541 ;
then 5 divides 2705 ;
hence not H2(n) is prime by A53; :: thesis: verum
end;
suppose A54: a = 54 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A55: 17 < H2(n) by A54, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 20) |^ (2 |^ 3)) + 1 by Th42;
hence not (a |^ (2 |^ n)) + 1 is prime by A54, A55; :: thesis: verum
end;
suppose A56: a = 56 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A57: 17 < H2(n) by A56, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 22) |^ (2 |^ 3)) + 1 by Th43;
hence not (a |^ (2 |^ n)) + 1 is prime by A56, A57; :: thesis: verum
end;
suppose A58: a = 58 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A59: 17 < H2(n) by A58, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 24) |^ (2 |^ 3)) + 1 by Th44;
hence not (a |^ (2 |^ n)) + 1 is prime by A58, A59; :: thesis: verum
end;
suppose A60: a = 60 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A61: 17 < H2(n) by A60, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 26) |^ (2 |^ 2)) + 1 by Th45;
hence not (a |^ (2 |^ n)) + 1 is prime by A60, A61; :: thesis: verum
end;
suppose A62: a = 62 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A63: 17 < H2(n) by A62, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 28) |^ (2 |^ 3)) + 1 by Th46;
hence not (a |^ (2 |^ n)) + 1 is prime by A62, A63; :: thesis: verum
end;
suppose A64: a = 64 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A65: 17 < H2(n) by A64, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 30) |^ (2 |^ 1)) + 1 by Th47;
hence not (a |^ (2 |^ n)) + 1 is prime by A64, A65; :: thesis: verum
end;
suppose A66: a = 66 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A67: 17 < H2(n) by A66, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 1) + 32) |^ (2 |^ 2)) + 1 by Th48;
hence not (a |^ (2 |^ n)) + 1 is prime by A66, A67; :: thesis: verum
end;
suppose A68: a = 68 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A69: H1(n) = 68 * 68 by A68, WSIERP_1:1;
hence 2 <= H2(n) ; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
4625 = 5 * 925 ;
then 5 divides 4625 ;
hence not H2(n) is prime by A69; :: thesis: verum
end;
suppose A70: a = 70 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A71: 17 < H2(n) by A70, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 2) |^ (2 |^ 2)) + 1 by Th35;
hence not (a |^ (2 |^ n)) + 1 is prime by A70, A71; :: thesis: verum
end;
suppose A72: a = 72 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A73: 17 < H2(n) by A72, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 4) |^ (2 |^ 1)) + 1 by Th36;
hence not (a |^ (2 |^ n)) + 1 is prime by A72, A73; :: thesis: verum
end;
suppose A74: a = 74 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A75: 17 < H2(n) by A74, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 6) |^ (2 |^ 3)) + 1 by Th37;
hence not (a |^ (2 |^ n)) + 1 is prime by A74, A75; :: thesis: verum
end;
suppose A76: a = 76 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A77: 17 < H2(n) by A76, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 8) |^ (2 |^ 2)) + 1 by Th38;
hence not (a |^ (2 |^ n)) + 1 is prime by A76, A77; :: thesis: verum
end;
suppose A78: a = 78 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A79: 17 < H2(n) by A78, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 10) |^ (2 |^ 3)) + 1 by Th39;
hence not (a |^ (2 |^ n)) + 1 is prime by A78, A79; :: thesis: verum
end;
suppose A80: a = 80 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A81: 17 < H2(n) by A80, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 12) |^ (2 |^ 3)) + 1 by Th40;
hence not (a |^ (2 |^ n)) + 1 is prime by A80, A81; :: thesis: verum
end;
suppose A82: a = 82 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A83: 17 < H2(n) by A82, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 14) |^ (2 |^ 3)) + 1 by Th41;
hence not (a |^ (2 |^ n)) + 1 is prime by A82, A83; :: thesis: verum
end;
suppose A84: a = 84 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 6; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A85: 84 |^ (2 |^ 6) = (84 |^ 2) |^ 32 by Lm6, NEWTON:9;
A86: 84 |^ 2 = 84 * 84 by WSIERP_1:1;
then (84 |^ 2) |^ 1 < (84 |^ 2) |^ 32 by PEPIN:66;
then 256 < 84 |^ (2 |^ 6) by A85, A86, XXREAL_0:2;
then A87: 256 + 1 < H2(n) by A84, XREAL_1:8;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
thus not (a |^ (2 |^ n)) + 1 is prime by A87, A84, Lm45; :: thesis: verum
end;
suppose A88: a = 86 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A89: H1(n) = 86 * 86 by A88, WSIERP_1:1;
hence 2 <= H2(n) ; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
7397 = 13 * 569 ;
then 13 divides 7397 ;
hence not H2(n) is prime by A89; :: thesis: verum
end;
suppose A90: a = 88 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A91: 17 < H2(n) by A90, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 20) |^ (2 |^ 3)) + 1 by Th42;
hence not (a |^ (2 |^ n)) + 1 is prime by A90, A91; :: thesis: verum
end;
suppose A92: a = 90 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A93: 17 < H2(n) by A92, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 22) |^ (2 |^ 3)) + 1 by Th43;
hence not (a |^ (2 |^ n)) + 1 is prime by A92, A93; :: thesis: verum
end;
suppose A94: a = 92 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A95: 17 < H2(n) by A94, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 24) |^ (2 |^ 3)) + 1 by Th44;
hence not (a |^ (2 |^ n)) + 1 is prime by A94, A95; :: thesis: verum
end;
suppose A96: a = 94 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A97: 17 < H2(n) by A96, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 26) |^ (2 |^ 2)) + 1 by Th45;
hence not (a |^ (2 |^ n)) + 1 is prime by A96, A97; :: thesis: verum
end;
suppose A98: a = 96 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 3; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A99: 17 < H2(n) by A98, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 28) |^ (2 |^ 3)) + 1 by Th46;
hence not (a |^ (2 |^ n)) + 1 is prime by A98, A99; :: thesis: verum
end;
suppose A100: a = 98 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 1; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A101: 17 < H2(n) by A100, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 30) |^ (2 |^ 1)) + 1 by Th47;
hence not (a |^ (2 |^ n)) + 1 is prime by A100, A101; :: thesis: verum
end;
suppose A102: a = 100 ; :: thesis: ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
take n = 2; :: thesis: ( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )
thus n <= 6 ; :: thesis: (a |^ (2 |^ n)) + 1 is composite
A103: 17 < H2(n) by A102, Lm49;
hence 2 <= H2(n) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (a |^ (2 |^ n)) + 1 is prime
17 divides (((34 * 2) + 32) |^ (2 |^ 2)) + 1 by Th48;
hence not (a |^ (2 |^ n)) + 1 is prime by A102, A103; :: thesis: verum
end;
end;