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	$⊢ (A \in ℝ^{+} \land 1 \leq A) \to \|\sum_{n = 1}^{⌊A⌋} {\log n}^{2} - A ({\log A}^{2} + 2 - 2 \log A)\| \leq {\log A}^{2} + 2$

Proof

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

Metamath Proof Explorer

Theorem log2sumbnd

Proof