Metamath Proof Explorer

Theorem basel

Description: The sum of the inverse squares is _pi ^ 2 / 6 . This is commonly known as the Basel problem, with the first known proof attributed to Euler. See http://en.wikipedia.org/wiki/Basel_problem . This particular proof approach is due to Cauchy (1821). This is Metamath 100 proof #14. (Contributed by Mario Carneiro, 30-Jul-2014)

Ref Expression
Assertion basel ⊢ ∑ k ∈ ℕ k − 2 = π 2 6

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ m = n → 2 ⁢ m = 2 ⁢ n
2 1 oveq1d ⊢ m = n → 2 ⁢ m + 1 = 2 ⁢ n + 1
3 2 oveq2d ⊢ m = n → 1 2 ⁢ m + 1 = 1 2 ⁢ n + 1
4 3 cbvmptv ⊢ m ∈ ℕ ⟼ 1 2 ⁢ m + 1 = n ∈ ℕ ⟼ 1 2 ⁢ n + 1
5 oveq1 ⊢ m = n → m − 2 = n − 2
6 5 cbvmptv ⊢ m ∈ ℕ ⟼ m − 2 = n ∈ ℕ ⟼ n − 2
7 seqeq3 ⊢ m ∈ ℕ ⟼ m − 2 = n ∈ ℕ ⟼ n − 2 → seq 1 + m ∈ ℕ ⟼ m − 2 = seq 1 + n ∈ ℕ ⟼ n − 2
8 6 7 ax-mp ⊢ seq 1 + m ∈ ℕ ⟼ m − 2 = seq 1 + n ∈ ℕ ⟼ n − 2
9 eqid ⊢ ℕ × π 2 6 × f ℕ × 1 − f m ∈ ℕ ⟼ 1 2 ⁢ m + 1 = ℕ × π 2 6 × f ℕ × 1 − f m ∈ ℕ ⟼ 1 2 ⁢ m + 1
10 eqid ⊢ ℕ × π 2 6 × f ℕ × 1 − f m ∈ ℕ ⟼ 1 2 ⁢ m + 1 × f ℕ × 1 + f ℕ × − 2 × f m ∈ ℕ ⟼ 1 2 ⁢ m + 1 = ℕ × π 2 6 × f ℕ × 1 − f m ∈ ℕ ⟼ 1 2 ⁢ m + 1 × f ℕ × 1 + f ℕ × − 2 × f m ∈ ℕ ⟼ 1 2 ⁢ m + 1
11 eqid ⊢ ℕ × π 2 6 × f ℕ × 1 − f m ∈ ℕ ⟼ 1 2 ⁢ m + 1 × f ℕ × 1 + f m ∈ ℕ ⟼ 1 2 ⁢ m + 1 = ℕ × π 2 6 × f ℕ × 1 − f m ∈ ℕ ⟼ 1 2 ⁢ m + 1 × f ℕ × 1 + f m ∈ ℕ ⟼ 1 2 ⁢ m + 1
12 4 8 9 10 11 basellem9 ⊢ ∑ k ∈ ℕ k − 2 = π 2 6