let k be Nat; ( k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 & k, - 1 are_congruent_mod 6700417 & k > 6700417 implies for n being positive Nat holds
( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) ) )
assume that
A1:
k,1 are_congruent_mod ((2 |^ 32) - 1) * 641
and
A2:
k, - 1 are_congruent_mod 6700417
and
A3:
k > 6700417
; for n being positive Nat holds
( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) )
let n be positive Nat; ( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) )
consider m, t being Nat such that
A4:
n = (2 |^ m) * ((2 * t) + 1)
by NAGATA_2:1;
A5:
(k * (2 |^ n)) + 1 >= 1 + 1
by A3, NAT_1:14, XREAL_1:6;
A6:
Fermat m <> 1
by PEPIN:55;
per cases
( m <= 4 or m > 4 )
;
suppose A7:
m <= 4
;
( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) )A8:
( 2
|^ n,2
|^ n are_congruent_mod (2 |^ 32) - 1 & 1,1
are_congruent_mod (2 |^ 32) - 1 )
by INT_1:11;
k,1
are_congruent_mod (2 |^ 32) - 1
by A1, INT_1:20;
then A9:
k * (2 |^ n),1
* (2 |^ n) are_congruent_mod (2 |^ 32) - 1
by A8, INT_1:18;
Fermat m divides (2 |^ 32) - 1
by A7, Lm2;
then A10:
Fermat m divides ((k * (2 |^ n)) + 1) - ((2 |^ n) + 1)
by A9, INT_2:9;
Fermat m divides (2 |^ n) + 1
by A4, Lm1;
then A11:
Fermat m divides (((k * (2 |^ n)) + 1) - ((2 |^ n) + 1)) + ((2 |^ n) + 1)
by A10, WSIERP_1:4;
2
|^ n >= 1
by NAT_1:14;
then
k * (2 |^ n) >= 1
* 6700417
by A3, XREAL_1:66;
then A12:
(k * (2 |^ n)) + 1
> 6700417
by NAT_1:13;
( 6700417
> Fermat 4 &
Fermat 4
>= Fermat m )
by A7, NUMBER09:31, Th28;
then
6700417
> Fermat m
by XXREAL_0:2;
then
not
(k * (2 |^ n)) + 1 is
prime
by A6, A11, A12;
hence
(
(k * (2 |^ n)) + 1 is
composite & ( not not
Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not
Fermat 4
divides (k * (2 |^ n)) + 1 or 641
divides (k * (2 |^ n)) + 1 or 6700417
divides (k * (2 |^ n)) + 1 ) )
by A7, A11, A5, NUMBER02:def 1;
verum end; suppose
m > 4
;
( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) )then
m >= 4
+ 1
by NAT_1:13;
per cases then
( m = 5 or m > 5 )
by XXREAL_0:1;
suppose A13:
m = 5
;
( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) )A14:
( 2
|^ n,2
|^ n are_congruent_mod 641 & 1,1
are_congruent_mod 641 )
by INT_1:11;
k,1
are_congruent_mod 641
by A1, INT_1:20;
then A15:
k * (2 |^ n),1
* (2 |^ n) are_congruent_mod 641
by A14, INT_1:18;
( 641
divides Fermat m &
Fermat m divides (2 |^ n) + 1 )
by A13, A4, Lm1, NAT_6:45;
then
641
divides (2 |^ n) + 1
by INT_2:9;
then A16:
641
divides (((k * (2 |^ n)) + 1) - ((2 |^ n) + 1)) + ((2 |^ n) + 1)
by A15, WSIERP_1:4;
2
|^ n >= 1
by NAT_1:14;
then
k * (2 |^ n) >= 1
* 6700417
by A3, XREAL_1:66;
then
(k * (2 |^ n)) + 1
> 6700417
by NAT_1:13;
then
(k * (2 |^ n)) + 1
> 641
by XXREAL_0:2;
then
not
(k * (2 |^ n)) + 1 is
prime
by A16;
hence
(
(k * (2 |^ n)) + 1 is
composite & ( not not
Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not
Fermat 4
divides (k * (2 |^ n)) + 1 or 641
divides (k * (2 |^ n)) + 1 or 6700417
divides (k * (2 |^ n)) + 1 ) )
by A16, A5, NUMBER02:def 1;
verum end; suppose
m > 5
;
( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) )then
m >= 5
+ 1
by NAT_1:13;
then
( 2
|^ 6
divides 2
|^ m & 2
|^ m divides n )
by A4, NEWTON:89;
then consider h being
Nat such that A17:
n = (2 |^ 6) * h
by INT_2:9, NAT_D:def 3;
A18:
( 2
|^ n,2
|^ n are_congruent_mod 6700417 & 1,1
are_congruent_mod 6700417 )
by INT_1:11;
k * (2 |^ n),
(- 1) * (2 |^ n) are_congruent_mod 6700417
by A2, A18, INT_1:18;
then A19:
6700417
divides ((k * (2 |^ n)) + 1) + ((2 |^ n) - 1)
;
6700417
divides Fermat 5
by Th28;
then A20:
6700417
divides (2 |^ (2 |^ 5)) + 1
by PEPIN:def 3;
(2 |^ (2 |^ 5)) |^ (2 * 1) =
2
|^ ((2 |^ 5) * 2)
by NEWTON:9
.=
2
|^ (2 |^ (5 + 1))
by NEWTON:6
;
then
(2 |^ (2 |^ 5)) + 1
divides (2 |^ (2 |^ 6)) - (1 |^ (2 * 1))
by NEWTON01:36;
then A21:
6700417
divides (2 |^ (2 |^ 6)) - 1
by A20, INT_2:9;
(2 |^ (2 |^ 6)) |^ h = 2
|^ n
by A17, NEWTON:9;
then
(2 |^ (2 |^ 6)) - 1
divides (2 |^ n) - (1 |^ h)
by NEWTON01:33;
then A22:
6700417
divides (2 |^ n) - (1 |^ h)
by A21, INT_2:9;
2
|^ n >= 1
by NAT_1:14;
then
k * (2 |^ n) >= 1
* 6700417
by A3, XREAL_1:66;
then
(k * (2 |^ n)) + 1
> 6700417
by NAT_1:13;
then
not
(k * (2 |^ n)) + 1 is
prime
by A22, A19, INT_2:1;
hence
(
(k * (2 |^ n)) + 1 is
composite & ( not not
Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not
Fermat 4
divides (k * (2 |^ n)) + 1 or 641
divides (k * (2 |^ n)) + 1 or 6700417
divides (k * (2 |^ n)) + 1 ) )
by A5, A22, A19, INT_2:1, NUMBER02:def 1;
verum end; end;