let n be Nat; ( 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n implies Fermat n is prime )
per cases
( n = 0 or n > 0 )
;
suppose A1:
n > 0
;
( 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n implies Fermat n is prime )
Fermat n > 2
by Th60;
then consider p being
Element of
NAT such that A2:
p is
prime
and A3:
p divides Fermat n
by INT_2:48;
set d =
order 3,
p;
consider i being
Nat such that A4:
Fermat n = p * i
by A3, NAT_D:def 3;
A5:
p > 2
A8:
(Fermat n) - 1
>= 0
;
assume A9:
3
|^ (((Fermat n) -' 1) div 2),
- 1
are_congruent_mod Fermat n
;
Fermat n is prime then A10:
(3 |^ (((Fermat n) -' 1) div 2)) ^2 ,
(- 1) ^2 are_congruent_mod Fermat n
by INT_1:39;
((Fermat n) -' 1) mod 2
= 0
by Lm13;
then A11:
3
|^ ((Fermat n) -' 1),
(- 1) ^2 are_congruent_mod Fermat n
by A10, Th28;
set 2N = 2
|^ (2 |^ n);
assume A12:
not
Fermat n is
prime
;
contradictionreconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
A13:
1
< p
by A2, INT_2:def 5;
A14:
p <> 3
then
order 3,
p divides p -' 1
by A2, Th44, Th54, INT_2:47;
then consider x being
Nat such that A16:
p -' 1
= (order 3,p) * x
by NAT_D:def 3;
A17:
3
|^ (((Fermat n) -' 1) div 2),
- 1
are_congruent_mod p
by A9, A4, INT_1:41;
A18:
not
order 3,
p divides ((Fermat n) -' 1) div 2
proof
assume
order 3,
p divides ((Fermat n) -' 1) div 2
;
contradiction
then
(3 |^ (((Fermat n) -' 1) div 2)) mod p = 1
by A2, A14, A13, Th44, Th53, INT_2:47;
then
3
|^ (((Fermat n) -' 1) div 2),1
are_congruent_mod p
by A13, Th40;
then
1,
- 1
are_congruent_mod p
by A17, Th43;
then
p divides 1
- (- 1)
by INT_2:19;
hence
contradiction
by A5, NAT_D:7;
verum
end; then A19:
not
order 3,
p divides (2 |^ (2 |^ n)) div 2
by A8, XREAL_0:def 2;
A20:
3,
p are_relative_prime
by A2, A14, Th44, INT_2:47;
then A21:
order 3,
p <> 0
by A13, Def2;
A22:
order 3,
p > 1
proof
assume A23:
order 3,
p <= 1
;
contradiction
hence
contradiction
;
verum
end;
3
|^ ((Fermat n) -' 1) > 1
by Lm14, Th26;
then
(3 |^ ((Fermat n) -' 1)) mod p = 1
by A4, A13, A11, Lm11, INT_1:41;
then
order 3,
p divides (Fermat n) -' 1
by A20, A13, Th52;
then
order 3,
p divides 2
|^ (2 |^ n)
by A8, XREAL_0:def 2;
then order 3,
p =
2
|^ (2 |^ n)
by A19, A22, Th39, INT_2:44
.=
(Fermat n) -' 1
by A8, XREAL_0:def 2
;
then A24:
order 3,
p = 2
|^ (2 |^ n)
by A8, XREAL_0:def 2;
A25:
(p * i) mod (2 |^ (2 |^ n)) = 1
by A4, Lm15;
p - 1
> 1
- 1
by A13, XREAL_1:11;
then A26:
p - 1
= x * (order 3,p)
by A16, XREAL_0:def 2;
then A27:
p = (x * (2 |^ (2 |^ n))) + 1
by A24;
then p mod (2 |^ (2 |^ n)) =
1
mod (2 |^ (2 |^ n))
by NAT_D:21
.=
1
by Lm2, NAT_D:24
;
then
(1 * i) mod (2 |^ (2 |^ n)) = 1
by A25, EULER_2:10;
then consider y being
Nat such that A28:
i = ((2 |^ (2 |^ n)) * y) + 1
and
1
< 2
|^ (2 |^ n)
by NAT_D:def 2;
A29:
2
|^ (2 |^ n) <> 0
by Lm2;
A30:
x >= 1
reconsider y =
y as
Element of
NAT by ORDINAL1:def 13;
Fermat n =
((x * (2 |^ (2 |^ n))) + 1) * ((y * (2 |^ (2 |^ n))) + 1)
by A4, A24, A26, A28
.=
((2 |^ (2 |^ n)) * ((((x * y) * (2 |^ (2 |^ n))) + x) + y)) + 1
;
then A31: 1 =
((2 |^ (2 |^ n)) * ((((x * y) * (2 |^ (2 |^ n))) + x) + y)) div (2 |^ (2 |^ n))
by A29, Th48
.=
(((x * y) * (2 |^ (2 |^ n))) + x) + y
by A29, NAT_D:18
;
2
|^ (2 |^ n) > 1
by Lm2;
then p =
(1 * (2 |^ (2 |^ n))) + 1
by A27, A30, A31, Lm1
.=
Fermat n
;
hence
contradiction
by A12, A2;
verum end;