let p, n be Nat; :: thesis: ( p is prime & p > 2 & p divides Fermat n implies ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1 )
assume A1:
( p is prime & p > 2 & p divides Fermat n )
; :: thesis: ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1
set 2N = 2 |^ (2 |^ n);
A2:
p > 1
by A1, INT_2:def 5;
set t = (Fermat n) div p;
A3:
p * ((Fermat n) div p) = (2 |^ (2 |^ n)) + 1
by A1, NAT_D:3;
A4:
2 |^ (2 |^ n) > 1
by Th26, PREPOWER:13;
then
(2 |^ (2 |^ n)) * (2 |^ (2 |^ n)) > 1 * (2 |^ (2 |^ n))
by XREAL_1:70;
then A5:
(2 |^ (2 |^ n)) ^2 > 1
by A4, XXREAL_0:2;
A6:
- 1, - 1 are_congruent_mod p
by INT_1:32;
(p * ((Fermat n) div p)) - 0 = p * ((Fermat n) div p)
;
then
p * ((Fermat n) div p), 0 are_congruent_mod p
by INT_1:def 3;
then A7:
(p * ((Fermat n) div p)) + (- 1),0 + (- 1) are_congruent_mod p
by A6, INT_1:37;
then
(2 |^ (2 |^ n)) ^2 ,(- 1) ^2 are_congruent_mod p
by A3, INT_1:39;
then
((2 |^ (2 |^ n)) ^2 ) mod p = 1
by A2, A5, Lm15;
then A8:
(2 |^ (2 |^ (n + 1))) mod p = 1
by Lm12;
A9:
(2 |^ (2 |^ n)) mod p <> 1
A10:
2,p are_relative_prime
by A1, INT_2:44, INT_2:47;
then A11:
order 2,p divides 2 |^ (n + 1)
by A2, A8, Th52, PREPOWER:13;
order 2,p <> 0
by A2, A10, Def2;
then
order 2,p >= 1
by NAT_1:14;
then A12:
( order 2,p = 1 or order 2,p > 1 )
by XXREAL_0:1;
(2 |^ (n + 1)) div 2 =
(2 * (2 |^ n)) div 2
by NEWTON:11
.=
2 |^ n
by NAT_D:18
;
then
not order 2,p divides (2 |^ (n + 1)) div 2
by A1, A2, A9, Th53, INT_2:44, INT_2:47;
then
order 2,p = 2 |^ (n + 1)
by A11, A12, Th39, INT_2:44, NAT_D:6;
then
2 |^ (n + 1) divides p -' 1
by A1, Th54, INT_2:44, INT_2:47;
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 13;
p - 1 > 1 - 1
by A2, XREAL_1:11;
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
; :: thesis: verum