Metamath Proof Explorer

Theorem trireciplem

Description: Lemma for trirecip . Show that the sum converges. (Contributed by Scott Fenton, 22-Apr-2014) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Hypothesis trireciplem.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
Assertion trireciplem seq 1 ( + , 𝐹 ) ⇝ 1

Proof

Step Hyp Ref Expression
1 trireciplem.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
2 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
3 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
4 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
5 nnex ⊢ ℕ ∈ V
6 5 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) ∈ V
7 6 a1i ⊢ ( ⊤ → ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) ∈ V )
8 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 + 1 ) = ( 𝑘 + 1 ) )
9 8 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 1 / ( 𝑛 + 1 ) ) = ( 1 / ( 𝑘 + 1 ) ) )
10 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) )
11 ovex ⊢ ( 1 / ( 𝑘 + 1 ) ) ∈ V
12 9 10 11 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝑘 + 1 ) ) )
13 12 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝑘 + 1 ) ) )
14 2 3 4 3 7 13 divcnvshft ⊢ ( ⊤ → ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) ⇝ 0 )
15 seqex ⊢ seq 1 ( + , 𝐹 ) ∈ V
16 15 a1i ⊢ ( ⊤ → seq 1 ( + , 𝐹 ) ∈ V )
17 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
18 17 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
19 18 nnrecred ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 1 / ( 𝑘 + 1 ) ) ∈ ℝ )
20 19 recnd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 1 / ( 𝑘 + 1 ) ) ∈ ℂ )
21 13 20 eqeltrd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) ‘ 𝑘 ) ∈ ℂ )
22 13 oveq2d ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 1 − ( ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) ‘ 𝑘 ) ) = ( 1 − ( 1 / ( 𝑘 + 1 ) ) ) )
23 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ℕ )
24 23 adantl ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 𝑗 ∈ ℕ )
25 24 nncnd ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 𝑗 ∈ ℂ )
26 peano2cn ⊢ ( 𝑗 ∈ ℂ → ( 𝑗 + 1 ) ∈ ℂ )
27 25 26 syl ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 + 1 ) ∈ ℂ )
28 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
29 24 28 syl ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 + 1 ) ∈ ℕ )
30 24 29 nnmulcld ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 · ( 𝑗 + 1 ) ) ∈ ℕ )
31 30 nncnd ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 · ( 𝑗 + 1 ) ) ∈ ℂ )
32 30 nnne0d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 · ( 𝑗 + 1 ) ) ≠ 0 )
33 27 25 31 32 divsubdird ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 𝑗 + 1 ) − 𝑗 ) / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( ( ( 𝑗 + 1 ) / ( 𝑗 · ( 𝑗 + 1 ) ) ) − ( 𝑗 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) )
34 ax-1cn ⊢ 1 ∈ ℂ
35 pncan2 ⊢ ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑗 + 1 ) − 𝑗 ) = 1 )
36 25 34 35 sylancl ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑗 + 1 ) − 𝑗 ) = 1 )
37 36 oveq1d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 𝑗 + 1 ) − 𝑗 ) / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
38 27 mulridd ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑗 + 1 ) · 1 ) = ( 𝑗 + 1 ) )
39 27 25 mulcomd ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑗 + 1 ) · 𝑗 ) = ( 𝑗 · ( 𝑗 + 1 ) ) )
40 38 39 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 𝑗 + 1 ) · 1 ) / ( ( 𝑗 + 1 ) · 𝑗 ) ) = ( ( 𝑗 + 1 ) / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
41 1cnd ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 1 ∈ ℂ )
42 24 nnne0d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 𝑗 ≠ 0 )
43 29 nnne0d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 + 1 ) ≠ 0 )
44 41 25 27 42 43 divcan5d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 𝑗 + 1 ) · 1 ) / ( ( 𝑗 + 1 ) · 𝑗 ) ) = ( 1 / 𝑗 ) )
45 40 44 eqtr3d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑗 + 1 ) / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( 1 / 𝑗 ) )
46 25 mulridd ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 · 1 ) = 𝑗 )
47 46 oveq1d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑗 · 1 ) / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( 𝑗 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
48 41 27 25 43 42 divcan5d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑗 · 1 ) / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( 1 / ( 𝑗 + 1 ) ) )
49 47 48 eqtr3d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝑗 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( 1 / ( 𝑗 + 1 ) ) )
50 45 49 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 𝑗 + 1 ) / ( 𝑗 · ( 𝑗 + 1 ) ) ) − ( 𝑗 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ) = ( ( 1 / 𝑗 ) − ( 1 / ( 𝑗 + 1 ) ) ) )
51 33 37 50 3eqtr3d ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( ( 1 / 𝑗 ) − ( 1 / ( 𝑗 + 1 ) ) ) )
52 51 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( ( 1 / 𝑗 ) − ( 1 / ( 𝑗 + 1 ) ) ) )
53 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 1 / 𝑛 ) = ( 1 / 𝑗 ) )
54 oveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 1 / 𝑛 ) = ( 1 / ( 𝑗 + 1 ) ) )
55 oveq2 ⊢ ( 𝑛 = 1 → ( 1 / 𝑛 ) = ( 1 / 1 ) )
56 1div1e1 ⊢ ( 1 / 1 ) = 1
57 55 56 eqtrdi ⊢ ( 𝑛 = 1 → ( 1 / 𝑛 ) = 1 )
58 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 1 / 𝑛 ) = ( 1 / ( 𝑘 + 1 ) ) )
59 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
60 59 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
61 18 2 eleqtrdi ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
62 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) → 𝑛 ∈ ℕ )
63 62 adantl ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ) → 𝑛 ∈ ℕ )
64 63 nnrecred ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
65 64 recnd ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
66 53 54 57 58 60 61 65 telfsum ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( ( 1 / 𝑗 ) − ( 1 / ( 𝑗 + 1 ) ) ) = ( 1 − ( 1 / ( 𝑘 + 1 ) ) ) )
67 52 66 eqtrd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( 1 − ( 1 / ( 𝑘 + 1 ) ) ) )
68 id ⊢ ( 𝑛 = 𝑗 → 𝑛 = 𝑗 )
69 oveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 + 1 ) = ( 𝑗 + 1 ) )
70 68 69 oveq12d ⊢ ( 𝑛 = 𝑗 → ( 𝑛 · ( 𝑛 + 1 ) ) = ( 𝑗 · ( 𝑗 + 1 ) ) )
71 70 oveq2d ⊢ ( 𝑛 = 𝑗 → ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
72 ovex ⊢ ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ V
73 71 1 72 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( 𝐹 ‘ 𝑗 ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
74 24 73 syl ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) )
75 simpr ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
76 75 2 eleqtrdi ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
77 30 nnrecred ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℝ )
78 77 recnd ⊢ ( ( ( ⊤ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) ∈ ℂ )
79 74 76 78 fsumser ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) ( 1 / ( 𝑗 · ( 𝑗 + 1 ) ) ) = ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) )
80 22 67 79 3eqtr2rd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) = ( 1 − ( ( 𝑛 ∈ ℕ ↦ ( 1 / ( 𝑛 + 1 ) ) ) ‘ 𝑘 ) ) )
81 2 3 14 4 16 21 80 climsubc2 ⊢ ( ⊤ → seq 1 ( + , 𝐹 ) ⇝ ( 1 − 0 ) )
82 81 mptru ⊢ seq 1 ( + , 𝐹 ) ⇝ ( 1 − 0 )
83 1m0e1 ⊢ ( 1 − 0 ) = 1
84 82 83 breqtri ⊢ seq 1 ( + , 𝐹 ) ⇝ 1