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.odd_mersenne_succ (k : ℕ) : ¬2 ∣ mersenne (k + 1)

theorem Theorems100.Nat.sigma_two_pow_eq_mersenne_succ (k : ℕ) : ↑(Nat.ArithmeticFunction.sigma 1) (2 ^ k) = mersenne (k + 1)

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

Euclid's theorem that Mersenne primes induce perfect numbers

theorem Theorems100.Nat.ne_zero_of_prime_mersenne (k : ℕ) (pr : Nat.Prime (mersenne (k + 1))) : k ≠ 0

theorem Theorems100.Nat.even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : Nat.Prime (mersenne (k + 1))) : Even (2 ^ k * mersenne (k + 1))

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 : Nat.Perfect n) : ∃ 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 ∧ Nat.Perfect n ↔ ∃ k, Nat.Prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)

The Euclid-Euler theorem characterizing even perfect numbers