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	⊢ Σ 𝑘 ∈ ℕ ( 𝑘 ↑ - 2 ) = ( ( π ↑ 2 ) / 6 )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑚 = 𝑛 → ( 2 · 𝑚 ) = ( 2 · 𝑛 ) )
2	1	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( 2 · 𝑚 ) + 1 ) = ( ( 2 · 𝑛 ) + 1 ) )
3	2	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
4	3	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
5		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 ↑ - 2 ) = ( 𝑛 ↑ - 2 ) )
6	5	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ ( 𝑚 ↑ - 2 ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) )
7		seqeq3	⊢ ( ( 𝑚 ∈ ℕ ↦ ( 𝑚 ↑ - 2 ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚 ↑ - 2 ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) ) )
8	6 7	ax-mp	⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚 ↑ - 2 ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) )
9		eqid	⊢ ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) ) = ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) )
10		eqid	⊢ ( ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) ) ∘f · ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { - 2 } ) ∘f · ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) ) ) = ( ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) ) ∘f · ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { - 2 } ) ∘f · ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) ) )
11		eqid	⊢ ( ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) ) ∘f · ( ( ℕ × { 1 } ) ∘f + ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) ) = ( ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) ) ∘f · ( ( ℕ × { 1 } ) ∘f + ( 𝑚 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑚 ) + 1 ) ) ) ) )
12	4 8 9 10 11	basellem9	⊢ Σ 𝑘 ∈ ℕ ( 𝑘 ↑ - 2 ) = ( ( π ↑ 2 ) / 6 )