# Metamath Proof Explorer

## Theorem log2sumbnd

Description: Bound on the difference between sum_ n <_ A , log ^ 2 ( n ) and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016)

Ref Expression
Assertion log2sumbnd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|\le {\mathrm{log}{A}}^{2}+2$

### Proof

Step Hyp Ref Expression
1 fzfid ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left(1\dots ⌊{A}⌋\right)\in \mathrm{Fin}$
2 elfznn ${⊢}{n}\in \left(1\dots ⌊{A}⌋\right)\to {n}\in ℕ$
3 2 adantl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to {n}\in ℕ$
4 3 nnrpd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to {n}\in {ℝ}^{+}$
5 4 relogcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \mathrm{log}{n}\in ℝ$
6 5 resqcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to {\mathrm{log}{n}}^{2}\in ℝ$
7 1 6 fsumrecl ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}\in ℝ$
8 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
9 8 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {A}\in ℝ$
10 relogcl ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{A}\in ℝ$
11 10 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \mathrm{log}{A}\in ℝ$
12 11 resqcld ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {\mathrm{log}{A}}^{2}\in ℝ$
13 2re ${⊢}2\in ℝ$
14 remulcl ${⊢}\left(2\in ℝ\wedge \mathrm{log}{A}\in ℝ\right)\to 2\mathrm{log}{A}\in ℝ$
15 13 11 14 sylancr ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 2\mathrm{log}{A}\in ℝ$
16 resubcl ${⊢}\left(2\in ℝ\wedge 2\mathrm{log}{A}\in ℝ\right)\to 2-2\mathrm{log}{A}\in ℝ$
17 13 15 16 sylancr ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 2-2\mathrm{log}{A}\in ℝ$
18 12 17 readdcld ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\in ℝ$
19 9 18 remulcld ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\in ℝ$
20 7 19 resubcld ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\in ℝ$
21 20 recnd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\in ℂ$
22 21 abscld ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|\in ℝ$
23 resubcl ${⊢}\left(\left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|\in ℝ\wedge 2\in ℝ\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-2\in ℝ$
24 22 13 23 sylancl ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-2\in ℝ$
25 2cn ${⊢}2\in ℂ$
26 25 negcli ${⊢}-2\in ℂ$
27 subcl ${⊢}\left(\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\in ℂ\wedge -2\in ℂ\right)\to \sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2\in ℂ$
28 21 26 27 sylancl ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2\in ℂ$
29 28 abscld ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2\right|\in ℝ$
30 25 absnegi ${⊢}\left|-2\right|=\left|2\right|$
31 0le2 ${⊢}0\le 2$
32 absid ${⊢}\left(2\in ℝ\wedge 0\le 2\right)\to \left|2\right|=2$
33 13 31 32 mp2an ${⊢}\left|2\right|=2$
34 30 33 eqtri ${⊢}\left|-2\right|=2$
35 34 oveq2i ${⊢}\left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-\left|-2\right|=\left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-2$
36 abs2dif ${⊢}\left(\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\in ℂ\wedge -2\in ℂ\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-\left|-2\right|\le \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2\right|$
37 21 26 36 sylancl ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-\left|-2\right|\le \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2\right|$
38 35 37 eqbrtrrid ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-2\le \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2\right|$
39 fveq2 ${⊢}{x}={A}\to ⌊{x}⌋=⌊{A}⌋$
40 39 oveq2d ${⊢}{x}={A}\to \left(1\dots ⌊{x}⌋\right)=\left(1\dots ⌊{A}⌋\right)$
41 40 sumeq1d ${⊢}{x}={A}\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}=\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}$
42 id ${⊢}{x}={A}\to {x}={A}$
43 fveq2 ${⊢}{x}={A}\to \mathrm{log}{x}=\mathrm{log}{A}$
44 43 oveq1d ${⊢}{x}={A}\to {\mathrm{log}{x}}^{2}={\mathrm{log}{A}}^{2}$
45 43 oveq2d ${⊢}{x}={A}\to 2\mathrm{log}{x}=2\mathrm{log}{A}$
46 45 oveq2d ${⊢}{x}={A}\to 2-2\mathrm{log}{x}=2-2\mathrm{log}{A}$
47 44 46 oveq12d ${⊢}{x}={A}\to {\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}={\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}$
48 42 47 oveq12d ${⊢}{x}={A}\to {x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)={A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)$
49 41 48 oveq12d ${⊢}{x}={A}\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)=\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)$
50 eqid ${⊢}\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)=\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)$
51 ovex ${⊢}\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\in \mathrm{V}$
52 49 50 51 fvmpt3i ${⊢}{A}\in {ℝ}^{+}\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left({A}\right)=\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)$
53 52 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left({A}\right)=\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)$
54 1rp ${⊢}1\in {ℝ}^{+}$
55 fveq2 ${⊢}{x}=1\to ⌊{x}⌋=⌊1⌋$
56 1z ${⊢}1\in ℤ$
57 flid ${⊢}1\in ℤ\to ⌊1⌋=1$
58 56 57 ax-mp ${⊢}⌊1⌋=1$
59 55 58 syl6eq ${⊢}{x}=1\to ⌊{x}⌋=1$
60 59 oveq2d ${⊢}{x}=1\to \left(1\dots ⌊{x}⌋\right)=\left(1\dots 1\right)$
61 60 sumeq1d ${⊢}{x}=1\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}=\sum _{{n}=1}^{1}{\mathrm{log}{n}}^{2}$
62 0cn ${⊢}0\in ℂ$
63 fveq2 ${⊢}{n}=1\to \mathrm{log}{n}=\mathrm{log}1$
64 log1 ${⊢}\mathrm{log}1=0$
65 63 64 syl6eq ${⊢}{n}=1\to \mathrm{log}{n}=0$
66 65 sq0id ${⊢}{n}=1\to {\mathrm{log}{n}}^{2}=0$
67 66 fsum1 ${⊢}\left(1\in ℤ\wedge 0\in ℂ\right)\to \sum _{{n}=1}^{1}{\mathrm{log}{n}}^{2}=0$
68 56 62 67 mp2an ${⊢}\sum _{{n}=1}^{1}{\mathrm{log}{n}}^{2}=0$
69 61 68 syl6eq ${⊢}{x}=1\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}=0$
70 id ${⊢}{x}=1\to {x}=1$
71 fveq2 ${⊢}{x}=1\to \mathrm{log}{x}=\mathrm{log}1$
72 71 64 syl6eq ${⊢}{x}=1\to \mathrm{log}{x}=0$
73 72 sq0id ${⊢}{x}=1\to {\mathrm{log}{x}}^{2}=0$
74 72 oveq2d ${⊢}{x}=1\to 2\mathrm{log}{x}=2\cdot 0$
75 2t0e0 ${⊢}2\cdot 0=0$
76 74 75 syl6eq ${⊢}{x}=1\to 2\mathrm{log}{x}=0$
77 76 oveq2d ${⊢}{x}=1\to 2-2\mathrm{log}{x}=2-0$
78 25 subid1i ${⊢}2-0=2$
79 77 78 syl6eq ${⊢}{x}=1\to 2-2\mathrm{log}{x}=2$
80 73 79 oveq12d ${⊢}{x}=1\to {\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}=0+2$
81 25 addid2i ${⊢}0+2=2$
82 80 81 syl6eq ${⊢}{x}=1\to {\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}=2$
83 70 82 oveq12d ${⊢}{x}=1\to {x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)=1\cdot 2$
84 25 mulid2i ${⊢}1\cdot 2=2$
85 83 84 syl6eq ${⊢}{x}=1\to {x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)=2$
86 69 85 oveq12d ${⊢}{x}=1\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)=0-2$
87 df-neg ${⊢}-2=0-2$
88 86 87 syl6eqr ${⊢}{x}=1\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)=-2$
89 88 50 51 fvmpt3i ${⊢}1\in {ℝ}^{+}\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left(1\right)=-2$
90 54 89 mp1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left(1\right)=-2$
91 53 90 oveq12d ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left({A}\right)-\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left(1\right)=\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2$
92 91 fveq2d ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left({A}\right)-\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left(1\right)\right|=\left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2\right|$
93 ioorp ${⊢}\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$
94 93 eqcomi ${⊢}{ℝ}^{+}=\left(0,\mathrm{+\infty }\right)$
95 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
96 56 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 1\in ℤ$
97 1red ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 1\in ℝ$
98 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
99 98 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
100 1re ${⊢}1\in ℝ$
101 1nn0 ${⊢}1\in {ℕ}_{0}$
102 100 101 nn0addge1i ${⊢}1\le 1+1$
103 102 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 1\le 1+1$
104 0red ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 0\in ℝ$
105 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
106 105 adantl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℝ$
107 simpr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\in {ℝ}^{+}$
108 107 relogcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}{x}\in ℝ$
109 108 resqcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {\mathrm{log}{x}}^{2}\in ℝ$
110 remulcl ${⊢}\left(2\in ℝ\wedge \mathrm{log}{x}\in ℝ\right)\to 2\mathrm{log}{x}\in ℝ$
111 13 108 110 sylancr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}\in ℝ$
112 resubcl ${⊢}\left(2\in ℝ\wedge 2\mathrm{log}{x}\in ℝ\right)\to 2-2\mathrm{log}{x}\in ℝ$
113 13 111 112 sylancr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2-2\mathrm{log}{x}\in ℝ$
114 109 113 readdcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\in ℝ$
115 106 114 remulcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\in ℝ$
116 nnrp ${⊢}{x}\in ℕ\to {x}\in {ℝ}^{+}$
117 116 109 sylan2 ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in ℕ\right)\to {\mathrm{log}{x}}^{2}\in ℝ$
118 reelprrecn ${⊢}ℝ\in \left\{ℝ,ℂ\right\}$
119 118 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to ℝ\in \left\{ℝ,ℂ\right\}$
120 106 recnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℂ$
121 1red ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 1\in ℝ$
122 recn ${⊢}{x}\in ℝ\to {x}\in ℂ$
123 122 adantl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in ℝ\right)\to {x}\in ℂ$
124 1red ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in ℝ\right)\to 1\in ℝ$
125 119 dvmptid ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in ℝ⟼{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in ℝ⟼1\right)$
126 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
127 126 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {ℝ}^{+}\subseteq ℝ$
128 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
129 128 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
130 iooretop ${⊢}\left(0,\mathrm{+\infty }\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
131 93 130 eqeltrri ${⊢}{ℝ}^{+}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
132 131 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {ℝ}^{+}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
133 119 123 124 125 127 129 128 132 dvmptres ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼1\right)$
134 114 recnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\in ℂ$
135 resubcl ${⊢}\left(2\mathrm{log}{x}\in ℝ\wedge 2\in ℝ\right)\to 2\mathrm{log}{x}-2\in ℝ$
136 111 13 135 sylancl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}-2\in ℝ$
137 136 107 rerpdivcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \frac{2\mathrm{log}{x}-2}{{x}}\in ℝ$
138 109 recnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {\mathrm{log}{x}}^{2}\in ℂ$
139 111 recnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}\in ℂ$
140 107 rpreccld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \frac{1}{{x}}\in {ℝ}^{+}$
141 140 rpcnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \frac{1}{{x}}\in ℂ$
142 139 141 mulcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}\left(\frac{1}{{x}}\right)\in ℂ$
143 cnelprrecn ${⊢}ℂ\in \left\{ℝ,ℂ\right\}$
144 143 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to ℂ\in \left\{ℝ,ℂ\right\}$
145 108 recnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}{x}\in ℂ$
146 sqcl ${⊢}{y}\in ℂ\to {{y}}^{2}\in ℂ$
147 146 adantl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {y}\in ℂ\right)\to {{y}}^{2}\in ℂ$
148 simpr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {y}\in ℂ\right)\to {y}\in ℂ$
149 mulcl ${⊢}\left(2\in ℂ\wedge {y}\in ℂ\right)\to 2{y}\in ℂ$
150 25 148 149 sylancr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {y}\in ℂ\right)\to 2{y}\in ℂ$
151 dvrelog ${⊢}ℝ\mathrm{D}\left({log↾}_{{ℝ}^{+}}\right)=\left({x}\in {ℝ}^{+}⟼\frac{1}{{x}}\right)$
152 relogf1o ${⊢}\left({log↾}_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1 onto}{⟶}ℝ$
153 f1of ${⊢}\left({log↾}_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1 onto}{⟶}ℝ\to \left({log↾}_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$
154 152 153 mp1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left({log↾}_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$
155 154 feqmptd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {log↾}_{{ℝ}^{+}}=\left({x}\in {ℝ}^{+}⟼\left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)\right)$
156 fvres ${⊢}{x}\in {ℝ}^{+}\to \left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)=\mathrm{log}{x}$
157 156 mpteq2ia ${⊢}\left({x}\in {ℝ}^{+}⟼\left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)\right)=\left({x}\in {ℝ}^{+}⟼\mathrm{log}{x}\right)$
158 155 157 syl6eq ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {log↾}_{{ℝ}^{+}}=\left({x}\in {ℝ}^{+}⟼\mathrm{log}{x}\right)$
159 158 oveq2d ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to ℝ\mathrm{D}\left({log↾}_{{ℝ}^{+}}\right)=\frac{d\left({x}\in {ℝ}^{+}⟼\mathrm{log}{x}\right)}{{d}_{ℝ}{x}}$
160 151 159 syl5reqr ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼\mathrm{log}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼\frac{1}{{x}}\right)$
161 2nn ${⊢}2\in ℕ$
162 dvexp ${⊢}2\in ℕ\to \frac{d\left({y}\in ℂ⟼{{y}}^{2}\right)}{{d}_{ℂ}{y}}=\left({y}\in ℂ⟼2{{y}}^{2-1}\right)$
163 161 162 mp1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({y}\in ℂ⟼{{y}}^{2}\right)}{{d}_{ℂ}{y}}=\left({y}\in ℂ⟼2{{y}}^{2-1}\right)$
164 2m1e1 ${⊢}2-1=1$
165 164 oveq2i ${⊢}{{y}}^{2-1}={{y}}^{1}$
166 exp1 ${⊢}{y}\in ℂ\to {{y}}^{1}={y}$
167 165 166 syl5eq ${⊢}{y}\in ℂ\to {{y}}^{2-1}={y}$
168 167 oveq2d ${⊢}{y}\in ℂ\to 2{{y}}^{2-1}=2{y}$
169 168 mpteq2ia ${⊢}\left({y}\in ℂ⟼2{{y}}^{2-1}\right)=\left({y}\in ℂ⟼2{y}\right)$
170 163 169 syl6eq ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({y}\in ℂ⟼{{y}}^{2}\right)}{{d}_{ℂ}{y}}=\left({y}\in ℂ⟼2{y}\right)$
171 oveq1 ${⊢}{y}=\mathrm{log}{x}\to {{y}}^{2}={\mathrm{log}{x}}^{2}$
172 oveq2 ${⊢}{y}=\mathrm{log}{x}\to 2{y}=2\mathrm{log}{x}$
173 119 144 145 140 147 150 160 170 171 172 dvmptco ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼{\mathrm{log}{x}}^{2}\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼2\mathrm{log}{x}\left(\frac{1}{{x}}\right)\right)$
174 113 recnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2-2\mathrm{log}{x}\in ℂ$
175 ovexd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 0-2\left(\frac{1}{{x}}\right)\in \mathrm{V}$
176 2cnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\in ℂ$
177 0red ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 0\in ℝ$
178 2cnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in ℝ\right)\to 2\in ℂ$
179 0red ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in ℝ\right)\to 0\in ℝ$
180 2cnd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 2\in ℂ$
181 119 180 dvmptc ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in ℝ⟼2\right)}{{d}_{ℝ}{x}}=\left({x}\in ℝ⟼0\right)$
182 119 178 179 181 127 129 128 132 dvmptres ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼2\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼0\right)$
183 mulcl ${⊢}\left(2\in ℂ\wedge \frac{1}{{x}}\in ℂ\right)\to 2\left(\frac{1}{{x}}\right)\in ℂ$
184 25 141 183 sylancr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\left(\frac{1}{{x}}\right)\in ℂ$
185 119 145 140 160 180 dvmptcmul ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼2\mathrm{log}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼2\left(\frac{1}{{x}}\right)\right)$
186 119 176 177 182 139 184 185 dvmptsub ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼2-2\mathrm{log}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼0-2\left(\frac{1}{{x}}\right)\right)$
187 119 138 142 173 174 175 186 dvmptadd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼{\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼2\mathrm{log}{x}\left(\frac{1}{{x}}\right)+0-2\left(\frac{1}{{x}}\right)\right)$
188 139 176 141 subdird ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(2\mathrm{log}{x}-2\right)\left(\frac{1}{{x}}\right)=2\mathrm{log}{x}\left(\frac{1}{{x}}\right)-2\left(\frac{1}{{x}}\right)$
189 136 recnd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}-2\in ℂ$
190 rpne0 ${⊢}{x}\in {ℝ}^{+}\to {x}\ne 0$
191 190 adantl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\ne 0$
192 189 120 191 divrecd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \frac{2\mathrm{log}{x}-2}{{x}}=\left(2\mathrm{log}{x}-2\right)\left(\frac{1}{{x}}\right)$
193 df-neg ${⊢}-2\left(\frac{1}{{x}}\right)=0-2\left(\frac{1}{{x}}\right)$
194 193 oveq2i ${⊢}2\mathrm{log}{x}\left(\frac{1}{{x}}\right)+\left(-2\left(\frac{1}{{x}}\right)\right)=2\mathrm{log}{x}\left(\frac{1}{{x}}\right)+0-2\left(\frac{1}{{x}}\right)$
195 142 184 negsubd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}\left(\frac{1}{{x}}\right)+\left(-2\left(\frac{1}{{x}}\right)\right)=2\mathrm{log}{x}\left(\frac{1}{{x}}\right)-2\left(\frac{1}{{x}}\right)$
196 194 195 syl5eqr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}\left(\frac{1}{{x}}\right)+0-2\left(\frac{1}{{x}}\right)=2\mathrm{log}{x}\left(\frac{1}{{x}}\right)-2\left(\frac{1}{{x}}\right)$
197 188 192 196 3eqtr4rd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}\left(\frac{1}{{x}}\right)+0-2\left(\frac{1}{{x}}\right)=\frac{2\mathrm{log}{x}-2}{{x}}$
198 197 mpteq2dva ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left({x}\in {ℝ}^{+}⟼2\mathrm{log}{x}\left(\frac{1}{{x}}\right)+0-2\left(\frac{1}{{x}}\right)\right)=\left({x}\in {ℝ}^{+}⟼\frac{2\mathrm{log}{x}-2}{{x}}\right)$
199 187 198 eqtrd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼{\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼\frac{2\mathrm{log}{x}-2}{{x}}\right)$
200 119 120 121 133 134 137 199 dvmptmul ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼1\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)+\left(\frac{2\mathrm{log}{x}-2}{{x}}\right){x}\right)$
201 134 mulid2d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 1\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)={\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}$
202 138 139 176 subsub2d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to {\mathrm{log}{x}}^{2}-\left(2\mathrm{log}{x}-2\right)={\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}$
203 201 202 eqtr4d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 1\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)={\mathrm{log}{x}}^{2}-\left(2\mathrm{log}{x}-2\right)$
204 189 120 191 divcan1d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\frac{2\mathrm{log}{x}-2}{{x}}\right){x}=2\mathrm{log}{x}-2$
205 203 204 oveq12d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 1\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)+\left(\frac{2\mathrm{log}{x}-2}{{x}}\right){x}=\left({\mathrm{log}{x}}^{2}-\left(2\mathrm{log}{x}-2\right)\right)+2\mathrm{log}{x}-2$
206 138 189 npcand ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left({\mathrm{log}{x}}^{2}-\left(2\mathrm{log}{x}-2\right)\right)+2\mathrm{log}{x}-2={\mathrm{log}{x}}^{2}$
207 205 206 eqtrd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge {x}\in {ℝ}^{+}\right)\to 1\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)+\left(\frac{2\mathrm{log}{x}-2}{{x}}\right){x}={\mathrm{log}{x}}^{2}$
208 207 mpteq2dva ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left({x}\in {ℝ}^{+}⟼1\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)+\left(\frac{2\mathrm{log}{x}-2}{{x}}\right){x}\right)=\left({x}\in {ℝ}^{+}⟼{\mathrm{log}{x}}^{2}\right)$
209 200 208 eqtrd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \frac{d\left({x}\in {ℝ}^{+}⟼{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)}{{d}_{ℝ}{x}}=\left({x}\in {ℝ}^{+}⟼{\mathrm{log}{x}}^{2}\right)$
210 fveq2 ${⊢}{x}={n}\to \mathrm{log}{x}=\mathrm{log}{n}$
211 210 oveq1d ${⊢}{x}={n}\to {\mathrm{log}{x}}^{2}={\mathrm{log}{n}}^{2}$
212 simp32 ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to {x}\le {n}$
213 simp2l ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to {x}\in {ℝ}^{+}$
214 simp2r ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to {n}\in {ℝ}^{+}$
215 213 214 logled ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to \left({x}\le {n}↔\mathrm{log}{x}\le \mathrm{log}{n}\right)$
216 212 215 mpbid ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\le \mathrm{log}{n}$
217 213 relogcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in ℝ$
218 214 relogcld ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to \mathrm{log}{n}\in ℝ$
219 simp31 ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to 1\le {x}$
220 logleb ${⊢}\left(1\in {ℝ}^{+}\wedge {x}\in {ℝ}^{+}\right)\to \left(1\le {x}↔\mathrm{log}1\le \mathrm{log}{x}\right)$
221 54 213 220 sylancr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to \left(1\le {x}↔\mathrm{log}1\le \mathrm{log}{x}\right)$
222 219 221 mpbid ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to \mathrm{log}1\le \mathrm{log}{x}$
223 64 222 eqbrtrrid ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to 0\le \mathrm{log}{x}$
224 214 rpred ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to {n}\in ℝ$
225 1red ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to 1\in ℝ$
226 213 rpred ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to {x}\in ℝ$
227 225 226 224 219 212 letrd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to 1\le {n}$
228 224 227 logge0d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to 0\le \mathrm{log}{n}$
229 217 218 223 228 le2sqd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to \left(\mathrm{log}{x}\le \mathrm{log}{n}↔{\mathrm{log}{x}}^{2}\le {\mathrm{log}{n}}^{2}\right)$
230 216 229 mpbid ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\wedge \left(1\le {x}\wedge {x}\le {n}\wedge {n}\le \mathrm{+\infty }\right)\right)\to {\mathrm{log}{x}}^{2}\le {\mathrm{log}{n}}^{2}$
231 relogcl ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℝ$
232 231 ad2antrl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \mathrm{log}{x}\in ℝ$
233 232 sqge0d ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to 0\le {\mathrm{log}{x}}^{2}$
234 54 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 1\in {ℝ}^{+}$
235 simpl ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {A}\in {ℝ}^{+}$
236 1le1 ${⊢}1\le 1$
237 236 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 1\le 1$
238 simpr ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 1\le {A}$
239 9 rexrd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {A}\in {ℝ}^{*}$
240 pnfge ${⊢}{A}\in {ℝ}^{*}\to {A}\le \mathrm{+\infty }$
241 239 240 syl ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to {A}\le \mathrm{+\infty }$
242 94 95 96 97 99 103 104 115 109 117 209 211 230 50 233 234 235 237 238 241 44 dvfsum2 ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left({A}\right)-\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}{n}}^{2}-{x}\left({\mathrm{log}{x}}^{2}+2-2\mathrm{log}{x}\right)\right)\left(1\right)\right|\le {\mathrm{log}{A}}^{2}$
243 92 242 eqbrtrrd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)--2\right|\le {\mathrm{log}{A}}^{2}$
244 24 29 12 38 243 letrd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-2\le {\mathrm{log}{A}}^{2}$
245 13 a1i ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to 2\in ℝ$
246 22 245 12 lesubaddd ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left(\left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|-2\le {\mathrm{log}{A}}^{2}↔\left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|\le {\mathrm{log}{A}}^{2}+2\right)$
247 244 246 mpbid ${⊢}\left({A}\in {ℝ}^{+}\wedge 1\le {A}\right)\to \left|\sum _{{n}=1}^{⌊{A}⌋}{\mathrm{log}{n}}^{2}-{A}\left({\mathrm{log}{A}}^{2}+2-2\mathrm{log}{A}\right)\right|\le {\mathrm{log}{A}}^{2}+2$