let n be Nat; ( n = 1 implies 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n )
A1: 2 -' 1 =
2 - 1
by XREAL_0:def 2
.=
1 + 0
;
A2: 5 -' 1 =
5 - 1
by XREAL_0:def 2
.=
4 + 0
;
A3: 2 to_power 2 =
2 |^ (1 + 1)
.=
(2 |^ 1) * 2
by NEWTON:6
.=
2 * 2
by NEWTON:5
;
assume A4:
n = 1
; 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n
2 to_power 1 =
2 |^ 1
.=
2
by NEWTON:5
;
then 4 div 2 =
2 to_power (2 -' 1)
by A3, NAT_2:16
.=
2 |^ 1
by A1
.=
2
by NEWTON:5
;
then
((Fermat 1) -' 1) div 2 = (4 * 0) + 2
by A2, Th51;
then
Fermat 1 divides (3 |^ (((Fermat n) -' 1) div 2)) + 1
by A4, Lm21;
then
Fermat 1 divides (3 |^ (((Fermat n) -' 1) div 2)) - (- 1)
;
hence
3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n
by A4; verum