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 ⊢ ∑ k ∈ ℕ 2 k ⁢ k + 1 = 2

Proof

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