# Metamath Proof Explorer

## Theorem emcllem2

Description: Lemma for emcl . F is increasing, and G is decreasing. (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)$
Assertion emcllem2 ${⊢}{N}\in ℕ\to \left({F}\left({N}+1\right)\le {F}\left({N}\right)\wedge {G}\left({N}\right)\le {G}\left({N}+1\right)\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 peano2nn ${⊢}{N}\in ℕ\to {N}+1\in ℕ$
4 3 nnrecred ${⊢}{N}\in ℕ\to \frac{1}{{N}+1}\in ℝ$
5 3 nnrpd ${⊢}{N}\in ℕ\to {N}+1\in {ℝ}^{+}$
6 5 relogcld ${⊢}{N}\in ℕ\to \mathrm{log}\left({N}+1\right)\in ℝ$
7 nnrp ${⊢}{N}\in ℕ\to {N}\in {ℝ}^{+}$
8 7 relogcld ${⊢}{N}\in ℕ\to \mathrm{log}{N}\in ℝ$
9 6 8 resubcld ${⊢}{N}\in ℕ\to \mathrm{log}\left({N}+1\right)-\mathrm{log}{N}\in ℝ$
10 fzfid ${⊢}{N}\in ℕ\to \left(1\dots {N}\right)\in \mathrm{Fin}$
11 elfznn ${⊢}{m}\in \left(1\dots {N}\right)\to {m}\in ℕ$
12 11 adantl ${⊢}\left({N}\in ℕ\wedge {m}\in \left(1\dots {N}\right)\right)\to {m}\in ℕ$
13 12 nnrecred ${⊢}\left({N}\in ℕ\wedge {m}\in \left(1\dots {N}\right)\right)\to \frac{1}{{m}}\in ℝ$
14 10 13 fsumrecl ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)\in ℝ$
15 5 rpreccld ${⊢}{N}\in ℕ\to \frac{1}{{N}+1}\in {ℝ}^{+}$
16 15 rpge0d ${⊢}{N}\in ℕ\to 0\le \frac{1}{{N}+1}$
17 1div1e1 ${⊢}\frac{1}{1}=1$
18 1re ${⊢}1\in ℝ$
19 ltaddrp ${⊢}\left(1\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to 1<1+{N}$
20 18 7 19 sylancr ${⊢}{N}\in ℕ\to 1<1+{N}$
21 ax-1cn ${⊢}1\in ℂ$
22 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
23 addcom ${⊢}\left(1\in ℂ\wedge {N}\in ℂ\right)\to 1+{N}={N}+1$
24 21 22 23 sylancr ${⊢}{N}\in ℕ\to 1+{N}={N}+1$
25 20 24 breqtrd ${⊢}{N}\in ℕ\to 1<{N}+1$
26 17 25 eqbrtrid ${⊢}{N}\in ℕ\to \frac{1}{1}<{N}+1$
27 3 nnred ${⊢}{N}\in ℕ\to {N}+1\in ℝ$
28 3 nngt0d ${⊢}{N}\in ℕ\to 0<{N}+1$
29 0lt1 ${⊢}0<1$
30 ltrec1 ${⊢}\left(\left(1\in ℝ\wedge 0<1\right)\wedge \left({N}+1\in ℝ\wedge 0<{N}+1\right)\right)\to \left(\frac{1}{1}<{N}+1↔\frac{1}{{N}+1}<1\right)$
31 18 29 30 mpanl12 ${⊢}\left({N}+1\in ℝ\wedge 0<{N}+1\right)\to \left(\frac{1}{1}<{N}+1↔\frac{1}{{N}+1}<1\right)$
32 27 28 31 syl2anc ${⊢}{N}\in ℕ\to \left(\frac{1}{1}<{N}+1↔\frac{1}{{N}+1}<1\right)$
33 26 32 mpbid ${⊢}{N}\in ℕ\to \frac{1}{{N}+1}<1$
34 4 16 33 eflegeo ${⊢}{N}\in ℕ\to {\mathrm{e}}^{\frac{1}{{N}+1}}\le \frac{1}{1-\left(\frac{1}{{N}+1}\right)}$
35 27 recnd ${⊢}{N}\in ℕ\to {N}+1\in ℂ$
36 nnne0 ${⊢}{N}\in ℕ\to {N}\ne 0$
37 3 nnne0d ${⊢}{N}\in ℕ\to {N}+1\ne 0$
38 22 35 36 37 recdivd ${⊢}{N}\in ℕ\to \frac{1}{\frac{{N}}{{N}+1}}=\frac{{N}+1}{{N}}$
39 1cnd ${⊢}{N}\in ℕ\to 1\in ℂ$
40 35 39 35 37 divsubdird ${⊢}{N}\in ℕ\to \frac{{N}+1-1}{{N}+1}=\left(\frac{{N}+1}{{N}+1}\right)-\left(\frac{1}{{N}+1}\right)$
41 pncan ${⊢}\left({N}\in ℂ\wedge 1\in ℂ\right)\to {N}+1-1={N}$
42 22 21 41 sylancl ${⊢}{N}\in ℕ\to {N}+1-1={N}$
43 42 oveq1d ${⊢}{N}\in ℕ\to \frac{{N}+1-1}{{N}+1}=\frac{{N}}{{N}+1}$
44 35 37 dividd ${⊢}{N}\in ℕ\to \frac{{N}+1}{{N}+1}=1$
45 44 oveq1d ${⊢}{N}\in ℕ\to \left(\frac{{N}+1}{{N}+1}\right)-\left(\frac{1}{{N}+1}\right)=1-\left(\frac{1}{{N}+1}\right)$
46 40 43 45 3eqtr3rd ${⊢}{N}\in ℕ\to 1-\left(\frac{1}{{N}+1}\right)=\frac{{N}}{{N}+1}$
47 46 oveq2d ${⊢}{N}\in ℕ\to \frac{1}{1-\left(\frac{1}{{N}+1}\right)}=\frac{1}{\frac{{N}}{{N}+1}}$
48 5 7 rpdivcld ${⊢}{N}\in ℕ\to \frac{{N}+1}{{N}}\in {ℝ}^{+}$
49 48 reeflogd ${⊢}{N}\in ℕ\to {\mathrm{e}}^{\mathrm{log}\left(\frac{{N}+1}{{N}}\right)}=\frac{{N}+1}{{N}}$
50 38 47 49 3eqtr4d ${⊢}{N}\in ℕ\to \frac{1}{1-\left(\frac{1}{{N}+1}\right)}={\mathrm{e}}^{\mathrm{log}\left(\frac{{N}+1}{{N}}\right)}$
51 34 50 breqtrd ${⊢}{N}\in ℕ\to {\mathrm{e}}^{\frac{1}{{N}+1}}\le {\mathrm{e}}^{\mathrm{log}\left(\frac{{N}+1}{{N}}\right)}$
52 5 7 relogdivd ${⊢}{N}\in ℕ\to \mathrm{log}\left(\frac{{N}+1}{{N}}\right)=\mathrm{log}\left({N}+1\right)-\mathrm{log}{N}$
53 52 9 eqeltrd ${⊢}{N}\in ℕ\to \mathrm{log}\left(\frac{{N}+1}{{N}}\right)\in ℝ$
54 efle ${⊢}\left(\frac{1}{{N}+1}\in ℝ\wedge \mathrm{log}\left(\frac{{N}+1}{{N}}\right)\in ℝ\right)\to \left(\frac{1}{{N}+1}\le \mathrm{log}\left(\frac{{N}+1}{{N}}\right)↔{\mathrm{e}}^{\frac{1}{{N}+1}}\le {\mathrm{e}}^{\mathrm{log}\left(\frac{{N}+1}{{N}}\right)}\right)$
55 4 53 54 syl2anc ${⊢}{N}\in ℕ\to \left(\frac{1}{{N}+1}\le \mathrm{log}\left(\frac{{N}+1}{{N}}\right)↔{\mathrm{e}}^{\frac{1}{{N}+1}}\le {\mathrm{e}}^{\mathrm{log}\left(\frac{{N}+1}{{N}}\right)}\right)$
56 51 55 mpbird ${⊢}{N}\in ℕ\to \frac{1}{{N}+1}\le \mathrm{log}\left(\frac{{N}+1}{{N}}\right)$
57 56 52 breqtrd ${⊢}{N}\in ℕ\to \frac{1}{{N}+1}\le \mathrm{log}\left({N}+1\right)-\mathrm{log}{N}$
58 4 9 14 57 leadd2dd ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)+\left(\frac{1}{{N}+1}\right)\le \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)+\mathrm{log}\left({N}+1\right)-\mathrm{log}{N}$
59 id ${⊢}{N}\in ℕ\to {N}\in ℕ$
60 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
61 59 60 eleqtrdi ${⊢}{N}\in ℕ\to {N}\in {ℤ}_{\ge 1}$
62 elfznn ${⊢}{m}\in \left(1\dots {N}+1\right)\to {m}\in ℕ$
63 62 adantl ${⊢}\left({N}\in ℕ\wedge {m}\in \left(1\dots {N}+1\right)\right)\to {m}\in ℕ$
64 63 nnrecred ${⊢}\left({N}\in ℕ\wedge {m}\in \left(1\dots {N}+1\right)\right)\to \frac{1}{{m}}\in ℝ$
65 64 recnd ${⊢}\left({N}\in ℕ\wedge {m}\in \left(1\dots {N}+1\right)\right)\to \frac{1}{{m}}\in ℂ$
66 oveq2 ${⊢}{m}={N}+1\to \frac{1}{{m}}=\frac{1}{{N}+1}$
67 61 65 66 fsump1 ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)=\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)+\left(\frac{1}{{N}+1}\right)$
68 6 recnd ${⊢}{N}\in ℕ\to \mathrm{log}\left({N}+1\right)\in ℂ$
69 14 recnd ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)\in ℂ$
70 8 recnd ${⊢}{N}\in ℕ\to \mathrm{log}{N}\in ℂ$
71 68 69 70 addsub12d ${⊢}{N}\in ℕ\to \mathrm{log}\left({N}+1\right)+\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}=\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)+\mathrm{log}\left({N}+1\right)-\mathrm{log}{N}$
72 58 67 71 3brtr4d ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)\le \mathrm{log}\left({N}+1\right)+\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}$
73 fzfid ${⊢}{N}\in ℕ\to \left(1\dots {N}+1\right)\in \mathrm{Fin}$
74 73 64 fsumrecl ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)\in ℝ$
75 14 8 resubcld ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}\in ℝ$
76 74 6 75 lesubadd2d ${⊢}{N}\in ℕ\to \left(\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\le \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}↔\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)\le \mathrm{log}\left({N}+1\right)+\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}\right)$
77 72 76 mpbird ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\le \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}$
78 oveq2 ${⊢}{n}={N}+1\to \left(1\dots {n}\right)=\left(1\dots {N}+1\right)$
79 78 sumeq1d ${⊢}{n}={N}+1\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)=\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)$
80 fveq2 ${⊢}{n}={N}+1\to \mathrm{log}{n}=\mathrm{log}\left({N}+1\right)$
81 79 80 oveq12d ${⊢}{n}={N}+1\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}=\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)$
82 ovex ${⊢}\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\in \mathrm{V}$
83 81 1 82 fvmpt ${⊢}{N}+1\in ℕ\to {F}\left({N}+1\right)=\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)$
84 3 83 syl ${⊢}{N}\in ℕ\to {F}\left({N}+1\right)=\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)$
85 oveq2 ${⊢}{n}={N}\to \left(1\dots {n}\right)=\left(1\dots {N}\right)$
86 85 sumeq1d ${⊢}{n}={N}\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)=\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)$
87 fveq2 ${⊢}{n}={N}\to \mathrm{log}{n}=\mathrm{log}{N}$
88 86 87 oveq12d ${⊢}{n}={N}\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}=\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}$
89 ovex ${⊢}\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}\in \mathrm{V}$
90 88 1 89 fvmpt ${⊢}{N}\in ℕ\to {F}\left({N}\right)=\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}{N}$
91 77 84 90 3brtr4d ${⊢}{N}\in ℕ\to {F}\left({N}+1\right)\le {F}\left({N}\right)$
92 peano2nn ${⊢}{N}+1\in ℕ\to {N}+1+1\in ℕ$
93 3 92 syl ${⊢}{N}\in ℕ\to {N}+1+1\in ℕ$
94 93 nnrpd ${⊢}{N}\in ℕ\to {N}+1+1\in {ℝ}^{+}$
95 94 relogcld ${⊢}{N}\in ℕ\to \mathrm{log}\left({N}+1+1\right)\in ℝ$
96 95 6 resubcld ${⊢}{N}\in ℕ\to \mathrm{log}\left({N}+1+1\right)-\mathrm{log}\left({N}+1\right)\in ℝ$
97 logdifbnd ${⊢}{N}+1\in {ℝ}^{+}\to \mathrm{log}\left({N}+1+1\right)-\mathrm{log}\left({N}+1\right)\le \frac{1}{{N}+1}$
98 5 97 syl ${⊢}{N}\in ℕ\to \mathrm{log}\left({N}+1+1\right)-\mathrm{log}\left({N}+1\right)\le \frac{1}{{N}+1}$
99 96 4 14 98 leadd2dd ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)+\mathrm{log}\left({N}+1+1\right)-\mathrm{log}\left({N}+1\right)\le \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)+\left(\frac{1}{{N}+1}\right)$
100 95 recnd ${⊢}{N}\in ℕ\to \mathrm{log}\left({N}+1+1\right)\in ℂ$
101 69 68 100 subadd23d ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)+\mathrm{log}\left({N}+1+1\right)=\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)+\mathrm{log}\left({N}+1+1\right)-\mathrm{log}\left({N}+1\right)$
102 99 101 67 3brtr4d ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)+\mathrm{log}\left({N}+1+1\right)\le \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)$
103 14 6 resubcld ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\in ℝ$
104 leaddsub ${⊢}\left(\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\in ℝ\wedge \mathrm{log}\left({N}+1+1\right)\in ℝ\wedge \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)\in ℝ\right)\to \left(\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)+\mathrm{log}\left({N}+1+1\right)\le \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)↔\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\le \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1+1\right)\right)$
105 103 95 74 104 syl3anc ${⊢}{N}\in ℕ\to \left(\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)+\mathrm{log}\left({N}+1+1\right)\le \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)↔\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\le \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1+1\right)\right)$
106 102 105 mpbid ${⊢}{N}\in ℕ\to \sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\le \sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1+1\right)$
107 fvoveq1 ${⊢}{n}={N}\to \mathrm{log}\left({n}+1\right)=\mathrm{log}\left({N}+1\right)$
108 86 107 oveq12d ${⊢}{n}={N}\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)=\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)$
109 ovex ${⊢}\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)\in \mathrm{V}$
110 108 2 109 fvmpt ${⊢}{N}\in ℕ\to {G}\left({N}\right)=\sum _{{m}=1}^{{N}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1\right)$
111 fvoveq1 ${⊢}{n}={N}+1\to \mathrm{log}\left({n}+1\right)=\mathrm{log}\left({N}+1+1\right)$
112 79 111 oveq12d ${⊢}{n}={N}+1\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)=\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1+1\right)$
113 ovex ${⊢}\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1+1\right)\in \mathrm{V}$
114 112 2 113 fvmpt ${⊢}{N}+1\in ℕ\to {G}\left({N}+1\right)=\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1+1\right)$
115 3 114 syl ${⊢}{N}\in ℕ\to {G}\left({N}+1\right)=\sum _{{m}=1}^{{N}+1}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({N}+1+1\right)$
116 106 110 115 3brtr4d ${⊢}{N}\in ℕ\to {G}\left({N}\right)\le {G}\left({N}+1\right)$
117 91 116 jca ${⊢}{N}\in ℕ\to \left({F}\left({N}+1\right)\le {F}\left({N}\right)\wedge {G}\left({N}\right)\le {G}\left({N}+1\right)\right)$