A0:
2 is Prime
by XPRIMES1:2;
A3:
3 is Prime
by XPRIMES1:3;
A1: card (PrimeDivisors 8) =
card {2}
by A0, NUMBER12:50, POWER:61
.=
1
by CARD_2:42
;
A2: card (PrimeDivisors (8 + 1)) =
card (PrimeDivisors (3 * 3))
.=
card (PrimeDivisors (3 |^ 2))
by NEWTON:81
.=
card {3}
by A3, NUMBER12:50
.=
1
by CARD_2:42
;
2 divides 2 * 4
;
then A4:
8 is not mersenne Prime
by INT_2:def 4;
3 * 3 is not Prime
;
hence
( card (PrimeDivisors 8) = 1 & card (PrimeDivisors (8 + 1)) = 1 & 8 is not mersenne Prime & 8 + 1 is not fermat Prime )
by A1, A2, A4; verum