let m be Nat; :: thesis: ( m <= 4 implies Fermat m divides (2 |^ 32) - 1 )
assume m <= 4 ; :: thesis: Fermat m divides (2 |^ 32) - 1
then A2: not not m = 0 & ... & not m = 4 ;
A3: 2 |^ (1 + 1) = (2 |^ 1) * 2 by NEWTON:6;
then A4: 2 |^ (2 + 1) = 4 * 2 by NEWTON:6;
A5: 2 |^ (2 + 2) = 4 * 4 by A3, NEWTON:8;
A6: ( 2 |^ (2 |^ 0) = 2 |^ 1 & 2 |^ 1 = 2 ) by NEWTON:4;
A7: (2 |^ (2 |^ 1)) |^ (2 * 8) = 2 |^ (2 * (2 * 8)) by NEWTON:9;
A8: (2 |^ (2 |^ 2)) |^ (2 * 4) = 2 |^ (4 * (2 * 4)) by A3, NEWTON:9;
A9: (2 |^ (2 |^ 3)) |^ (2 * 2) = 2 |^ (8 * (2 * 2)) by A4, NEWTON:9;
A10: (2 |^ (2 |^ 4)) |^ (1 * 2) = 2 |^ (16 * (1 * 2)) by A5, NEWTON:9;

per cases ( m = 0 or m = 1 or m = 2 or m = 3 or m = 4 ) by A2;

suppose m = 0 ; :: thesis: Fermat m divides (2 |^ 32) - 1

then Fermat m = (2 |^ (2 |^ 0)) + 1 by PEPIN:def 3;
then Fermat m divides ((2 |^ (2 |^ 0)) |^ (2 * 16)) - (1 |^ (2 * 16)) by NEWTON01:36;
hence Fermat m divides (2 |^ 32) - 1 by A6; :: thesis: verum

end;

suppose m = 1 ; :: thesis: Fermat m divides (2 |^ 32) - 1

then Fermat m = (2 |^ (2 |^ 1)) + 1 by PEPIN:def 3;
then Fermat m divides ((2 |^ (2 |^ 1)) |^ (2 * 8)) - (1 |^ (2 * 8)) by NEWTON01:36;
hence Fermat m divides (2 |^ 32) - 1 by A7; :: thesis: verum

end;

suppose m = 2 ; :: thesis: Fermat m divides (2 |^ 32) - 1

then Fermat m = (2 |^ (2 |^ 2)) + 1 by PEPIN:def 3;
then Fermat m divides ((2 |^ (2 |^ 2)) |^ (2 * 4)) - (1 |^ (2 * 4)) by NEWTON01:36;
hence Fermat m divides (2 |^ 32) - 1 by A8; :: thesis: verum

end;

suppose m = 3 ; :: thesis: Fermat m divides (2 |^ 32) - 1

then Fermat m = (2 |^ (2 |^ 3)) + 1 by PEPIN:def 3;
then Fermat m divides ((2 |^ (2 |^ 3)) |^ (2 * 2)) - (1 |^ (2 * 2)) by NEWTON01:36;
hence Fermat m divides (2 |^ 32) - 1 by A9; :: thesis: verum

end;

suppose m = 4 ; :: thesis: Fermat m divides (2 |^ 32) - 1

then Fermat m = (2 |^ (2 |^ 4)) + 1 by PEPIN:def 3;
then Fermat m divides ((2 |^ (2 |^ 4)) |^ (1 * 2)) - (1 |^ (1 * 2)) by NEWTON01:36;
hence Fermat m divides (2 |^ 32) - 1 by A10; :: thesis: verum

end;

end;