let n be fermat Prime; ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n - 1)) = 1 )
consider k being Nat such that
A1:
n = Fermat k
by FerDef;
A2:
Fermat k = (2 |^ (2 |^ k)) + 1
by PEPIN:def 3;
2 |^ k >= 2 |^ 0
by PREPOWER:93;
then A5:
2 |^ k >= 1
by NEWTON:4;
A4:
n - 1 = 2 |^ (2 |^ k)
by A1, A2;
2 is Prime
by INT_2:28;
then
PrimeDivisors (2 |^ (2 |^ k)) = {2}
by A5, NUMBER12:50;
then T1:
card (PrimeDivisors (n - 1)) = 1
by A4, CARD_2:42;
PrimeDivisors n =
PrimeDivisors (n |^ 1)
.=
{n}
by NUMBER12:50
;
hence
( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n - 1)) = 1 )
by T1, CARD_2:42; verum