A1: 4 -' 1 =
4 - 1
by XREAL_0:def 2
.=
3 + 0
;
A2: 17 -' 1 =
17 - 1
by XREAL_0:def 2
.=
16 + 0
;
2 to_power 1 =
2 |^ 1
.=
2
by NEWTON:5
;
then 16 div 2 =
2 to_power (4 -' 1)
by NAT_2:16, POWER:62
.=
8
by A1, POWER:61
;
then
((Fermat 2) -' 1) div 2 = (16 * 0) + 8
by A2, Th57;
then
Fermat 2 divides (3 |^ (((Fermat 2) -' 1) div 2)) + 1
by Lm23;
then
Fermat 2 divides (3 |^ (((Fermat 2) -' 1) div 2)) - (- 1)
;
then
3 |^ (((Fermat 2) -' 1) div 2), - 1 are_congruent_mod Fermat 2
by INT_2:15;
hence
17 is prime
by Th57, Th63; verum