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 ( ( 𝐴 ∈ ℝ+ ∧ 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 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
129 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
130 iooretop ⊢ ( 0 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
131 93 130 eqeltrri ⊢ ℝ+ ∈ ( topGen ‘ ran (,) )
132 131 a1i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ℝ+ ∈ ( topGen ‘ ran (,) ) )
133 119 123 124 125 127 128 129 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 128 129 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 ) )