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