MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  log2sumbnd Structured version   Visualization version   GIF version

Theorem log2sumbnd 26037
Description: Bound on the difference between Σ𝑛𝐴, log↑2(𝑛) and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016.)
Assertion
Ref Expression
log2sumbnd ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) ≤ (((log‘𝐴)↑2) + 2))
Distinct variable group:   𝐴,𝑛

Proof of Theorem log2sumbnd
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 13331 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (1...(⌊‘𝐴)) ∈ Fin)
2 elfznn 12926 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℕ)
32adantl 482 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
43nnrpd 12419 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ+)
54relogcld 25122 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (log‘𝑛) ∈ ℝ)
65resqcld 13601 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((log‘𝑛)↑2) ∈ ℝ)
71, 6fsumrecl 15081 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) ∈ ℝ)
8 rpre 12387 . . . . . . . . 9 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
98adantr 481 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ)
10 relogcl 25075 . . . . . . . . . . 11 (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
1110adantr 481 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℝ)
1211resqcld 13601 . . . . . . . . 9 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((log‘𝐴)↑2) ∈ ℝ)
13 2re 11700 . . . . . . . . . 10 2 ∈ ℝ
14 remulcl 10611 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ (log‘𝐴) ∈ ℝ) → (2 · (log‘𝐴)) ∈ ℝ)
1513, 11, 14sylancr 587 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (2 · (log‘𝐴)) ∈ ℝ)
16 resubcl 10939 . . . . . . . . . 10 ((2 ∈ ℝ ∧ (2 · (log‘𝐴)) ∈ ℝ) → (2 − (2 · (log‘𝐴))) ∈ ℝ)
1713, 15, 16sylancr 587 . . . . . . . . 9 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (2 − (2 · (log‘𝐴))) ∈ ℝ)
1812, 17readdcld 10659 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))) ∈ ℝ)
199, 18remulcld 10660 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))) ∈ ℝ)
207, 19resubcld 11057 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) ∈ ℝ)
2120recnd 10658 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) ∈ ℂ)
2221abscld 14786 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) ∈ ℝ)
23 resubcl 10939 . . . 4 (((abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) ∈ ℝ ∧ 2 ∈ ℝ) → ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) − 2) ∈ ℝ)
2422, 13, 23sylancl 586 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) − 2) ∈ ℝ)
25 2cn 11701 . . . . . 6 2 ∈ ℂ
2625negcli 10943 . . . . 5 -2 ∈ ℂ
27 subcl 10874 . . . . 5 (((Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) ∈ ℂ ∧ -2 ∈ ℂ) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) − -2) ∈ ℂ)
2821, 26, 27sylancl 586 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) − -2) ∈ ℂ)
2928abscld 14786 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) − -2)) ∈ ℝ)
3025absnegi 14750 . . . . . 6 (abs‘-2) = (abs‘2)
31 0le2 11728 . . . . . . 7 0 ≤ 2
32 absid 14646 . . . . . . 7 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
3313, 31, 32mp2an 688 . . . . . 6 (abs‘2) = 2
3430, 33eqtri 2849 . . . . 5 (abs‘-2) = 2
3534oveq2i 7159 . . . 4 ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) − (abs‘-2)) = ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) − 2)
36 abs2dif 14682 . . . . 5 (((Σ𝑛 ∈ (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)))
3721, 26, 36sylancl 586 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) − (abs‘-2)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) − -2)))
3835, 37eqbrtrrid 5099 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) − 2) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) − -2)))
39 fveq2 6667 . . . . . . . . . . 11 (𝑥 = 𝐴 → (⌊‘𝑥) = (⌊‘𝐴))
4039oveq2d 7164 . . . . . . . . . 10 (𝑥 = 𝐴 → (1...(⌊‘𝑥)) = (1...(⌊‘𝐴)))
4140sumeq1d 15048 . . . . . . . . 9 (𝑥 = 𝐴 → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) = Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2))
42 id 22 . . . . . . . . . 10 (𝑥 = 𝐴𝑥 = 𝐴)
43 fveq2 6667 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴))
4443oveq1d 7163 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((log‘𝑥)↑2) = ((log‘𝐴)↑2))
4543oveq2d 7164 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (2 · (log‘𝑥)) = (2 · (log‘𝐴)))
4645oveq2d 7164 . . . . . . . . . . 11 (𝑥 = 𝐴 → (2 − (2 · (log‘𝑥))) = (2 − (2 · (log‘𝐴))))
4744, 46oveq12d 7166 . . . . . . . . . 10 (𝑥 = 𝐴 → (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))) = (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))
4842, 47oveq12d 7166 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) = (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))
4941, 48oveq12d 7166 . . . . . . . 8 (𝑥 = 𝐴 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))))
50 eqid 2826 . . . . . . . 8 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))))
51 ovex 7181 . . . . . . . 8 𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))) ∈ V
5249, 50, 51fvmpt3i 6770 . . . . . . 7 (𝐴 ∈ ℝ+ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))))
5352adantr 481 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))))
54 1rp 12383 . . . . . . 7 1 ∈ ℝ+
55 fveq2 6667 . . . . . . . . . . . . . 14 (𝑥 = 1 → (⌊‘𝑥) = (⌊‘1))
56 1z 12001 . . . . . . . . . . . . . . 15 1 ∈ ℤ
57 flid 13168 . . . . . . . . . . . . . . 15 (1 ∈ ℤ → (⌊‘1) = 1)
5856, 57ax-mp 5 . . . . . . . . . . . . . 14 (⌊‘1) = 1
5955, 58syl6eq 2877 . . . . . . . . . . . . 13 (𝑥 = 1 → (⌊‘𝑥) = 1)
6059oveq2d 7164 . . . . . . . . . . . 12 (𝑥 = 1 → (1...(⌊‘𝑥)) = (1...1))
6160sumeq1d 15048 . . . . . . . . . . 11 (𝑥 = 1 → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) = Σ𝑛 ∈ (1...1)((log‘𝑛)↑2))
62 0cn 10622 . . . . . . . . . . . 12 0 ∈ ℂ
63 fveq2 6667 . . . . . . . . . . . . . . 15 (𝑛 = 1 → (log‘𝑛) = (log‘1))
64 log1 25085 . . . . . . . . . . . . . . 15 (log‘1) = 0
6563, 64syl6eq 2877 . . . . . . . . . . . . . 14 (𝑛 = 1 → (log‘𝑛) = 0)
6665sq0id 13547 . . . . . . . . . . . . 13 (𝑛 = 1 → ((log‘𝑛)↑2) = 0)
6766fsum1 15092 . . . . . . . . . . . 12 ((1 ∈ ℤ ∧ 0 ∈ ℂ) → Σ𝑛 ∈ (1...1)((log‘𝑛)↑2) = 0)
6856, 62, 67mp2an 688 . . . . . . . . . . 11 Σ𝑛 ∈ (1...1)((log‘𝑛)↑2) = 0
6961, 68syl6eq 2877 . . . . . . . . . 10 (𝑥 = 1 → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) = 0)
70 id 22 . . . . . . . . . . . 12 (𝑥 = 1 → 𝑥 = 1)
71 fveq2 6667 . . . . . . . . . . . . . . . 16 (𝑥 = 1 → (log‘𝑥) = (log‘1))
7271, 64syl6eq 2877 . . . . . . . . . . . . . . 15 (𝑥 = 1 → (log‘𝑥) = 0)
7372sq0id 13547 . . . . . . . . . . . . . 14 (𝑥 = 1 → ((log‘𝑥)↑2) = 0)
7472oveq2d 7164 . . . . . . . . . . . . . . . . 17 (𝑥 = 1 → (2 · (log‘𝑥)) = (2 · 0))
75 2t0e0 11795 . . . . . . . . . . . . . . . . 17 (2 · 0) = 0
7674, 75syl6eq 2877 . . . . . . . . . . . . . . . 16 (𝑥 = 1 → (2 · (log‘𝑥)) = 0)
7776oveq2d 7164 . . . . . . . . . . . . . . 15 (𝑥 = 1 → (2 − (2 · (log‘𝑥))) = (2 − 0))
7825subid1i 10947 . . . . . . . . . . . . . . 15 (2 − 0) = 2
7977, 78syl6eq 2877 . . . . . . . . . . . . . 14 (𝑥 = 1 → (2 − (2 · (log‘𝑥))) = 2)
8073, 79oveq12d 7166 . . . . . . . . . . . . 13 (𝑥 = 1 → (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))) = (0 + 2))
8125addid2i 10817 . . . . . . . . . . . . 13 (0 + 2) = 2
8280, 81syl6eq 2877 . . . . . . . . . . . 12 (𝑥 = 1 → (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))) = 2)
8370, 82oveq12d 7166 . . . . . . . . . . 11 (𝑥 = 1 → (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) = (1 · 2))
8425mulid2i 10635 . . . . . . . . . . 11 (1 · 2) = 2
8583, 84syl6eq 2877 . . . . . . . . . 10 (𝑥 = 1 → (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) = 2)
8669, 85oveq12d 7166 . . . . . . . . 9 (𝑥 = 1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))) = (0 − 2))
87 df-neg 10862 . . . . . . . . 9 -2 = (0 − 2)
8886, 87syl6eqr 2879 . . . . . . . 8 (𝑥 = 1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))) = -2)
8988, 50, 51fvmpt3i 6770 . . . . . . 7 (1 ∈ ℝ+ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))))‘1) = -2)
9054, 89mp1i 13 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))))‘1) = -2)
9153, 90oveq12d 7166 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 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))
9291fveq2d 6671 . . . 4 ((𝐴 ∈ ℝ+ ∧ 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 12804 . . . . . 6 (0(,)+∞) = ℝ+
9493eqcomi 2835 . . . . 5 + = (0(,)+∞)
95 nnuz 12270 . . . . 5 ℕ = (ℤ‘1)
9656a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ∈ ℤ)
97 1red 10631 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ)
98 pnfxr 10684 . . . . . 6 +∞ ∈ ℝ*
9998a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → +∞ ∈ ℝ*)
100 1re 10630 . . . . . . 7 1 ∈ ℝ
101 1nn0 11902 . . . . . . 7 1 ∈ ℕ0
102100, 101nn0addge1i 11934 . . . . . 6 1 ≤ (1 + 1)
103102a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ≤ (1 + 1))
104 0red 10633 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 0 ∈ ℝ)
105 rpre 12387 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
106105adantl 482 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
107 simpr 485 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
108107relogcld 25122 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
109108resqcld 13601 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑2) ∈ ℝ)
110 remulcl 10611 . . . . . . . . 9 ((2 ∈ ℝ ∧ (log‘𝑥) ∈ ℝ) → (2 · (log‘𝑥)) ∈ ℝ)
11113, 108, 110sylancr 587 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 · (log‘𝑥)) ∈ ℝ)
112 resubcl 10939 . . . . . . . 8 ((2 ∈ ℝ ∧ (2 · (log‘𝑥)) ∈ ℝ) → (2 − (2 · (log‘𝑥))) ∈ ℝ)
11313, 111, 112sylancr 587 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 − (2 · (log‘𝑥))) ∈ ℝ)
114109, 113readdcld 10659 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))) ∈ ℝ)
115106, 114remulcld 10660 . . . . 5 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) ∈ ℝ)
116 nnrp 12390 . . . . . 6 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ+)
117116, 109sylan2 592 . . . . 5 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℕ) → ((log‘𝑥)↑2) ∈ ℝ)
118 reelprrecn 10618 . . . . . . . 8 ℝ ∈ {ℝ, ℂ}
119118a1i 11 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ℝ ∈ {ℝ, ℂ})
120106recnd 10658 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
121 1red 10631 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℝ)
122 recn 10616 . . . . . . . . 9 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
123122adantl 482 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
124 1red 10631 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
125119dvmptid 24472 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
126 rpssre 12386 . . . . . . . . 9 + ⊆ ℝ
127126a1i 11 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ℝ+ ⊆ ℝ)
128 eqid 2826 . . . . . . . . 9 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
129128tgioo2 23329 . . . . . . . 8 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
130 iooretop 23292 . . . . . . . . . 10 (0(,)+∞) ∈ (topGen‘ran (,))
13193, 130eqeltrri 2915 . . . . . . . . 9 + ∈ (topGen‘ran (,))
132131a1i 11 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ℝ+ ∈ (topGen‘ran (,)))
133119, 123, 124, 125, 127, 129, 128, 132dvmptres 24478 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+𝑥)) = (𝑥 ∈ ℝ+ ↦ 1))
134114recnd 10658 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))) ∈ ℂ)
135 resubcl 10939 . . . . . . . . 9 (((2 · (log‘𝑥)) ∈ ℝ ∧ 2 ∈ ℝ) → ((2 · (log‘𝑥)) − 2) ∈ ℝ)
136111, 13, 135sylancl 586 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((2 · (log‘𝑥)) − 2) ∈ ℝ)
137136, 107rerpdivcld 12452 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((2 · (log‘𝑥)) − 2) / 𝑥) ∈ ℝ)
138109recnd 10658 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑2) ∈ ℂ)
139111recnd 10658 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 · (log‘𝑥)) ∈ ℂ)
140107rpreccld 12431 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
141140rpcnd 12423 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℂ)
142139, 141mulcld 10650 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((2 · (log‘𝑥)) · (1 / 𝑥)) ∈ ℂ)
143 cnelprrecn 10619 . . . . . . . . . . 11 ℂ ∈ {ℝ, ℂ}
144143a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ℂ ∈ {ℝ, ℂ})
145108recnd 10658 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
146 sqcl 13474 . . . . . . . . . . 11 (𝑦 ∈ ℂ → (𝑦↑2) ∈ ℂ)
147146adantl 482 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑦 ∈ ℂ) → (𝑦↑2) ∈ ℂ)
148 simpr 485 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
149 mulcl 10610 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (2 · 𝑦) ∈ ℂ)
15025, 148, 149sylancr 587 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑦 ∈ ℂ) → (2 · 𝑦) ∈ ℂ)
151 dvrelog 25136 . . . . . . . . . . 11 (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))
152 relogf1o 25066 . . . . . . . . . . . . . . 15 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
153 f1of 6612 . . . . . . . . . . . . . . 15 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
154152, 153mp1i 13 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log ↾ ℝ+):ℝ+⟶ℝ)
155154feqmptd 6730 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)))
156 fvres 6686 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+ → ((log ↾ ℝ+)‘𝑥) = (log‘𝑥))
157156mpteq2ia 5154 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥))
158155, 157syl6eq 2877 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)))
159158oveq2d 7164 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (log ↾ ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝑥))))
160151, 159syl5reqr 2876 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
161 2nn 11699 . . . . . . . . . . . 12 2 ∈ ℕ
162 dvexp 24468 . . . . . . . . . . . 12 (2 ∈ ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2 · (𝑦↑(2 − 1)))))
163161, 162mp1i 13 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2 · (𝑦↑(2 − 1)))))
164 2m1e1 11752 . . . . . . . . . . . . . . 15 (2 − 1) = 1
165164oveq2i 7159 . . . . . . . . . . . . . 14 (𝑦↑(2 − 1)) = (𝑦↑1)
166 exp1 13425 . . . . . . . . . . . . . 14 (𝑦 ∈ ℂ → (𝑦↑1) = 𝑦)
167165, 166syl5eq 2873 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → (𝑦↑(2 − 1)) = 𝑦)
168167oveq2d 7164 . . . . . . . . . . . 12 (𝑦 ∈ ℂ → (2 · (𝑦↑(2 − 1))) = (2 · 𝑦))
169168mpteq2ia 5154 . . . . . . . . . . 11 (𝑦 ∈ ℂ ↦ (2 · (𝑦↑(2 − 1)))) = (𝑦 ∈ ℂ ↦ (2 · 𝑦))
170163, 169syl6eq 2877 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2 · 𝑦)))
171 oveq1 7155 . . . . . . . . . 10 (𝑦 = (log‘𝑥) → (𝑦↑2) = ((log‘𝑥)↑2))
172 oveq2 7156 . . . . . . . . . 10 (𝑦 = (log‘𝑥) → (2 · 𝑦) = (2 · (log‘𝑥)))
173119, 144, 145, 140, 147, 150, 160, 170, 171, 172dvmptco 24487 . . . . . . . . 9 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ ((log‘𝑥)↑2))) = (𝑥 ∈ ℝ+ ↦ ((2 · (log‘𝑥)) · (1 / 𝑥))))
174113recnd 10658 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 − (2 · (log‘𝑥))) ∈ ℂ)
175 ovexd 7183 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (0 − (2 · (1 / 𝑥))) ∈ V)
176 2cnd 11704 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℂ)
177 0red 10633 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 0 ∈ ℝ)
178 2cnd 11704 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
179 0red 10633 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
180 2cnd 11704 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 2 ∈ ℂ)
181119, 180dvmptc 24473 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ 2)) = (𝑥 ∈ ℝ ↦ 0))
182119, 178, 179, 181, 127, 129, 128, 132dvmptres 24478 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ 2)) = (𝑥 ∈ ℝ+ ↦ 0))
183 mulcl 10610 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ (1 / 𝑥) ∈ ℂ) → (2 · (1 / 𝑥)) ∈ ℂ)
18425, 141, 183sylancr 587 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 · (1 / 𝑥)) ∈ ℂ)
185119, 145, 140, 160, 180dvmptcmul 24479 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ (2 · (1 / 𝑥))))
186119, 176, 177, 182, 139, 184, 185dvmptsub 24482 . . . . . . . . 9 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (2 − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦ (0 − (2 · (1 / 𝑥)))))
187119, 138, 142, 173, 174, 175, 186dvmptadd 24475 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))) = (𝑥 ∈ ℝ+ ↦ (((2 · (log‘𝑥)) · (1 / 𝑥)) + (0 − (2 · (1 / 𝑥))))))
188139, 176, 141subdird 11086 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((2 · (log‘𝑥)) − 2) · (1 / 𝑥)) = (((2 · (log‘𝑥)) · (1 / 𝑥)) − (2 · (1 / 𝑥))))
189136recnd 10658 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((2 · (log‘𝑥)) − 2) ∈ ℂ)
190 rpne0 12395 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ≠ 0)
191190adantl 482 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
192189, 120, 191divrecd 11408 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((2 · (log‘𝑥)) − 2) / 𝑥) = (((2 · (log‘𝑥)) − 2) · (1 / 𝑥)))
193 df-neg 10862 . . . . . . . . . . . 12 -(2 · (1 / 𝑥)) = (0 − (2 · (1 / 𝑥)))
194193oveq2i 7159 . . . . . . . . . . 11 (((2 · (log‘𝑥)) · (1 / 𝑥)) + -(2 · (1 / 𝑥))) = (((2 · (log‘𝑥)) · (1 / 𝑥)) + (0 − (2 · (1 / 𝑥))))
195142, 184negsubd 10992 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((2 · (log‘𝑥)) · (1 / 𝑥)) + -(2 · (1 / 𝑥))) = (((2 · (log‘𝑥)) · (1 / 𝑥)) − (2 · (1 / 𝑥))))
196194, 195syl5eqr 2875 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((2 · (log‘𝑥)) · (1 / 𝑥)) + (0 − (2 · (1 / 𝑥)))) = (((2 · (log‘𝑥)) · (1 / 𝑥)) − (2 · (1 / 𝑥))))
197188, 192, 1963eqtr4rd 2872 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((2 · (log‘𝑥)) · (1 / 𝑥)) + (0 − (2 · (1 / 𝑥)))) = (((2 · (log‘𝑥)) − 2) / 𝑥))
198197mpteq2dva 5158 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (𝑥 ∈ ℝ+ ↦ (((2 · (log‘𝑥)) · (1 / 𝑥)) + (0 − (2 · (1 / 𝑥))))) = (𝑥 ∈ ℝ+ ↦ (((2 · (log‘𝑥)) − 2) / 𝑥)))
199187, 198eqtrd 2861 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))) = (𝑥 ∈ ℝ+ ↦ (((2 · (log‘𝑥)) − 2) / 𝑥)))
200119, 120, 121, 133, 134, 137, 199dvmptmul 24476 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))))) = (𝑥 ∈ ℝ+ ↦ ((1 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) + ((((2 · (log‘𝑥)) − 2) / 𝑥) · 𝑥))))
201134mulid2d 10648 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (1 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) = (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))
202138, 139, 176subsub2d 11015 . . . . . . . . . 10 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑2) − ((2 · (log‘𝑥)) − 2)) = (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))
203201, 202eqtr4d 2864 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (1 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) = (((log‘𝑥)↑2) − ((2 · (log‘𝑥)) − 2)))
204189, 120, 191divcan1d 11406 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((((2 · (log‘𝑥)) − 2) / 𝑥) · 𝑥) = ((2 · (log‘𝑥)) − 2))
205203, 204oveq12d 7166 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((1 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) + ((((2 · (log‘𝑥)) − 2) / 𝑥) · 𝑥)) = ((((log‘𝑥)↑2) − ((2 · (log‘𝑥)) − 2)) + ((2 · (log‘𝑥)) − 2)))
206138, 189npcand 10990 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑2) − ((2 · (log‘𝑥)) − 2)) + ((2 · (log‘𝑥)) − 2)) = ((log‘𝑥)↑2))
207205, 206eqtrd 2861 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((1 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) + ((((2 · (log‘𝑥)) − 2) / 𝑥) · 𝑥)) = ((log‘𝑥)↑2))
208207mpteq2dva 5158 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (𝑥 ∈ ℝ+ ↦ ((1 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))) + ((((2 · (log‘𝑥)) − 2) / 𝑥) · 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥)↑2)))
209200, 208eqtrd 2861 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥))))))) = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥)↑2)))
210 fveq2 6667 . . . . . 6 (𝑥 = 𝑛 → (log‘𝑥) = (log‘𝑛))
211210oveq1d 7163 . . . . 5 (𝑥 = 𝑛 → ((log‘𝑥)↑2) = ((log‘𝑛)↑2))
212 simp32 1204 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 𝑥𝑛)
213 simp2l 1193 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 𝑥 ∈ ℝ+)
214 simp2r 1194 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 𝑛 ∈ ℝ+)
215213, 214logled 25126 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → (𝑥𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛)))
216212, 215mpbid 233 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → (log‘𝑥) ≤ (log‘𝑛))
217213relogcld 25122 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → (log‘𝑥) ∈ ℝ)
218214relogcld 25122 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → (log‘𝑛) ∈ ℝ)
219 simp31 1203 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 1 ≤ 𝑥)
220 logleb 25102 . . . . . . . . . 10 ((1 ∈ ℝ+𝑥 ∈ ℝ+) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
22154, 213, 220sylancr 587 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
222219, 221mpbid 233 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → (log‘1) ≤ (log‘𝑥))
22364, 222eqbrtrrid 5099 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 0 ≤ (log‘𝑥))
224214rpred 12421 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 𝑛 ∈ ℝ)
225 1red 10631 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 1 ∈ ℝ)
226213rpred 12421 . . . . . . . . 9 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 𝑥 ∈ ℝ)
227225, 226, 224, 219, 212letrd 10786 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 1 ≤ 𝑛)
228224, 227logge0d 25129 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 0 ≤ (log‘𝑛))
229217, 218, 223, 228le2sqd 13610 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → ((log‘𝑥) ≤ (log‘𝑛) ↔ ((log‘𝑥)↑2) ≤ ((log‘𝑛)↑2)))
230216, 229mpbid 233 . . . . 5 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → ((log‘𝑥)↑2) ≤ ((log‘𝑛)↑2))
231 relogcl 25075 . . . . . . 7 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
232231ad2antrl 724 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
233232sqge0d 13602 . . . . 5 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ ((log‘𝑥)↑2))
23454a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ+)
235 simpl 483 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ+)
236 1le1 11257 . . . . . 6 1 ≤ 1
237236a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ≤ 1)
238 simpr 485 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ≤ 𝐴)
2399rexrd 10680 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ*)
240 pnfge 12515 . . . . . 6 (𝐴 ∈ ℝ*𝐴 ≤ +∞)
241239, 240syl 17 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 𝐴 ≤ +∞)
24294, 95, 96, 97, 99, 103, 104, 115, 109, 117, 209, 211, 230, 50, 233, 234, 235, 237, 238, 241, 44dvfsum2 24549 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘𝑛)↑2) − (𝑥 · (((log‘𝑥)↑2) + (2 − (2 · (log‘𝑥)))))))‘1))) ≤ ((log‘𝐴)↑2))
24392, 242eqbrtrrd 5087 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴)))))) − -2)) ≤ ((log‘𝐴)↑2))
24424, 29, 12, 38, 243letrd 10786 . 2 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) − 2) ≤ ((log‘𝐴)↑2))
24513a1i 11 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 2 ∈ ℝ)
24622, 245, 12lesubaddd 11226 . 2 ((𝐴 ∈ ℝ+ ∧ 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)))
247244, 246mpbid 233 1 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) ≤ (((log‘𝐴)↑2) + 2))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wne 3021  Vcvv 3500  wss 3940  {cpr 4566   class class class wbr 5063  cmpt 5143  ran crn 5555  cres 5556  wf 6348  1-1-ontowf1o 6351  cfv 6352  (class class class)co 7148  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  +∞cpnf 10661  *cxr 10663  cle 10665  cmin 10859  -cneg 10860   / cdiv 11286  cn 11627  2c2 11681  cz 11970  +crp 12379  (,)cioo 12728  ...cfz 12882  cfl 13150  cexp 13419  abscabs 14583  Σcsu 15032  TopOpenctopn 16685  topGenctg 16701  fldccnfld 20464   D cdv 24379  logclog 25054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-inf2 9093  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-isom 6361  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7399  df-om 7569  df-1st 7680  df-2nd 7681  df-supp 7822  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-2o 8094  df-oadd 8097  df-er 8279  df-map 8398  df-pm 8399  df-ixp 8451  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-fsupp 8823  df-fi 8864  df-sup 8895  df-inf 8896  df-oi 8963  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-q 12338  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-ioc 12733  df-ico 12734  df-icc 12735  df-fz 12883  df-fzo 13024  df-fl 13152  df-mod 13228  df-seq 13360  df-exp 13420  df-fac 13624  df-bc 13653  df-hash 13681  df-shft 14416  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-limsup 14818  df-clim 14835  df-rlim 14836  df-sum 15033  df-ef 15411  df-sin 15413  df-cos 15414  df-pi 15416  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-starv 16570  df-sca 16571  df-vsca 16572  df-ip 16573  df-tset 16574  df-ple 16575  df-ds 16577  df-unif 16578  df-hom 16579  df-cco 16580  df-rest 16686  df-topn 16687  df-0g 16705  df-gsum 16706  df-topgen 16707  df-pt 16708  df-prds 16711  df-xrs 16765  df-qtop 16770  df-imas 16771  df-xps 16773  df-mre 16847  df-mrc 16848  df-acs 16850  df-mgm 17842  df-sgrp 17890  df-mnd 17901  df-submnd 17945  df-mulg 18155  df-cntz 18377  df-cmn 18828  df-psmet 20456  df-xmet 20457  df-met 20458  df-bl 20459  df-mopn 20460  df-fbas 20461  df-fg 20462  df-cnfld 20465  df-top 21421  df-topon 21438  df-topsp 21460  df-bases 21473  df-cld 21546  df-ntr 21547  df-cls 21548  df-nei 21625  df-lp 21663  df-perf 21664  df-cn 21754  df-cnp 21755  df-haus 21842  df-cmp 21914  df-tx 22089  df-hmeo 22282  df-fil 22373  df-fm 22465  df-flim 22466  df-flf 22467  df-xms 22848  df-ms 22849  df-tms 22850  df-cncf 23404  df-limc 24382  df-dv 24383  df-log 25056
This theorem is referenced by:  selberglem2  26039
  Copyright terms: Public domain W3C validator