let n, p be Nat; ( p is prime & p > 2 & p divides Fermat n implies ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1 )
assume that
A1:
p is prime
and
A2:
p > 2
and
A3:
p divides Fermat n
; ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1
A4:
p > 1
by A1, INT_2:def 4;
set t = (Fermat n) div p;
set 2N = 2 |^ (2 |^ n);
A5:
(p * ((Fermat n) div p)) + (- 1),0 + (- 1) are_congruent_mod p
;
A6:
p * ((Fermat n) div p) = (2 |^ (2 |^ n)) + 1
by A3, NAT_D:3;
A7:
(2 |^ (2 |^ n)) mod p <> 1
A8:
2,p are_coprime
by A1, A2, INT_2:28, INT_2:30;
then
order (2,p) <> 0
by A4, Def2;
then
order (2,p) >= 1
by NAT_1:14;
then A9:
( order (2,p) = 1 or order (2,p) > 1 )
by XXREAL_0:1;
A10:
2 |^ (2 |^ n) > 1
by Th25, PREPOWER:6;
then
(2 |^ (2 |^ n)) * (2 |^ (2 |^ n)) > 1 * (2 |^ (2 |^ n))
by XREAL_1:68;
then A11:
(2 |^ (2 |^ n)) ^2 > 1
by A10, XXREAL_0:2;
(2 |^ (2 |^ n)) ^2 ,(- 1) ^2 are_congruent_mod p
by A6, A5, INT_1:18;
then
((2 |^ (2 |^ n)) ^2) mod p = 1
by A4, A11, Lm11;
then
(2 |^ (2 |^ (n + 1))) mod p = 1
by Lm8;
then A12:
order (2,p) divides 2 |^ (n + 1)
by A4, A8, Th47;
(2 |^ (n + 1)) div 2 =
(2 * (2 |^ n)) div 2
by NEWTON:6
.=
2 |^ n
by NAT_D:18
;
then
not order (2,p) divides (2 |^ (n + 1)) div 2
by A1, A2, A4, A7, Th48, INT_2:28, INT_2:30;
then
order (2,p) = 2 |^ (n + 1)
by A12, A9, Th38, INT_2:28, NAT_D:6;
then
2 |^ (n + 1) divides p -' 1
by A1, A2, Th49, INT_2:28, INT_2:30;
then consider t2 being Nat such that
A13:
p -' 1 = (2 |^ (n + 1)) * t2
by NAT_D:def 3;
reconsider t2 = t2 as Element of NAT by ORDINAL1:def 12;
p - 1 > 1 - 1
by A4, XREAL_1:9;
then
p - 1 = (2 |^ (n + 1)) * t2
by A13, XREAL_0:def 2;
then
p = (t2 * (2 |^ (n + 1))) + 1
;
hence
ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1
; verum