# Perfect Numbers #

This file proves Theorem 70 from the 100 Theorems List.

The theorem characterizes even perfect numbers.

Euclid proved that if 2 ^ (k + 1) - 1 is prime (these primes are known as Mersenne primes), then 2 ^ k * 2 ^ (k + 1) - 1 is perfect.

Euler proved the converse, that if n is even and perfect, then there exists k such that n = 2 ^ k * 2 ^ (k + 1) - 1 and 2 ^ (k + 1) - 1 is prime.

## References #

https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem

theorem Theorems100.Nat.perfect_two_pow_mul_mersenne_of_prime (k : ) (pr : Nat.Prime (mersenne (k + 1))) :
(2 ^ k * mersenne (k + 1)).Perfect

Euclid's theorem that Mersenne primes induce perfect numbers

theorem Theorems100.Nat.eq_two_pow_mul_odd {n : } (hpos : 0 < n) :
∃ (k : ) (m : ), n = 2 ^ k * m ¬Even m
theorem Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect {n : } (ev : Even n) (perf : n.Perfect) :
∃ (k : ), Nat.Prime (mersenne (k + 1)) n = 2 ^ k * mersenne (k + 1)

Perfect Number Theorem: Euler's theorem that even perfect numbers can be factored as a power of two times a Mersenne prime.

theorem Theorems100.Nat.even_and_perfect_iff {n : } :
Even n n.Perfect ∃ (k : ), Nat.Prime (mersenne (k + 1)) n = 2 ^ k * mersenne (k + 1)

The Euclid-Euler theorem characterizing even perfect numbers