Metamath Proof Explorer


Table of Contents - 21.47.12.2. Mersenne primes

"In mathematics, a Mersenne prime is a prime number that is one less than a power of two. That is, it is a prime number of the form Mn = 2^n-1 for some integer n. They are named after Marin Mersenne ... If n is a composite number then so is 2^n-1. Therefore, an equivalent definition of the Mersenne primes is that they are the prime numbers of the form Mp = 2^p-1 for some prime p.", see Wikipedia "Mersenne prime", 16-Aug-2021, https://en.wikipedia.org/wiki/Mersenne_prime. See also definition in [ApostolNT] p. 4.

This means that if Mn = 2^n-1 is prime, than n must be prime, too, see mersenne. The reverse direction is not generally valid: If p is prime, then Mp = 2^p-1 needs not be prime, e.g. M11 = 2047 = 23 x 89, see m11nprm. This is an example of sgprmdvdsmersenne, stating that if p with p = 3 modulo 4 (here 11) and q=2p+1 (here 23) are prime, then q divides Mp.

"In number theory, a prime number p is a Sophie Germain prime if 2p+1 is also prime. The number 2p+1 associated with a Sophie Germain prime is called a safe prime.", see Wikipedia "Safe and Sophie Germain primes", 21-Aug-2021, https://en.wikipedia.org/wiki/Safe_and_Sophie_Germain_primes. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne, it is shown that if a safe prime q is congruent to 7 modulo 8, then it is a divisor of the Mersenne number with its matching Sophie Germain prime as exponent.

The main result of this section, however, is the formal proof of a theorem of S. Ligh and L. Neal in "A note on Mersenne numbers", see lighneal.

  1. m2prm
  2. m3prm
  3. flsqrt
  4. flsqrt5
  5. 3ndvds4
  6. 139prmALT
  7. 31prm
  8. m5prm
  9. 127prm
  10. m7prm
  11. m11nprm
  12. mod42tp1mod8
  13. sfprmdvdsmersenne
  14. sgprmdvdsmersenne
  15. lighneallem1
  16. lighneallem2
  17. lighneallem3
  18. lighneallem4a
  19. lighneallem4b
  20. lighneallem4
  21. lighneal