# Metamath Proof Explorer

## Theorem emcllem5

Description: Lemma for emcl . The partial sums of the series T , which is used in the definition df-em , is in fact the same as G . (Contributed by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypotheses emcl.1 ${⊢}{F}=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}\right)$
emcl.2 ${⊢}{G}=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\right)$
emcl.3 ${⊢}{H}=\left({n}\in ℕ⟼\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)\right)$
emcl.4 ${⊢}{T}=\left({n}\in ℕ⟼\left(\frac{1}{{n}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)\right)$
Assertion emcllem5 ${⊢}{G}=seq1\left(+,{T}\right)$

### Proof

Step Hyp Ref Expression
1 emcl.1 ${⊢}{F}=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}\right)$
2 emcl.2 ${⊢}{G}=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\right)$
3 emcl.3 ${⊢}{H}=\left({n}\in ℕ⟼\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)\right)$
4 emcl.4 ${⊢}{T}=\left({n}\in ℕ⟼\left(\frac{1}{{n}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)\right)$
5 elfznn ${⊢}{m}\in \left(1\dots {n}\right)\to {m}\in ℕ$
6 5 adantl ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to {m}\in ℕ$
7 6 nncnd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to {m}\in ℂ$
8 1cnd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to 1\in ℂ$
9 6 nnne0d ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to {m}\ne 0$
10 7 8 7 9 divdird ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \frac{{m}+1}{{m}}=\left(\frac{{m}}{{m}}\right)+\left(\frac{1}{{m}}\right)$
11 7 9 dividd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \frac{{m}}{{m}}=1$
12 11 oveq1d ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \left(\frac{{m}}{{m}}\right)+\left(\frac{1}{{m}}\right)=1+\left(\frac{1}{{m}}\right)$
13 10 12 eqtrd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \frac{{m}+1}{{m}}=1+\left(\frac{1}{{m}}\right)$
14 13 fveq2d ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \mathrm{log}\left(\frac{{m}+1}{{m}}\right)=\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)$
15 peano2nn ${⊢}{m}\in ℕ\to {m}+1\in ℕ$
16 6 15 syl ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to {m}+1\in ℕ$
17 16 nnrpd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to {m}+1\in {ℝ}^{+}$
18 6 nnrpd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to {m}\in {ℝ}^{+}$
19 17 18 relogdivd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \mathrm{log}\left(\frac{{m}+1}{{m}}\right)=\mathrm{log}\left({m}+1\right)-\mathrm{log}{m}$
20 14 19 eqtr3d ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)=\mathrm{log}\left({m}+1\right)-\mathrm{log}{m}$
21 20 sumeq2dv ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)=\sum _{{m}=1}^{{n}}\left(\mathrm{log}\left({m}+1\right)-\mathrm{log}{m}\right)$
22 fveq2 ${⊢}{x}={m}\to \mathrm{log}{x}=\mathrm{log}{m}$
23 fveq2 ${⊢}{x}={m}+1\to \mathrm{log}{x}=\mathrm{log}\left({m}+1\right)$
24 fveq2 ${⊢}{x}=1\to \mathrm{log}{x}=\mathrm{log}1$
25 fveq2 ${⊢}{x}={n}+1\to \mathrm{log}{x}=\mathrm{log}\left({n}+1\right)$
26 nnz ${⊢}{n}\in ℕ\to {n}\in ℤ$
27 peano2nn ${⊢}{n}\in ℕ\to {n}+1\in ℕ$
28 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
29 27 28 eleqtrdi ${⊢}{n}\in ℕ\to {n}+1\in {ℤ}_{\ge 1}$
30 elfznn ${⊢}{x}\in \left(1\dots {n}+1\right)\to {x}\in ℕ$
31 30 adantl ${⊢}\left({n}\in ℕ\wedge {x}\in \left(1\dots {n}+1\right)\right)\to {x}\in ℕ$
32 31 nnrpd ${⊢}\left({n}\in ℕ\wedge {x}\in \left(1\dots {n}+1\right)\right)\to {x}\in {ℝ}^{+}$
33 32 relogcld ${⊢}\left({n}\in ℕ\wedge {x}\in \left(1\dots {n}+1\right)\right)\to \mathrm{log}{x}\in ℝ$
34 33 recnd ${⊢}\left({n}\in ℕ\wedge {x}\in \left(1\dots {n}+1\right)\right)\to \mathrm{log}{x}\in ℂ$
35 22 23 24 25 26 29 34 telfsum2 ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\mathrm{log}\left({m}+1\right)-\mathrm{log}{m}\right)=\mathrm{log}\left({n}+1\right)-\mathrm{log}1$
36 log1 ${⊢}\mathrm{log}1=0$
37 36 oveq2i ${⊢}\mathrm{log}\left({n}+1\right)-\mathrm{log}1=\mathrm{log}\left({n}+1\right)-0$
38 27 nnrpd ${⊢}{n}\in ℕ\to {n}+1\in {ℝ}^{+}$
39 38 relogcld ${⊢}{n}\in ℕ\to \mathrm{log}\left({n}+1\right)\in ℝ$
40 39 recnd ${⊢}{n}\in ℕ\to \mathrm{log}\left({n}+1\right)\in ℂ$
41 40 subid1d ${⊢}{n}\in ℕ\to \mathrm{log}\left({n}+1\right)-0=\mathrm{log}\left({n}+1\right)$
42 37 41 syl5eq ${⊢}{n}\in ℕ\to \mathrm{log}\left({n}+1\right)-\mathrm{log}1=\mathrm{log}\left({n}+1\right)$
43 21 35 42 3eqtrd ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)=\mathrm{log}\left({n}+1\right)$
44 43 oveq2d ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\sum _{{m}=1}^{{n}}\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)=\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)$
45 fzfid ${⊢}{n}\in ℕ\to \left(1\dots {n}\right)\in \mathrm{Fin}$
46 6 nnrecred ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \frac{1}{{m}}\in ℝ$
47 46 recnd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \frac{1}{{m}}\in ℂ$
48 1rp ${⊢}1\in {ℝ}^{+}$
49 18 rpreccld ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \frac{1}{{m}}\in {ℝ}^{+}$
50 rpaddcl ${⊢}\left(1\in {ℝ}^{+}\wedge \frac{1}{{m}}\in {ℝ}^{+}\right)\to 1+\left(\frac{1}{{m}}\right)\in {ℝ}^{+}$
51 48 49 50 sylancr ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to 1+\left(\frac{1}{{m}}\right)\in {ℝ}^{+}$
52 51 relogcld ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)\in ℝ$
53 52 recnd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)\in ℂ$
54 45 47 53 fsumsub ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\left(\frac{1}{{m}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)\right)=\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\sum _{{m}=1}^{{n}}\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)$
55 oveq2 ${⊢}{n}={m}\to \frac{1}{{n}}=\frac{1}{{m}}$
56 55 oveq2d ${⊢}{n}={m}\to 1+\left(\frac{1}{{n}}\right)=1+\left(\frac{1}{{m}}\right)$
57 56 fveq2d ${⊢}{n}={m}\to \mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)=\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)$
58 55 57 oveq12d ${⊢}{n}={m}\to \left(\frac{1}{{n}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)=\left(\frac{1}{{m}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)$
59 ovex ${⊢}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)\in \mathrm{V}$
60 58 4 59 fvmpt ${⊢}{m}\in ℕ\to {T}\left({m}\right)=\left(\frac{1}{{m}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)$
61 6 60 syl ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to {T}\left({m}\right)=\left(\frac{1}{{m}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)$
62 id ${⊢}{n}\in ℕ\to {n}\in ℕ$
63 62 28 eleqtrdi ${⊢}{n}\in ℕ\to {n}\in {ℤ}_{\ge 1}$
64 46 52 resubcld ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \left(\frac{1}{{m}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)\in ℝ$
65 64 recnd ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \left(\frac{1}{{m}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)\in ℂ$
66 61 63 65 fsumser ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\left(\frac{1}{{m}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)\right)=seq1\left(+,{T}\right)\left({n}\right)$
67 54 66 eqtr3d ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\sum _{{m}=1}^{{n}}\mathrm{log}\left(1+\left(\frac{1}{{m}}\right)\right)=seq1\left(+,{T}\right)\left({n}\right)$
68 44 67 eqtr3d ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)=seq1\left(+,{T}\right)\left({n}\right)$
69 68 mpteq2ia ${⊢}\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\right)=\left({n}\in ℕ⟼seq1\left(+,{T}\right)\left({n}\right)\right)$
70 1z ${⊢}1\in ℤ$
71 seqfn ${⊢}1\in ℤ\to seq1\left(+,{T}\right)Fn{ℤ}_{\ge 1}$
72 70 71 ax-mp ${⊢}seq1\left(+,{T}\right)Fn{ℤ}_{\ge 1}$
73 28 fneq2i ${⊢}seq1\left(+,{T}\right)Fnℕ↔seq1\left(+,{T}\right)Fn{ℤ}_{\ge 1}$
74 72 73 mpbir ${⊢}seq1\left(+,{T}\right)Fnℕ$
75 dffn5 ${⊢}seq1\left(+,{T}\right)Fnℕ↔seq1\left(+,{T}\right)=\left({n}\in ℕ⟼seq1\left(+,{T}\right)\left({n}\right)\right)$
76 74 75 mpbi ${⊢}seq1\left(+,{T}\right)=\left({n}\in ℕ⟼seq1\left(+,{T}\right)\left({n}\right)\right)$
77 69 2 76 3eqtr4i ${⊢}{G}=seq1\left(+,{T}\right)$