A1:
(2 |^ 7) * (2 |^ 7) = 2 |^ (7 + 7)
by NEWTON:8;
A2: 5 * 5 =
(5 |^ 1) * 5
.=
(5 |^ 1) * (5 |^ 1)
.=
5 |^ (1 + 1)
by NEWTON:8
;
A3:
(5 |^ 2) * (5 |^ 2) = 5 |^ (2 + 2)
by NEWTON:8;
A4:
(2 |^ 14) * (2 |^ 14) = 2 |^ (14 + 14)
by NEWTON:8;
A5:
(2 |^ 4) * (2 |^ 28) = 2 |^ (4 + 28)
by NEWTON:8;
A6: 2 |^ 2 =
2 |^ (1 + 1)
.=
(2 |^ 1) * 2
by NEWTON:6
.=
2 * 2
;
A7: 2 |^ 3 =
2 |^ (2 + 1)
.=
(2 |^ 2) * 2
by NEWTON:6
.=
8
by A6
;
A8: 2 |^ 4 =
2 |^ (3 + 1)
.=
(2 |^ 3) * 2
by NEWTON:6
.=
16
by A7
;
A9:
2 |^ (3 + 4) = 8 * 16
by A8, A7, NEWTON:8;
5 * (2 |^ 7), - 1 are_congruent_mod 641
by A9;
then
(5 * (2 |^ 7)) * (5 * (2 |^ 7)),(- 1) * (- 1) are_congruent_mod 641
by INT_1:18;
then A10:
((5 |^ 2) * (2 |^ 14)) * ((5 |^ 2) * (2 |^ 14)),1 * 1 are_congruent_mod 641
by A1, A2, INT_1:18;
((5 |^ 4) + (2 |^ 4)) - (2 |^ 4),0 - (2 |^ 4) are_congruent_mod 641
by A2, A3, A8;
then A11:
- (2 |^ 4),5 |^ 4 are_congruent_mod 641
by INT_1:14;
2 |^ 28,2 |^ 28 are_congruent_mod 641
by INT_1:11;
then
(- (2 |^ 4)) * (2 |^ 28),(5 |^ 4) * (2 |^ 28) are_congruent_mod 641
by A11, INT_1:18;
then A12:
- (2 |^ 32),1 are_congruent_mod 641
by A3, A4, A5, A10, INT_1:15;
- 1, - 1 are_congruent_mod 641
by INT_1:11;
then A13:
(- 1) * (- (2 |^ 32)),(- 1) * 1 are_congruent_mod 641
by A12, INT_1:18;
A14:
(5 * (2 |^ 7)) + 1 = 641
by A9;
2 |^ (4 + 1) = 16 * 2
by A8, NEWTON:6;
then A15:
Fermat 5 = (2 |^ 32) + 1
by PEPIN:def 3;
5 * (2 |^ 7) < (2 |^ 3) * (2 |^ 7)
by A7, XREAL_1:68;
then A16:
5 * (2 |^ 7) < 2 |^ (3 + 7)
by NEWTON:8;
not 2 is trivial
;
then
2 |^ 10 < 2 |^ 32
by Th2;
then
5 * (2 |^ 7) < 2 |^ 32
by A16, XXREAL_0:2;
then
641 < (2 |^ 32) + 1
by A14, XREAL_1:6;
hence
not Fermat 5 is prime
by A15, A13; verum