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 ${⊢}{F}=\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)$
Assertion trireciplem ${⊢}seq1\left(+,{F}\right)⇝1$

Proof

Step Hyp Ref Expression
1 trireciplem.1 ${⊢}{F}=\left({n}\in ℕ⟼\frac{1}{{n}\left({n}+1\right)}\right)$
2 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
3 1zzd ${⊢}\top \to 1\in ℤ$
4 1cnd ${⊢}\top \to 1\in ℂ$
5 nnex ${⊢}ℕ\in \mathrm{V}$
6 5 mptex ${⊢}\left({n}\in ℕ⟼\frac{1}{{n}+1}\right)\in \mathrm{V}$
7 6 a1i ${⊢}\top \to \left({n}\in ℕ⟼\frac{1}{{n}+1}\right)\in \mathrm{V}$
8 oveq1 ${⊢}{n}={k}\to {n}+1={k}+1$
9 8 oveq2d ${⊢}{n}={k}\to \frac{1}{{n}+1}=\frac{1}{{k}+1}$
10 eqid ${⊢}\left({n}\in ℕ⟼\frac{1}{{n}+1}\right)=\left({n}\in ℕ⟼\frac{1}{{n}+1}\right)$
11 ovex ${⊢}\frac{1}{{k}+1}\in \mathrm{V}$
12 9 10 11 fvmpt ${⊢}{k}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{{n}+1}\right)\left({k}\right)=\frac{1}{{k}+1}$
13 12 adantl ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \left({n}\in ℕ⟼\frac{1}{{n}+1}\right)\left({k}\right)=\frac{1}{{k}+1}$
14 2 3 4 3 7 13 divcnvshft ${⊢}\top \to \left({n}\in ℕ⟼\frac{1}{{n}+1}\right)⇝0$
15 seqex ${⊢}seq1\left(+,{F}\right)\in \mathrm{V}$
16 15 a1i ${⊢}\top \to seq1\left(+,{F}\right)\in \mathrm{V}$
17 peano2nn ${⊢}{k}\in ℕ\to {k}+1\in ℕ$
18 17 adantl ${⊢}\left(\top \wedge {k}\in ℕ\right)\to {k}+1\in ℕ$
19 18 nnrecred ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \frac{1}{{k}+1}\in ℝ$
20 19 recnd ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \frac{1}{{k}+1}\in ℂ$
21 13 20 eqeltrd ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \left({n}\in ℕ⟼\frac{1}{{n}+1}\right)\left({k}\right)\in ℂ$
22 13 oveq2d ${⊢}\left(\top \wedge {k}\in ℕ\right)\to 1-\left({n}\in ℕ⟼\frac{1}{{n}+1}\right)\left({k}\right)=1-\left(\frac{1}{{k}+1}\right)$
23 elfznn ${⊢}{j}\in \left(1\dots {k}\right)\to {j}\in ℕ$
24 23 adantl ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}\in ℕ$
25 24 nncnd ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}\in ℂ$
26 peano2cn ${⊢}{j}\in ℂ\to {j}+1\in ℂ$
27 25 26 syl ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}+1\in ℂ$
28 peano2nn ${⊢}{j}\in ℕ\to {j}+1\in ℕ$
29 24 28 syl ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}+1\in ℕ$
30 24 29 nnmulcld ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}\left({j}+1\right)\in ℕ$
31 30 nncnd ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}\left({j}+1\right)\in ℂ$
32 30 nnne0d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}\left({j}+1\right)\ne 0$
33 27 25 31 32 divsubdird ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{{j}+1-{j}}{{j}\left({j}+1\right)}=\left(\frac{{j}+1}{{j}\left({j}+1\right)}\right)-\left(\frac{{j}}{{j}\left({j}+1\right)}\right)$
34 ax-1cn ${⊢}1\in ℂ$
35 pncan2 ${⊢}\left({j}\in ℂ\wedge 1\in ℂ\right)\to {j}+1-{j}=1$
36 25 34 35 sylancl ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}+1-{j}=1$
37 36 oveq1d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{{j}+1-{j}}{{j}\left({j}+1\right)}=\frac{1}{{j}\left({j}+1\right)}$
38 27 mulid1d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \left({j}+1\right)\cdot 1={j}+1$
39 27 25 mulcomd ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \left({j}+1\right){j}={j}\left({j}+1\right)$
40 38 39 oveq12d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{\left({j}+1\right)\cdot 1}{\left({j}+1\right){j}}=\frac{{j}+1}{{j}\left({j}+1\right)}$
41 1cnd ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to 1\in ℂ$
42 24 nnne0d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}\ne 0$
43 29 nnne0d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}+1\ne 0$
44 41 25 27 42 43 divcan5d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{\left({j}+1\right)\cdot 1}{\left({j}+1\right){j}}=\frac{1}{{j}}$
45 40 44 eqtr3d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{{j}+1}{{j}\left({j}+1\right)}=\frac{1}{{j}}$
46 25 mulid1d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {j}\cdot 1={j}$
47 46 oveq1d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{{j}\cdot 1}{{j}\left({j}+1\right)}=\frac{{j}}{{j}\left({j}+1\right)}$
48 41 27 25 43 42 divcan5d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{{j}\cdot 1}{{j}\left({j}+1\right)}=\frac{1}{{j}+1}$
49 47 48 eqtr3d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{{j}}{{j}\left({j}+1\right)}=\frac{1}{{j}+1}$
50 45 49 oveq12d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \left(\frac{{j}+1}{{j}\left({j}+1\right)}\right)-\left(\frac{{j}}{{j}\left({j}+1\right)}\right)=\left(\frac{1}{{j}}\right)-\left(\frac{1}{{j}+1}\right)$
51 33 37 50 3eqtr3d ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{1}{{j}\left({j}+1\right)}=\left(\frac{1}{{j}}\right)-\left(\frac{1}{{j}+1}\right)$
52 51 sumeq2dv ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \sum _{{j}=1}^{{k}}\left(\frac{1}{{j}\left({j}+1\right)}\right)=\sum _{{j}=1}^{{k}}\left(\left(\frac{1}{{j}}\right)-\left(\frac{1}{{j}+1}\right)\right)$
53 oveq2 ${⊢}{n}={j}\to \frac{1}{{n}}=\frac{1}{{j}}$
54 oveq2 ${⊢}{n}={j}+1\to \frac{1}{{n}}=\frac{1}{{j}+1}$
55 oveq2 ${⊢}{n}=1\to \frac{1}{{n}}=\frac{1}{1}$
56 1div1e1 ${⊢}\frac{1}{1}=1$
57 55 56 syl6eq ${⊢}{n}=1\to \frac{1}{{n}}=1$
58 oveq2 ${⊢}{n}={k}+1\to \frac{1}{{n}}=\frac{1}{{k}+1}$
59 nnz ${⊢}{k}\in ℕ\to {k}\in ℤ$
60 59 adantl ${⊢}\left(\top \wedge {k}\in ℕ\right)\to {k}\in ℤ$
61 18 2 eleqtrdi ${⊢}\left(\top \wedge {k}\in ℕ\right)\to {k}+1\in {ℤ}_{\ge 1}$
62 elfznn ${⊢}{n}\in \left(1\dots {k}+1\right)\to {n}\in ℕ$
63 62 adantl ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {n}\in \left(1\dots {k}+1\right)\right)\to {n}\in ℕ$
64 63 nnrecred ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {n}\in \left(1\dots {k}+1\right)\right)\to \frac{1}{{n}}\in ℝ$
65 64 recnd ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {n}\in \left(1\dots {k}+1\right)\right)\to \frac{1}{{n}}\in ℂ$
66 53 54 57 58 60 61 65 telfsum ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \sum _{{j}=1}^{{k}}\left(\left(\frac{1}{{j}}\right)-\left(\frac{1}{{j}+1}\right)\right)=1-\left(\frac{1}{{k}+1}\right)$
67 52 66 eqtrd ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \sum _{{j}=1}^{{k}}\left(\frac{1}{{j}\left({j}+1\right)}\right)=1-\left(\frac{1}{{k}+1}\right)$
68 id ${⊢}{n}={j}\to {n}={j}$
69 oveq1 ${⊢}{n}={j}\to {n}+1={j}+1$
70 68 69 oveq12d ${⊢}{n}={j}\to {n}\left({n}+1\right)={j}\left({j}+1\right)$
71 70 oveq2d ${⊢}{n}={j}\to \frac{1}{{n}\left({n}+1\right)}=\frac{1}{{j}\left({j}+1\right)}$
72 ovex ${⊢}\frac{1}{{j}\left({j}+1\right)}\in \mathrm{V}$
73 71 1 72 fvmpt ${⊢}{j}\in ℕ\to {F}\left({j}\right)=\frac{1}{{j}\left({j}+1\right)}$
74 24 73 syl ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to {F}\left({j}\right)=\frac{1}{{j}\left({j}+1\right)}$
75 simpr ${⊢}\left(\top \wedge {k}\in ℕ\right)\to {k}\in ℕ$
76 75 2 eleqtrdi ${⊢}\left(\top \wedge {k}\in ℕ\right)\to {k}\in {ℤ}_{\ge 1}$
77 30 nnrecred ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{1}{{j}\left({j}+1\right)}\in ℝ$
78 77 recnd ${⊢}\left(\left(\top \wedge {k}\in ℕ\right)\wedge {j}\in \left(1\dots {k}\right)\right)\to \frac{1}{{j}\left({j}+1\right)}\in ℂ$
79 74 76 78 fsumser ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \sum _{{j}=1}^{{k}}\left(\frac{1}{{j}\left({j}+1\right)}\right)=seq1\left(+,{F}\right)\left({k}\right)$
80 22 67 79 3eqtr2rd ${⊢}\left(\top \wedge {k}\in ℕ\right)\to seq1\left(+,{F}\right)\left({k}\right)=1-\left({n}\in ℕ⟼\frac{1}{{n}+1}\right)\left({k}\right)$
81 2 3 14 4 16 21 80 climsubc2 ${⊢}\top \to seq1\left(+,{F}\right)⇝\left(1-0\right)$
82 81 mptru ${⊢}seq1\left(+,{F}\right)⇝\left(1-0\right)$
83 1m0e1 ${⊢}1-0=1$
84 82 83 breqtri ${⊢}seq1\left(+,{F}\right)⇝1$