# 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 ${⊢}\sum _{{k}\in ℕ}\left(\frac{2}{{k}\left({k}+1\right)}\right)=2$

### Proof

Step Hyp Ref Expression
1 2cnd ${⊢}{k}\in ℕ\to 2\in ℂ$
2 peano2nn ${⊢}{k}\in ℕ\to {k}+1\in ℕ$
3 nnmulcl ${⊢}\left({k}\in ℕ\wedge {k}+1\in ℕ\right)\to {k}\left({k}+1\right)\in ℕ$
4 2 3 mpdan ${⊢}{k}\in ℕ\to {k}\left({k}+1\right)\in ℕ$
5 4 nncnd ${⊢}{k}\in ℕ\to {k}\left({k}+1\right)\in ℂ$
6 4 nnne0d ${⊢}{k}\in ℕ\to {k}\left({k}+1\right)\ne 0$
7 1 5 6 divrecd ${⊢}{k}\in ℕ\to \frac{2}{{k}\left({k}+1\right)}=2\left(\frac{1}{{k}\left({k}+1\right)}\right)$
8 7 sumeq2i ${⊢}\sum _{{k}\in ℕ}\left(\frac{2}{{k}\left({k}+1\right)}\right)=\sum _{{k}\in ℕ}2\left(\frac{1}{{k}\left({k}+1\right)}\right)$
9 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
10 1zzd ${⊢}\top \to 1\in ℤ$
11 id ${⊢}{n}={k}\to {n}={k}$
12 oveq1 ${⊢}{n}={k}\to {n}+1={k}+1$
13 11 12 oveq12d ${⊢}{n}={k}\to {n}\left({n}+1\right)={k}\left({k}+1\right)$
14 13 oveq2d ${⊢}{n}={k}\to \frac{1}{{n}\left({n}+1\right)}=\frac{1}{{k}\left({k}+1\right)}$
15 eqid ${⊢}\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)=\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)$
16 ovex ${⊢}\frac{1}{{k}\left({k}+1\right)}\in \mathrm{V}$
17 14 15 16 fvmpt ${⊢}{k}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)\left({k}\right)=\frac{1}{{k}\left({k}+1\right)}$
18 17 adantl ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)\left({k}\right)=\frac{1}{{k}\left({k}+1\right)}$
19 4 nnrecred ${⊢}{k}\in ℕ\to \frac{1}{{k}\left({k}+1\right)}\in ℝ$
20 19 recnd ${⊢}{k}\in ℕ\to \frac{1}{{k}\left({k}+1\right)}\in ℂ$
21 20 adantl ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \frac{1}{{k}\left({k}+1\right)}\in ℂ$
22 15 trireciplem ${⊢}seq1\left(+,\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)\right)⇝1$
23 22 a1i ${⊢}\top \to seq1\left(+,\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)\right)⇝1$
24 climrel ${⊢}\mathrm{Rel}⇝$
25 24 releldmi ${⊢}seq1\left(+,\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)\right)⇝1\to seq1\left(+,\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)\right)\in \mathrm{dom}⇝$
26 23 25 syl ${⊢}\top \to seq1\left(+,\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)\right)\in \mathrm{dom}⇝$
27 2cnd ${⊢}\top \to 2\in ℂ$
28 9 10 18 21 26 27 isummulc2 ${⊢}\top \to 2\sum _{{k}\in ℕ}\left(\frac{1}{{k}\left({k}+1\right)}\right)=\sum _{{k}\in ℕ}2\left(\frac{1}{{k}\left({k}+1\right)}\right)$
29 9 10 18 21 23 isumclim ${⊢}\top \to \sum _{{k}\in ℕ}\left(\frac{1}{{k}\left({k}+1\right)}\right)=1$
30 29 oveq2d ${⊢}\top \to 2\sum _{{k}\in ℕ}\left(\frac{1}{{k}\left({k}+1\right)}\right)=2\cdot 1$
31 28 30 eqtr3d ${⊢}\top \to \sum _{{k}\in ℕ}2\left(\frac{1}{{k}\left({k}+1\right)}\right)=2\cdot 1$
32 31 mptru ${⊢}\sum _{{k}\in ℕ}2\left(\frac{1}{{k}\left({k}+1\right)}\right)=2\cdot 1$
33 2t1e2 ${⊢}2\cdot 1=2$
34 8 32 33 3eqtri ${⊢}\sum _{{k}\in ℕ}\left(\frac{2}{{k}\left({k}+1\right)}\right)=2$