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=π26

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→12⁢m+1=12⁢n+1
4 3 cbvmptv ⊢m∈ℕ⟼12⁢m+1=n∈ℕ⟼12⁢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→seq1+m∈ℕ⟼m−2=seq1+n∈ℕ⟼n−2
8 6 7 ax-mp ⊢seq1+m∈ℕ⟼m−2=seq1+n∈ℕ⟼n−2
9 eqid ⊢ℕ×π26×fℕ×1−fm∈ℕ⟼12⁢m+1=ℕ×π26×fℕ×1−fm∈ℕ⟼12⁢m+1
10 eqid ⊢ℕ×π26×fℕ×1−fm∈ℕ⟼12⁢m+1×fℕ×1+fℕ×−2×fm∈ℕ⟼12⁢m+1=ℕ×π26×fℕ×1−fm∈ℕ⟼12⁢m+1×fℕ×1+fℕ×−2×fm∈ℕ⟼12⁢m+1
11 eqid ⊢ℕ×π26×fℕ×1−fm∈ℕ⟼12⁢m+1×fℕ×1+fm∈ℕ⟼12⁢m+1=ℕ×π26×fℕ×1−fm∈ℕ⟼12⁢m+1×fℕ×1+fm∈ℕ⟼12⁢m+1
12 4 8 9 10 11 basellem9 ⊢∑k∈ℕk−2=π26