A1:
2 |^ (1 + 1) = (2 |^ 1) * 2
by NEWTON:6;
then
2 |^ (2 + 1) = 4 * 2
by NEWTON:6;
then A2:
2 |^ (2 + 3) = 4 * 8
by A1, NEWTON:8;
A3:
2 |^ (2 + 2) = 4 * 4
by A1, NEWTON:8;
then
2 |^ (4 + 4) = 16 * 16
by NEWTON:8;
then A4:
2 |^ (8 + 8) = 256 * 256
by NEWTON:8;
A5:
2 |^ (16 + 16) = (2 |^ 16) * (2 |^ 16)
by NEWTON:8;
( Fermat 5 = (2 |^ (2 |^ 5)) + 1 & Fermat 4 = (2 |^ (2 |^ 4)) + 1 )
by PEPIN:def 3;
hence
( Fermat 5 = (2 |^ 32) + 1 & (2 |^ 32) + 1 = 641 * 6700417 & 6700417 > Fermat 4 )
by A3, A2, A4, A5; verum