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