let l be non zero Nat; ( Fermat l is prime iff 3 |^ (((Fermat l) - 1) / 2), - 1 are_congruent_mod Fermat l )
set k = 1;
A1: 2 |^ 2 =
2 |^ (1 + 1)
.=
(2 |^ 1) * 2
by NEWTON:6
.=
2 * 2
;
l + 1 >= 0 + 1
by XREAL_1:6;
then
l >= 1
by NAT_1:13;
then
2 |^ l >= 2 |^ 1
by Th1;
then
2 |^ l >= 2
;
then reconsider l1 = 2 |^ l as 2 _or_greater Nat by EC_PF_2:def 1;
A2:
not 3 divides 1
by INT_2:27;
(2 |^ l1) - 1 >= 4 - 1
by A1, XREAL_1:9, EC_PF_2:def 1;
then A3:
1 <= (2 |^ l1) - 1
by XXREAL_0:2;
A4:
(1 * (2 |^ l1)) + 1 = Fermat l
by PEPIN:def 3;
((Fermat l) - 1) / 2 =
(((2 |^ (2 |^ l)) + 1) - 1) / 2
by PEPIN:def 3
.=
(2 |^ ((l1 - 1) + 1)) / 2
.=
((2 |^ (l1 - 1)) * 2) / 2
by NEWTON:6
.=
1 * (2 |^ (l1 - 1))
;
hence
( Fermat l is prime iff 3 |^ (((Fermat l) - 1) / 2), - 1 are_congruent_mod Fermat l )
by A2, A3, A4, Th41; verum