theorem :: NUMBER18:61

( { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } is finite implies Mersenne_Primes \/ Fermat_Primes is finite )