# Metamath Proof Explorer

## Theorem mulog2sumlem1

Description: Asymptotic formula for sum_ n <_ x , log ( x / n ) / n = ( 1 / 2 ) log ^ 2 ( x ) + gamma x. log x - L + O ( log x / x ) , with explicit constants. Equation 10.2.7 of Shapiro, p. 407. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses logdivsum.1 ${⊢}{F}=\left({y}\in {ℝ}^{+}⟼\sum _{{i}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{i}}{{i}}\right)-\left(\frac{{\mathrm{log}{y}}^{2}}{2}\right)\right)$
mulog2sumlem.1
mulog2sumlem1.2 ${⊢}{\phi }\to {A}\in {ℝ}^{+}$
mulog2sumlem1.3 ${⊢}{\phi }\to \mathrm{e}\le {A}$
Assertion mulog2sumlem1 ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)\right|\le 2\left(\frac{\mathrm{log}{A}}{{A}}\right)$

### Proof

Step Hyp Ref Expression
1 logdivsum.1 ${⊢}{F}=\left({y}\in {ℝ}^{+}⟼\sum _{{i}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{i}}{{i}}\right)-\left(\frac{{\mathrm{log}{y}}^{2}}{2}\right)\right)$
2 mulog2sumlem.1
3 mulog2sumlem1.2 ${⊢}{\phi }\to {A}\in {ℝ}^{+}$
4 mulog2sumlem1.3 ${⊢}{\phi }\to \mathrm{e}\le {A}$
5 fzfid ${⊢}{\phi }\to \left(1\dots ⌊{A}⌋\right)\in \mathrm{Fin}$
6 elfznn ${⊢}{m}\in \left(1\dots ⌊{A}⌋\right)\to {m}\in ℕ$
7 6 nnrpd ${⊢}{m}\in \left(1\dots ⌊{A}⌋\right)\to {m}\in {ℝ}^{+}$
8 rpdivcl ${⊢}\left({A}\in {ℝ}^{+}\wedge {m}\in {ℝ}^{+}\right)\to \frac{{A}}{{m}}\in {ℝ}^{+}$
9 3 7 8 syl2an ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{{A}}{{m}}\in {ℝ}^{+}$
10 9 relogcld ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \mathrm{log}\left(\frac{{A}}{{m}}\right)\in ℝ$
11 6 adantl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to {m}\in ℕ$
12 10 11 nndivred ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\in ℝ$
13 5 12 fsumrecl ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)\in ℝ$
14 3 relogcld ${⊢}{\phi }\to \mathrm{log}{A}\in ℝ$
15 14 resqcld ${⊢}{\phi }\to {\mathrm{log}{A}}^{2}\in ℝ$
16 15 rehalfcld ${⊢}{\phi }\to \frac{{\mathrm{log}{A}}^{2}}{2}\in ℝ$
17 emre ${⊢}\gamma \in ℝ$
18 remulcl ${⊢}\left(\gamma \in ℝ\wedge \mathrm{log}{A}\in ℝ\right)\to \gamma \mathrm{log}{A}\in ℝ$
19 17 14 18 sylancr ${⊢}{\phi }\to \gamma \mathrm{log}{A}\in ℝ$
20 rpsup ${⊢}sup\left({ℝ}^{+},{ℝ}^{*},<\right)=\mathrm{+\infty }$
21 20 a1i ${⊢}{\phi }\to sup\left({ℝ}^{+},{ℝ}^{*},<\right)=\mathrm{+\infty }$
22 1 logdivsum
23 22 simp1i ${⊢}{F}:{ℝ}^{+}⟶ℝ$
24 23 a1i ${⊢}{\phi }\to {F}:{ℝ}^{+}⟶ℝ$
25 24 feqmptd ${⊢}{\phi }\to {F}=\left({x}\in {ℝ}^{+}⟼{F}\left({x}\right)\right)$
26 25 2 eqbrtrrd
27 23 ffvelrni ${⊢}{x}\in {ℝ}^{+}\to {F}\left({x}\right)\in ℝ$
28 27 adantl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {F}\left({x}\right)\in ℝ$
29 21 26 28 rlimrecl ${⊢}{\phi }\to {L}\in ℝ$
30 19 29 resubcld ${⊢}{\phi }\to \gamma \mathrm{log}{A}-{L}\in ℝ$
31 16 30 readdcld ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\in ℝ$
32 13 31 resubcld ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)\in ℝ$
33 32 recnd ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)\in ℂ$
34 33 abscld ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)\right|\in ℝ$
35 rerpdivcl ${⊢}\left(\mathrm{log}{A}\in ℝ\wedge {m}\in {ℝ}^{+}\right)\to \frac{\mathrm{log}{A}}{{m}}\in ℝ$
36 14 7 35 syl2an ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}{A}}{{m}}\in ℝ$
37 36 recnd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}{A}}{{m}}\in ℂ$
38 5 37 fsumcl ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)\in ℂ$
39 14 recnd ${⊢}{\phi }\to \mathrm{log}{A}\in ℂ$
40 readdcl ${⊢}\left(\mathrm{log}{A}\in ℝ\wedge \gamma \in ℝ\right)\to \mathrm{log}{A}+\gamma \in ℝ$
41 14 17 40 sylancl ${⊢}{\phi }\to \mathrm{log}{A}+\gamma \in ℝ$
42 41 recnd ${⊢}{\phi }\to \mathrm{log}{A}+\gamma \in ℂ$
43 39 42 mulcld ${⊢}{\phi }\to \mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\in ℂ$
44 38 43 subcld ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\in ℂ$
45 44 abscld ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|\in ℝ$
46 11 nnrpd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to {m}\in {ℝ}^{+}$
47 46 relogcld ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \mathrm{log}{m}\in ℝ$
48 47 11 nndivred ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}{m}}{{m}}\in ℝ$
49 48 recnd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}{m}}{{m}}\in ℂ$
50 5 49 fsumcl ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)\in ℂ$
51 16 recnd ${⊢}{\phi }\to \frac{{\mathrm{log}{A}}^{2}}{2}\in ℂ$
52 29 recnd ${⊢}{\phi }\to {L}\in ℂ$
53 51 52 addcld ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\in ℂ$
54 50 53 subcld ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\in ℂ$
55 54 abscld ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right|\in ℝ$
56 45 55 readdcld ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|+\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right|\in ℝ$
57 2re ${⊢}2\in ℝ$
58 14 3 rerpdivcld ${⊢}{\phi }\to \frac{\mathrm{log}{A}}{{A}}\in ℝ$
59 remulcl ${⊢}\left(2\in ℝ\wedge \frac{\mathrm{log}{A}}{{A}}\in ℝ\right)\to 2\left(\frac{\mathrm{log}{A}}{{A}}\right)\in ℝ$
60 57 58 59 sylancr ${⊢}{\phi }\to 2\left(\frac{\mathrm{log}{A}}{{A}}\right)\in ℝ$
61 relogdiv ${⊢}\left({A}\in {ℝ}^{+}\wedge {m}\in {ℝ}^{+}\right)\to \mathrm{log}\left(\frac{{A}}{{m}}\right)=\mathrm{log}{A}-\mathrm{log}{m}$
62 3 7 61 syl2an ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \mathrm{log}\left(\frac{{A}}{{m}}\right)=\mathrm{log}{A}-\mathrm{log}{m}$
63 62 oveq1d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}=\frac{\mathrm{log}{A}-\mathrm{log}{m}}{{m}}$
64 39 adantr ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \mathrm{log}{A}\in ℂ$
65 47 recnd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \mathrm{log}{m}\in ℂ$
66 46 rpcnne0d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \left({m}\in ℂ\wedge {m}\ne 0\right)$
67 divsubdir ${⊢}\left(\mathrm{log}{A}\in ℂ\wedge \mathrm{log}{m}\in ℂ\wedge \left({m}\in ℂ\wedge {m}\ne 0\right)\right)\to \frac{\mathrm{log}{A}-\mathrm{log}{m}}{{m}}=\left(\frac{\mathrm{log}{A}}{{m}}\right)-\left(\frac{\mathrm{log}{m}}{{m}}\right)$
68 64 65 66 67 syl3anc ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}{A}-\mathrm{log}{m}}{{m}}=\left(\frac{\mathrm{log}{A}}{{m}}\right)-\left(\frac{\mathrm{log}{m}}{{m}}\right)$
69 63 68 eqtrd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}=\left(\frac{\mathrm{log}{A}}{{m}}\right)-\left(\frac{\mathrm{log}{m}}{{m}}\right)$
70 69 sumeq2dv ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\left(\frac{\mathrm{log}{A}}{{m}}\right)-\left(\frac{\mathrm{log}{m}}{{m}}\right)\right)$
71 5 37 49 fsumsub ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\left(\frac{\mathrm{log}{A}}{{m}}\right)-\left(\frac{\mathrm{log}{m}}{{m}}\right)\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
72 70 71 eqtrd ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
73 remulcl ${⊢}\left(\mathrm{log}{A}\in ℝ\wedge \gamma \in ℝ\right)\to \mathrm{log}{A}\gamma \in ℝ$
74 14 17 73 sylancl ${⊢}{\phi }\to \mathrm{log}{A}\gamma \in ℝ$
75 16 74 readdcld ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma \in ℝ$
76 75 recnd ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma \in ℂ$
77 76 51 pncand ${⊢}{\phi }\to \left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma \right)+\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)=\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma$
78 17 recni ${⊢}\gamma \in ℂ$
79 78 a1i ${⊢}{\phi }\to \gamma \in ℂ$
80 39 39 79 adddid ${⊢}{\phi }\to \mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)=\mathrm{log}{A}\mathrm{log}{A}+\mathrm{log}{A}\gamma$
81 15 recnd ${⊢}{\phi }\to {\mathrm{log}{A}}^{2}\in ℂ$
82 81 2halvesd ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)={\mathrm{log}{A}}^{2}$
83 39 sqvald ${⊢}{\phi }\to {\mathrm{log}{A}}^{2}=\mathrm{log}{A}\mathrm{log}{A}$
84 82 83 eqtrd ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)=\mathrm{log}{A}\mathrm{log}{A}$
85 84 oveq1d ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma =\mathrm{log}{A}\mathrm{log}{A}+\mathrm{log}{A}\gamma$
86 74 recnd ${⊢}{\phi }\to \mathrm{log}{A}\gamma \in ℂ$
87 51 51 86 add32d ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma =\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma +\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)$
88 80 85 87 3eqtr2d ${⊢}{\phi }\to \mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)=\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma +\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)$
89 88 oveq1d ${⊢}{\phi }\to \mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)=\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma \right)+\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)$
90 mulcom ${⊢}\left(\gamma \in ℂ\wedge \mathrm{log}{A}\in ℂ\right)\to \gamma \mathrm{log}{A}=\mathrm{log}{A}\gamma$
91 78 39 90 sylancr ${⊢}{\phi }\to \gamma \mathrm{log}{A}=\mathrm{log}{A}\gamma$
92 91 oveq2d ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}=\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\mathrm{log}{A}\gamma$
93 77 89 92 3eqtr4rd ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}=\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)$
94 93 oveq1d ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}=\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)-{L}$
95 91 86 eqeltrd ${⊢}{\phi }\to \gamma \mathrm{log}{A}\in ℂ$
96 51 95 52 addsubassd ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}=\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}$
97 43 51 52 subsub4d ${⊢}{\phi }\to \mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)-{L}=\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)$
98 94 96 97 3eqtr3d ${⊢}{\phi }\to \left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}=\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)$
99 72 98 oveq12d ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right)$
100 38 50 43 53 sub4d ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right)$
101 99 100 eqtrd ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right)$
102 101 fveq2d ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)\right|=\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right)\right|$
103 44 54 abs2dif2d ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)-\left(\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right)\right|\le \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|+\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right|$
104 102 103 eqbrtrd ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)\right|\le \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|+\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right|$
105 harmonicbnd4 ${⊢}{A}\in {ℝ}^{+}\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\le \frac{1}{{A}}$
106 3 105 syl ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\le \frac{1}{{A}}$
107 11 nnrecred ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{1}{{m}}\in ℝ$
108 5 107 fsumrecl ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)\in ℝ$
109 108 41 resubcld ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\in ℝ$
110 109 recnd ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\in ℂ$
111 110 abscld ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\in ℝ$
112 3 rprecred ${⊢}{\phi }\to \frac{1}{{A}}\in ℝ$
113 0red ${⊢}{\phi }\to 0\in ℝ$
114 1red ${⊢}{\phi }\to 1\in ℝ$
115 0lt1 ${⊢}0<1$
116 115 a1i ${⊢}{\phi }\to 0<1$
117 loge ${⊢}\mathrm{log}\mathrm{e}=1$
118 epr ${⊢}\mathrm{e}\in {ℝ}^{+}$
119 logleb ${⊢}\left(\mathrm{e}\in {ℝ}^{+}\wedge {A}\in {ℝ}^{+}\right)\to \left(\mathrm{e}\le {A}↔\mathrm{log}\mathrm{e}\le \mathrm{log}{A}\right)$
120 118 3 119 sylancr ${⊢}{\phi }\to \left(\mathrm{e}\le {A}↔\mathrm{log}\mathrm{e}\le \mathrm{log}{A}\right)$
121 4 120 mpbid ${⊢}{\phi }\to \mathrm{log}\mathrm{e}\le \mathrm{log}{A}$
122 117 121 eqbrtrrid ${⊢}{\phi }\to 1\le \mathrm{log}{A}$
123 113 114 14 116 122 ltletrd ${⊢}{\phi }\to 0<\mathrm{log}{A}$
124 lemul2 ${⊢}\left(\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\in ℝ\wedge \frac{1}{{A}}\in ℝ\wedge \left(\mathrm{log}{A}\in ℝ\wedge 0<\mathrm{log}{A}\right)\right)\to \left(\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\le \frac{1}{{A}}↔\mathrm{log}{A}\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\le \mathrm{log}{A}\left(\frac{1}{{A}}\right)\right)$
125 111 112 14 123 124 syl112anc ${⊢}{\phi }\to \left(\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\le \frac{1}{{A}}↔\mathrm{log}{A}\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\le \mathrm{log}{A}\left(\frac{1}{{A}}\right)\right)$
126 106 125 mpbid ${⊢}{\phi }\to \mathrm{log}{A}\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|\le \mathrm{log}{A}\left(\frac{1}{{A}}\right)$
127 46 rpcnd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to {m}\in ℂ$
128 46 rpne0d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to {m}\ne 0$
129 64 127 128 divrecd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{\mathrm{log}{A}}{{m}}=\mathrm{log}{A}\left(\frac{1}{{m}}\right)$
130 129 sumeq2dv ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\mathrm{log}{A}\left(\frac{1}{{m}}\right)$
131 107 recnd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{1}{{m}}\in ℂ$
132 5 39 131 fsummulc2 ${⊢}{\phi }\to \mathrm{log}{A}\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\mathrm{log}{A}\left(\frac{1}{{m}}\right)$
133 130 132 eqtr4d ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)=\mathrm{log}{A}\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)$
134 133 oveq1d ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)=\mathrm{log}{A}\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)$
135 5 131 fsumcl ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)\in ℂ$
136 39 135 42 subdid ${⊢}{\phi }\to \mathrm{log}{A}\left(\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right)=\mathrm{log}{A}\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)$
137 134 136 eqtr4d ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)=\mathrm{log}{A}\left(\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right)$
138 137 fveq2d ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|=\left|\mathrm{log}{A}\left(\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right)\right|$
139 135 42 subcld ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\in ℂ$
140 39 139 absmuld ${⊢}{\phi }\to \left|\mathrm{log}{A}\left(\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right)\right|=\left|\mathrm{log}{A}\right|\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|$
141 113 14 123 ltled ${⊢}{\phi }\to 0\le \mathrm{log}{A}$
142 14 141 absidd ${⊢}{\phi }\to \left|\mathrm{log}{A}\right|=\mathrm{log}{A}$
143 142 oveq1d ${⊢}{\phi }\to \left|\mathrm{log}{A}\right|\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|=\mathrm{log}{A}\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|$
144 138 140 143 3eqtrd ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|=\mathrm{log}{A}\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{1}{{m}}\right)-\left(\mathrm{log}{A}+\gamma \right)\right|$
145 3 rpcnd ${⊢}{\phi }\to {A}\in ℂ$
146 3 rpne0d ${⊢}{\phi }\to {A}\ne 0$
147 39 145 146 divrecd ${⊢}{\phi }\to \frac{\mathrm{log}{A}}{{A}}=\mathrm{log}{A}\left(\frac{1}{{A}}\right)$
148 126 144 147 3brtr4d ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|\le \frac{\mathrm{log}{A}}{{A}}$
149 fveq2 ${⊢}{i}={m}\to \mathrm{log}{i}=\mathrm{log}{m}$
150 id ${⊢}{i}={m}\to {i}={m}$
151 149 150 oveq12d ${⊢}{i}={m}\to \frac{\mathrm{log}{i}}{{i}}=\frac{\mathrm{log}{m}}{{m}}$
152 151 cbvsumv ${⊢}\sum _{{i}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{i}}{{i}}\right)=\sum _{{m}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
153 fveq2 ${⊢}{y}={A}\to ⌊{y}⌋=⌊{A}⌋$
154 153 oveq2d ${⊢}{y}={A}\to \left(1\dots ⌊{y}⌋\right)=\left(1\dots ⌊{A}⌋\right)$
155 154 sumeq1d ${⊢}{y}={A}\to \sum _{{m}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
156 152 155 syl5eq ${⊢}{y}={A}\to \sum _{{i}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{i}}{{i}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
157 fveq2 ${⊢}{y}={A}\to \mathrm{log}{y}=\mathrm{log}{A}$
158 157 oveq1d ${⊢}{y}={A}\to {\mathrm{log}{y}}^{2}={\mathrm{log}{A}}^{2}$
159 158 oveq1d ${⊢}{y}={A}\to \frac{{\mathrm{log}{y}}^{2}}{2}=\frac{{\mathrm{log}{A}}^{2}}{2}$
160 156 159 oveq12d ${⊢}{y}={A}\to \sum _{{i}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{i}}{{i}}\right)-\left(\frac{{\mathrm{log}{y}}^{2}}{2}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)$
161 ovex ${⊢}\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)\in \mathrm{V}$
162 160 1 161 fvmpt ${⊢}{A}\in {ℝ}^{+}\to {F}\left({A}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)$
163 3 162 syl ${⊢}{\phi }\to {F}\left({A}\right)=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)$
164 163 oveq1d ${⊢}{\phi }\to {F}\left({A}\right)-{L}=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)-{L}$
165 50 51 52 subsub4d ${⊢}{\phi }\to \sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)-{L}=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)$
166 164 165 eqtrd ${⊢}{\phi }\to {F}\left({A}\right)-{L}=\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)$
167 166 fveq2d ${⊢}{\phi }\to \left|{F}\left({A}\right)-{L}\right|=\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right|$
168 22 simp3i
169 2 3 4 168 syl3anc ${⊢}{\phi }\to \left|{F}\left({A}\right)-{L}\right|\le \frac{\mathrm{log}{A}}{{A}}$
170 167 169 eqbrtrrd ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right|\le \frac{\mathrm{log}{A}}{{A}}$
171 45 55 58 58 148 170 le2addd ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|+\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right|\le \left(\frac{\mathrm{log}{A}}{{A}}\right)+\left(\frac{\mathrm{log}{A}}{{A}}\right)$
172 58 recnd ${⊢}{\phi }\to \frac{\mathrm{log}{A}}{{A}}\in ℂ$
173 172 2timesd ${⊢}{\phi }\to 2\left(\frac{\mathrm{log}{A}}{{A}}\right)=\left(\frac{\mathrm{log}{A}}{{A}}\right)+\left(\frac{\mathrm{log}{A}}{{A}}\right)$
174 171 173 breqtrrd ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{A}}{{m}}\right)-\mathrm{log}{A}\left(\mathrm{log}{A}+\gamma \right)\right|+\left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}{m}}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+{L}\right)\right|\le 2\left(\frac{\mathrm{log}{A}}{{A}}\right)$
175 34 56 60 104 174 letrd ${⊢}{\phi }\to \left|\sum _{{m}=1}^{⌊{A}⌋}\left(\frac{\mathrm{log}\left(\frac{{A}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}{A}}^{2}}{2}\right)+\gamma \mathrm{log}{A}-{L}\right)\right|\le 2\left(\frac{\mathrm{log}{A}}{{A}}\right)$