let m be Nat; ( m >= 1 & Fermat m is Prime implies ( card (PrimeDivisors (Fermat m)) = 1 & card (PrimeDivisors ((Fermat m) - 1)) = 1 ) )
A0:
2 is Prime
by INT_2:28;
assume
m >= 1
; ( not Fermat m is Prime or ( card (PrimeDivisors (Fermat m)) = 1 & card (PrimeDivisors ((Fermat m) - 1)) = 1 ) )
then
2 |^ m >= 2 |^ 1
by PREPOWER:93;
then A2:
2 |^ m >= 1
by XXREAL_0:2;
assume ZZ:
Fermat m is Prime
; ( card (PrimeDivisors (Fermat m)) = 1 & card (PrimeDivisors ((Fermat m) - 1)) = 1 )
Fermat m = (2 |^ (2 |^ m)) + 1
by PEPIN:def 3;
then
PrimeDivisors ((Fermat m) - 1) = {2}
by A0, A2, NUMBER12:50;
then T1:
card (PrimeDivisors ((Fermat m) - 1)) = 1
by CARD_2:42;
PrimeDivisors (Fermat m) =
PrimeDivisors ((Fermat m) |^ 1)
.=
{(Fermat m)}
by ZZ, NUMBER12:50
;
hence
( card (PrimeDivisors (Fermat m)) = 1 & card (PrimeDivisors ((Fermat m) - 1)) = 1 )
by T1, CARD_2:42; verum