This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trirecip

Description: The sum of the reciprocals of the triangle numbers converge to two. This is Metamath 100 proof #42. (Contributed by Scott Fenton, 23-Apr-2014) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion trirecip Σ 𝑘 ∈ ℕ ( 2 / ( 𝑘 · ( 𝑘 + 1 ) ) ) = 2

Proof

Step Hyp Ref Expression
1 2cnd ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℂ )
2 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
3 nnmulcl ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝑘 · ( 𝑘 + 1 ) ) ∈ ℕ )
4 2 3 mpdan ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 · ( 𝑘 + 1 ) ) ∈ ℕ )
5 4 nncnd ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 · ( 𝑘 + 1 ) ) ∈ ℂ )
6 4 nnne0d ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 · ( 𝑘 + 1 ) ) ≠ 0 )
7 1 5 6 divrecd ⊢ ( 𝑘 ∈ ℕ → ( 2 / ( 𝑘 · ( 𝑘 + 1 ) ) ) = ( 2 · ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ) )
8 7 sumeq2i ⊢ Σ 𝑘 ∈ ℕ ( 2 / ( 𝑘 · ( 𝑘 + 1 ) ) ) = Σ 𝑘 ∈ ℕ ( 2 · ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) )
9 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
10 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
11 id ⊢ ( 𝑛 = 𝑘 → 𝑛 = 𝑘 )
12 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 + 1 ) = ( 𝑘 + 1 ) )
13 11 12 oveq12d ⊢ ( 𝑛 = 𝑘 → ( 𝑛 · ( 𝑛 + 1 ) ) = ( 𝑘 · ( 𝑘 + 1 ) ) )
14 13 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) )
15 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
16 ovex ⊢ ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ∈ V
17 14 15 16 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) )
18 17 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) )
19 4 nnrecred ⊢ ( 𝑘 ∈ ℕ → ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ∈ ℝ )
20 19 recnd ⊢ ( 𝑘 ∈ ℕ → ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ∈ ℂ )
21 20 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ∈ ℂ )
22 15 trireciplem ⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ) ⇝ 1
23 22 a1i ⊢ ( ⊤ → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ) ⇝ 1 )
24 climrel ⊢ Rel ⇝
25 24 releldmi ⊢ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ) ⇝ 1 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ) ∈ dom ⇝ )
26 23 25 syl ⊢ ( ⊤ → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ) ∈ dom ⇝ )
27 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
28 9 10 18 21 26 27 isummulc2 ⊢ ( ⊤ → ( 2 · Σ 𝑘 ∈ ℕ ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ) = Σ 𝑘 ∈ ℕ ( 2 · ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ) )
29 9 10 18 21 23 isumclim ⊢ ( ⊤ → Σ 𝑘 ∈ ℕ ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) = 1 )
30 29 oveq2d ⊢ ( ⊤ → ( 2 · Σ 𝑘 ∈ ℕ ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ) = ( 2 · 1 ) )
31 28 30 eqtr3d ⊢ ( ⊤ → Σ 𝑘 ∈ ℕ ( 2 · ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ) = ( 2 · 1 ) )
32 31 mptru ⊢ Σ 𝑘 ∈ ℕ ( 2 · ( 1 / ( 𝑘 · ( 𝑘 + 1 ) ) ) ) = ( 2 · 1 )
33 2t1e2 ⊢ ( 2 · 1 ) = 2
34 8 32 33 3eqtri ⊢ Σ 𝑘 ∈ ℕ ( 2 / ( 𝑘 · ( 𝑘 + 1 ) ) ) = 2