reconsider p = Fermat l as Nat ;
set k = 1;
set n = 2 |^ l;
A3:
2 |^ (2 |^ l) > 2 |^ l
by NEWTON:86;
(2 |^ l) + 1 > 0 + 1
by XREAL_1:6;
then
2 |^ l >= 1
by NAT_1:13;
then A1:
2 |^ (2 |^ l) > 1
by A3, XXREAL_0:2;
A2:
(2 * 0) + 1 = 1
;
p = (1 * (2 |^ (2 |^ l))) + 1
by PEPIN:def 3;
hence
Fermat l is Proth
by A1, A2; verum