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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑛 ) ↑ 2 ) − ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ 𝐴 ) ) ) ) ) ) ) ≤ ( ( ( log ‘ 𝐴 ) ↑ 2 ) + 2 ) )

Proof

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