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⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|\le {\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 \mathbb{N}$$
3	2	adantl	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge n\in \left(1\dots ⌊A⌋\right)\right)\to n\in \mathbb{N}$$
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 \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 {\log n}^2\in ℝ$$
7	1 6	fsumrecl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \sum _{n=1}^{⌊A⌋}{\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 \log A\in ℝ$$
11	10	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log A\in ℝ$$
12	11	resqcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to {\log A}^2\in ℝ$$
13		2re	$$⊢2\in ℝ$$
14		remulcl	$$⊢\left(2\in ℝ\wedge \log A\in ℝ\right)\to 2\log A\in ℝ$$
15	13 11 14	sylancr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 2\log A\in ℝ$$
16		resubcl	$$⊢\left(2\in ℝ\wedge 2\log A\in ℝ\right)\to 2-2\log A\in ℝ$$
17	13 15 16	sylancr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 2-2\log A\in ℝ$$
18	12 17	readdcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to {\log A}^2+2-2\log A\in ℝ$$
19	9 18	remulcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\left({\log A}^2+2-2\log A\right)\in ℝ$$
20	7 19	resubcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\in ℝ$$
21	20	recnd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\in ℂ$$
22	21	abscld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|\in ℝ$$
23		resubcl	$$⊢\left(\left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|\in ℝ\wedge 2\in ℝ\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\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⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|-2\in ℝ$$
25		2cn	$$⊢2\in ℂ$$
26	25	negcli	$$⊢-2\in ℂ$$
27		subcl	$$⊢\left(\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\in ℂ\wedge -2\in ℂ\right)\to \sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)--2\in ℂ$$
28	21 26 27	sylancl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)--2\in ℂ$$
29	28	abscld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\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⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|-\left|-2\right|=\left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|-2$$
36		abs2dif	$$⊢\left(\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\in ℂ\wedge -2\in ℂ\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|-\left|-2\right|\le \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)--2\right|$$
37	21 26 36	sylancl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|-\left|-2\right|\le \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)--2\right|$$
38	35 37	eqbrtrrid	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|-2\le \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\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⌋}{\log n}^2=\sum _{n=1}^{⌊A⌋}{\log n}^2$$
42		id	$$⊢x=A\to x=A$$
43		fveq2	$$⊢x=A\to \log x=\log A$$
44	43	oveq1d	$$⊢x=A\to {\log x}^2={\log A}^2$$
45	43	oveq2d	$$⊢x=A\to 2\log x=2\log A$$
46	45	oveq2d	$$⊢x=A\to 2-2\log x=2-2\log A$$
47	44 46	oveq12d	$$⊢x=A\to {\log x}^2+2-2\log x={\log A}^2+2-2\log A$$
48	42 47	oveq12d	$$⊢x=A\to x\left({\log x}^2+2-2\log x\right)=A\left({\log A}^2+2-2\log A\right)$$
49	41 48	oveq12d	$$⊢x=A\to \sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)=\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)$$
50		eqid	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)$$
51		ovex	$$⊢\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\in \mathrm{V}$$
52	49 50 51	fvmpt3i	$$⊢A\in {ℝ}^{+}\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)\left(A\right)=\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)$$
53	52	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)\left(A\right)=\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)$$
54		1rp	$$⊢1\in {ℝ}^{+}$$
55		fveq2	$$⊢x=1\to ⌊x⌋=⌊1⌋$$
56		1z	$$⊢1\in \mathbb{Z}$$
57		flid	$$⊢1\in \mathbb{Z}\to ⌊1⌋=1$$
58	56 57	ax-mp	$$⊢⌊1⌋=1$$
59	55 58	eqtrdi	$$⊢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⌋}{\log n}^2=\sum _{n=1}^1{\log n}^2$$
62		0cn	$$⊢0\in ℂ$$
63		fveq2	$$⊢n=1\to \log n=\log 1$$
64		log1	$$⊢\log 1=0$$
65	63 64	eqtrdi	$$⊢n=1\to \log n=0$$
66	65	sq0id	$$⊢n=1\to {\log n}^2=0$$
67	66	fsum1	$$⊢\left(1\in \mathbb{Z}\wedge 0\in ℂ\right)\to \sum _{n=1}^1{\log n}^2=0$$
68	56 62 67	mp2an	$$⊢\sum _{n=1}^1{\log n}^2=0$$
69	61 68	eqtrdi	$$⊢x=1\to \sum _{n=1}^{⌊x⌋}{\log n}^2=0$$
70		id	$$⊢x=1\to x=1$$
71		fveq2	$$⊢x=1\to \log x=\log 1$$
72	71 64	eqtrdi	$$⊢x=1\to \log x=0$$
73	72	sq0id	$$⊢x=1\to {\log x}^2=0$$
74	72	oveq2d	$$⊢x=1\to 2\log x=2\cdot 0$$
75		2t0e0	$$⊢2\cdot 0=0$$
76	74 75	eqtrdi	$$⊢x=1\to 2\log x=0$$
77	76	oveq2d	$$⊢x=1\to 2-2\log x=2-0$$
78	25	subid1i	$$⊢2-0=2$$
79	77 78	eqtrdi	$$⊢x=1\to 2-2\log x=2$$
80	73 79	oveq12d	$$⊢x=1\to {\log x}^2+2-2\log x=0+2$$
81	25	addid2i	$$⊢0+2=2$$
82	80 81	eqtrdi	$$⊢x=1\to {\log x}^2+2-2\log x=2$$
83	70 82	oveq12d	$$⊢x=1\to x\left({\log x}^2+2-2\log x\right)=1\cdot 2$$
84	25	mulid2i	$$⊢1\cdot 2=2$$
85	83 84	eqtrdi	$$⊢x=1\to x\left({\log x}^2+2-2\log x\right)=2$$
86	69 85	oveq12d	$$⊢x=1\to \sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)=0-2$$
87		df-neg	$$⊢-2=0-2$$
88	86 87	eqtr4di	$$⊢x=1\to \sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)=-2$$
89	88 50 51	fvmpt3i	$$⊢1\in {ℝ}^{+}\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\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⌋}{\log n}^2-x\left({\log x}^2+2-2\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⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)\left(A\right)-\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)\left(1\right)=\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)--2$$
92	91	fveq2d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)\left(A\right)-\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)\left(1\right)\right|=\left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)--2\right|$$
93		ioorp	$$⊢\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$$
94	93	eqcomi	$$⊢{ℝ}^{+}=\left(0,\mathrm{+\infty }\right)$$
95		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
96	56	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 1\in \mathbb{Z}$$
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 {\mathbb{N}}_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 \log x\in ℝ$$
109	108	resqcld	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to {\log x}^2\in ℝ$$
110		remulcl	$$⊢\left(2\in ℝ\wedge \log x\in ℝ\right)\to 2\log x\in ℝ$$
111	13 108 110	sylancr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to 2\log x\in ℝ$$
112		resubcl	$$⊢\left(2\in ℝ\wedge 2\log x\in ℝ\right)\to 2-2\log x\in ℝ$$
113	13 111 112	sylancr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to 2-2\log x\in ℝ$$
114	109 113	readdcld	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to {\log x}^2+2-2\log x\in ℝ$$
115	106 114	remulcld	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to x\left({\log x}^2+2-2\log x\right)\in ℝ$$
116		nnrp	$$⊢x\in \mathbb{N}\to x\in {ℝ}^{+}$$
117	116 109	sylan2	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in \mathbb{N}\right)\to {\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){\upharpoonright }_{𝑡}ℝ$$
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 {\log x}^2+2-2\log x\in ℂ$$
135		resubcl	$$⊢\left(2\log x\in ℝ\wedge 2\in ℝ\right)\to 2\log x-2\in ℝ$$
136	111 13 135	sylancl	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to 2\log x-2\in ℝ$$
137	136 107	rerpdivcld	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to \frac{2\log x-2}{x}\in ℝ$$
138	109	recnd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to {\log x}^2\in ℂ$$
139	111	recnd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to 2\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\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 \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 2y\in ℂ$$
150	25 148 149	sylancr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge y\in ℂ\right)\to 2y\in ℂ$$
151		relogf1o	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$
152		f1of	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
153	151 152	mp1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
154	153	feqmptd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to {log\upharpoonright }_{{ℝ}^{+}}=\left(x\in {ℝ}^{+}⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)\right)$$
155		fvres	$$⊢x\in {ℝ}^{+}\to \left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)=\log x$$
156	155	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)\right)=\left(x\in {ℝ}^{+}⟼\log x\right)$$
157	154 156	eqtrdi	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to {log\upharpoonright }_{{ℝ}^{+}}=\left(x\in {ℝ}^{+}⟼\log x\right)$$
158	157	oveq2d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\frac{d\left(x\in {ℝ}^{+}⟼\log x\right)}{d_{ℝ}x}$$
159		dvrelog	$$⊢ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
160	158 159	eqtr3di	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \frac{d\left(x\in {ℝ}^{+}⟼\log x\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
161		2nn	$$⊢2\in \mathbb{N}$$
162		dvexp	$$⊢2\in \mathbb{N}\to \frac{d\left(y\in ℂ⟼y^2\right)}{d_{ℂ}y}=\left(y\in ℂ⟼2y^{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 ℂ⟼2y^{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 2y^{2-1}=2y$$
169	168	mpteq2ia	$$⊢\left(y\in ℂ⟼2y^{2-1}\right)=\left(y\in ℂ⟼2y\right)$$
170	163 169	eqtrdi	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \frac{d\left(y\in ℂ⟼y^2\right)}{d_{ℂ}y}=\left(y\in ℂ⟼2y\right)$$
171		oveq1	$$⊢y=\log x\to y^2={\log x}^2$$
172		oveq2	$$⊢y=\log x\to 2y=2\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 {ℝ}^{+}⟼{\log x}^2\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼2\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\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\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\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 {ℝ}^{+}⟼{\log x}^2+2-2\log x\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼2\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\log x-2\right)\left(\frac{1}{x}\right)=2\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\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\log x-2}{x}=\left(2\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\log x\left(\frac{1}{x}\right)+\left(-2\left(\frac{1}{x}\right)\right)=2\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\log x\left(\frac{1}{x}\right)+\left(-2\left(\frac{1}{x}\right)\right)=2\log x\left(\frac{1}{x}\right)-2\left(\frac{1}{x}\right)$$
196	194 195	eqtr3id	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to 2\log x\left(\frac{1}{x}\right)+0-2\left(\frac{1}{x}\right)=2\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\log x\left(\frac{1}{x}\right)+0-2\left(\frac{1}{x}\right)=\frac{2\log x-2}{x}$$
198	197	mpteq2dva	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(x\in {ℝ}^{+}⟼2\log x\left(\frac{1}{x}\right)+0-2\left(\frac{1}{x}\right)\right)=\left(x\in {ℝ}^{+}⟼\frac{2\log x-2}{x}\right)$$
199	187 198	eqtrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \frac{d\left(x\in {ℝ}^{+}⟼{\log x}^2+2-2\log x\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\frac{2\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({\log x}^2+2-2\log x\right)\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼1\left({\log x}^2+2-2\log x\right)+\left(\frac{2\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({\log x}^2+2-2\log x\right)={\log x}^2+2-2\log x$$
202	138 139 176	subsub2d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to {\log x}^2-\left(2\log x-2\right)={\log x}^2+2-2\log x$$
203	201 202	eqtr4d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to 1\left({\log x}^2+2-2\log x\right)={\log x}^2-\left(2\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\log x-2}{x}\right)x=2\log x-2$$
205	203 204	oveq12d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to 1\left({\log x}^2+2-2\log x\right)+\left(\frac{2\log x-2}{x}\right)x=\left({\log x}^2-\left(2\log x-2\right)\right)+2\log x-2$$
206	138 189	npcand	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to \left({\log x}^2-\left(2\log x-2\right)\right)+2\log x-2={\log x}^2$$
207	205 206	eqtrd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to 1\left({\log x}^2+2-2\log x\right)+\left(\frac{2\log x-2}{x}\right)x={\log x}^2$$
208	207	mpteq2dva	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(x\in {ℝ}^{+}⟼1\left({\log x}^2+2-2\log x\right)+\left(\frac{2\log x-2}{x}\right)x\right)=\left(x\in {ℝ}^{+}⟼{\log x}^2\right)$$
209	200 208	eqtrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \frac{d\left(x\in {ℝ}^{+}⟼x\left({\log x}^2+2-2\log x\right)\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼{\log x}^2\right)$$
210		fveq2	$$⊢x=n\to \log x=\log n$$
211	210	oveq1d	$$⊢x=n\to {\log x}^2={\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\leftrightarrow \log x\le \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 \log x\le \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 \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 \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\leftrightarrow \log 1\le \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\leftrightarrow \log 1\le \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 \log 1\le \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 \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 \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(\log x\le \log n\leftrightarrow {\log x}^2\le {\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 {\log x}^2\le {\log n}^2$$
231		relogcl	$$⊢x\in {ℝ}^{+}\to \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 \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 {\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⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)\left(A\right)-\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}{\log n}^2-x\left({\log x}^2+2-2\log x\right)\right)\left(1\right)\right|\le {\log A}^2$$
243	92 242	eqbrtrrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)--2\right|\le {\log A}^2$$
244	24 29 12 38 243	letrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|-2\le {\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⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|-2\le {\log A}^2\leftrightarrow \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|\le {\log A}^2+2\right)$$
247	244 246	mpbid	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\sum _{n=1}^{⌊A⌋}{\log n}^2-A\left({\log A}^2+2-2\log A\right)\right|\le {\log A}^2+2$$