assume A1: ( card (PrimeDivisors 5) = 1 & card (PrimeDivisors (5 + 1)) = 1 ) ; :: thesis: ( 5 is mersenne Prime or 5 + 1 is fermat Prime )
card (PrimeDivisors (2 * 3)) = 2 by XPRIMES1:2, XPRIMES1:3, Moshe1;
hence ( 5 is mersenne Prime or 5 + 1 is fermat Prime ) by A1; :: thesis: verum