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

Theorem selberglem2 26694
Description: Lemma for selberg 26696. (Contributed by Mario Carneiro, 23-May-2016.)
Hypothesis
Ref Expression
selberglem1.t 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)
Assertion
Ref Expression
selberglem2 (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Distinct variable group:   𝑚,𝑛,𝑥
Allowed substitution hints:   𝑇(𝑥,𝑚,𝑛)

Proof of Theorem selberglem2
StepHypRef Expression
1 reex 10962 . . . . . . 7 ℝ ∈ V
2 rpssre 12737 . . . . . . 7 + ⊆ ℝ
31, 2ssexi 5246 . . . . . 6 + ∈ V
43a1i 11 . . . . 5 (⊤ → ℝ+ ∈ V)
5 fzfid 13693 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
6 elfznn 13285 . . . . . . . . . . 11 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
76adantl 482 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8 mucl 26290 . . . . . . . . . 10 (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
97, 8syl 17 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
109zred 12426 . . . . . . . 8 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
1110recnd 11003 . . . . . . 7 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
12 fzfid 13693 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
13 elfznn 13285 . . . . . . . . . . . . . . 15 (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
1413adantl 482 . . . . . . . . . . . . . 14 ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
1514nnrpd 12770 . . . . . . . . . . . . 13 ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ+)
1615relogcld 25778 . . . . . . . . . . . 12 ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ)
1716resqcld 13965 . . . . . . . . . . 11 ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℝ)
1812, 17fsumrecl 15446 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℝ)
19 simplr 766 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
2018, 19rerpdivcld 12803 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℝ)
2120recnd 11003 . . . . . . . 8 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℂ)
22 selberglem1.t . . . . . . . . . 10 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)
23 simpr 485 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
246nnrpd 12770 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
25 rpdivcl 12755 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
2623, 24, 25syl2an 596 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
2726relogcld 25778 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
2827resqcld 13965 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
29 2re 12047 . . . . . . . . . . . . 13 2 ∈ ℝ
30 remulcl 10956 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
3129, 27, 30sylancr 587 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
32 resubcl 11285 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
3329, 31, 32sylancr 587 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
3428, 33readdcld 11004 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℝ)
3534, 7nndivred 12027 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛) ∈ ℝ)
3622, 35eqeltrid 2843 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℝ)
3736recnd 11003 . . . . . . . 8 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
3821, 37subcld 11332 . . . . . . 7 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) ∈ ℂ)
3911, 38mulcld 10995 . . . . . 6 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
405, 39fsumcl 15445 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
4111, 37mulcld 10995 . . . . . . 7 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · 𝑇) ∈ ℂ)
425, 41fsumcl 15445 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) ∈ ℂ)
43 2cn 12048 . . . . . . 7 2 ∈ ℂ
44 relogcl 25731 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
4544adantl 482 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
4645recnd 11003 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
47 mulcl 10955 . . . . . . 7 ((2 ∈ ℂ ∧ (log‘𝑥) ∈ ℂ) → (2 · (log‘𝑥)) ∈ ℂ)
4843, 46, 47sylancr 587 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℝ+) → (2 · (log‘𝑥)) ∈ ℂ)
4942, 48subcld 11332 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))) ∈ ℂ)
50 eqidd 2739 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
51 eqidd 2739 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
524, 40, 49, 50, 51offval2 7553 . . . 4 (⊤ → ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))))
5340, 42, 48addsubassd 11352 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
54 rpcnne0 12748 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
5554adantl 482 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
5655simpld 495 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
5710adantr 481 . . . . . . . . . . . 12 ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (μ‘𝑛) ∈ ℝ)
5857, 17remulcld 11005 . . . . . . . . . . 11 ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
5912, 58fsumrecl 15446 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
6059recnd 11003 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℂ)
6155simprd 496 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
625, 56, 60, 61fsumdivc 15498 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
6317recnd 11003 . . . . . . . . . . . 12 ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℂ)
6412, 63fsumcl 15445 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ)
6555adantr 481 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
66 divass 11651 . . . . . . . . . . 11 (((μ‘𝑛) ∈ ℂ ∧ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
6711, 64, 65, 66syl3anc 1370 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
6812, 11, 63fsummulc2 15496 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)))
6968oveq1d 7290 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
7021, 37npcand 11336 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))
7170oveq2d 7291 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
7211, 38, 37adddid 10999 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
7371, 72eqtr3d 2780 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
7467, 69, 733eqtr3d 2786 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
7574sumeq2dv 15415 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
765, 39, 41fsumadd 15452 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)))
7762, 75, 763eqtrrd 2783 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
7877oveq1d 7290 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
7953, 78eqtr3d 2780 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
8079mpteq2dva 5174 . . . 4 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
8152, 80eqtrd 2778 . . 3 (⊤ → ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
82 1red 10976 . . . . 5 (⊤ → 1 ∈ ℝ)
835, 28fsumrecl 15446 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
8483, 23rerpdivcld 12803 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ)
8584recnd 11003 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℂ)
86 2cnd 12051 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℂ)
87 2nn0 12250 . . . . . . . 8 2 ∈ ℕ0
88 logexprlim 26373 . . . . . . . 8 (2 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝𝑟 (!‘2))
8987, 88mp1i 13 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝𝑟 (!‘2))
90 2cnd 12051 . . . . . . . 8 (⊤ → 2 ∈ ℂ)
91 rlimconst 15253 . . . . . . . 8 ((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 2) ⇝𝑟 2)
922, 90, 91sylancr 587 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ 2) ⇝𝑟 2)
9385, 86, 89, 92rlimadd 15352 . . . . . 6 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝𝑟 ((!‘2) + 2))
94 rlimo1 15326 . . . . . 6 ((𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝𝑟 ((!‘2) + 2) → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ 𝑂(1))
9593, 94syl 17 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ 𝑂(1))
96 readdcl 10954 . . . . . 6 (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ ∧ 2 ∈ ℝ) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
9784, 29, 96sylancl 586 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
9840abscld 15148 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
9997recnd 11003 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℂ)
10099abscld 15148 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ ℝ)
10139abscld 15148 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
1025, 101fsumrecl 15446 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
1035, 39fsumabs 15513 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
104 readdcl 10954 . . . . . . . . . . . 12 ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 2 ∈ ℝ) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
10528, 29, 104sylancl 586 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
106105, 19rerpdivcld 12803 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
1075, 106fsumrecl 15446 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
10838abscld 15148 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℝ)
10911, 38absmuld 15166 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
11011abscld 15148 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
111 1red 10976 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
11238absge0d 15156 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
113 mule1 26297 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
1147, 113syl 17 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
115110, 111, 108, 112, 114lemul1ad 11914 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
116108recnd 11003 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
117116mulid2d 10993 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
118115, 117breqtrd 5100 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
119109, 118eqbrtrd 5096 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
12065simpld 495 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
121120, 38absmuld 15166 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
122120, 21, 37subdid 11431 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)))
12365simprd 496 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0)
12464, 120, 123divcan2d 11753 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2))
12534recnd 11003 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
1267nnrpd 12770 . . . . . . . . . . . . . . . . . . 19 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
127 rpcnne0 12748 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
128126, 127syl 17 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
129 divass 11651 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)))
13022oveq2i 7286 . . . . . . . . . . . . . . . . . . . 20 (𝑥 · 𝑇) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛))
131129, 130eqtr4di 2796 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · 𝑇))
132 div23 11652 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
133131, 132eqtr3d 2780 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
134120, 125, 128, 133syl3anc 1370 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
135124, 134oveq12d 7293 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
136122, 135eqtrd 2778 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
137136fveq2d 6778 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))))
138 rprege0 12745 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
139 absid 15008 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
14019, 138, 1393syl 18 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑥) = 𝑥)
141140oveq1d 7290 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
142121, 137, 1413eqtr3d 2786 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
1437nncnd 11989 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
144143mulid2d 10993 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
145 rpre 12738 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
146145adantl 482 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
147 fznnfl 13582 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
148146, 147syl 17 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
149148simplbda 500 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛𝑥)
150144, 149eqbrtrd 5096 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
15119rpred 12772 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
152111, 151, 126lemuldivd 12821 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
153150, 152mpbid 231 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
154 log2sumbnd 26692 . . . . . . . . . . . . . 14 (((𝑥 / 𝑛) ∈ ℝ+ ∧ 1 ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
15526, 153, 154syl2anc 584 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
156142, 155eqbrtrrd 5098 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
157108, 105, 19lemuldiv2d 12822 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2) ↔ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)))
158156, 157mpbid 231 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
159101, 108, 106, 119, 158letrd 11132 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
1605, 101, 106, 159fsumle 15511 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
1615, 105fsumrecl 15446 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
162 remulcl 10956 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
163146, 29, 162sylancl 586 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 · 2) ∈ ℝ)
16483, 163readdcld 11004 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) ∈ ℝ)
16528recnd 11003 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
166 2cnd 12051 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
1675, 165, 166fsumadd 15452 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2))
168 fsumconst 15502 . . . . . . . . . . . . . . . 16 (((1...(⌊‘𝑥)) ∈ Fin ∧ 2 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
1695, 43, 168sylancl 586 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
170138adantl 482 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
171 flge0nn0 13540 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
172 hashfz1 14060 . . . . . . . . . . . . . . . . 17 ((⌊‘𝑥) ∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
173170, 171, 1723syl 18 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ ℝ+) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
174173oveq1d 7290 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((♯‘(1...(⌊‘𝑥))) · 2) = ((⌊‘𝑥) · 2))
175169, 174eqtrd 2778 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((⌊‘𝑥) · 2))
176175oveq2d 7291 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
177167, 176eqtrd 2778 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
178 reflcl 13516 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
179146, 178syl 17 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℝ)
18029a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℝ)
181179, 180remulcld 11005 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) · 2) ∈ ℝ)
182 flle 13519 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
183146, 182syl 17 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ≤ 𝑥)
184 2pos 12076 . . . . . . . . . . . . . . . . 17 0 < 2
18529, 184pm3.2i 471 . . . . . . . . . . . . . . . 16 (2 ∈ ℝ ∧ 0 < 2)
186185a1i 11 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → (2 ∈ ℝ ∧ 0 < 2))
187 lemul1 11827 . . . . . . . . . . . . . . 15 (((⌊‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
188179, 146, 186, 187syl3anc 1370 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
189183, 188mpbid 231 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) · 2) ≤ (𝑥 · 2))
190181, 163, 83, 189leadd2dd 11590 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)))
191177, 190eqbrtrd 5096 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)))
192161, 164, 23, 191lediv1dd 12830 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥))
193105recnd 11003 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℂ)
1945, 56, 193, 61fsumdivc 15498 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
19583recnd 11003 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
19656, 86mulcld 10995 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 · 2) ∈ ℂ)
197 divdir 11658 . . . . . . . . . . . 12 ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ ∧ (𝑥 · 2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
198195, 196, 55, 197syl3anc 1370 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
19986, 56, 61divcan3d 11756 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((𝑥 · 2) / 𝑥) = 2)
200199oveq2d 7291 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
201198, 200eqtrd 2778 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
202192, 194, 2013brtr3d 5105 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
203102, 107, 97, 160, 202letrd 11132 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
20498, 102, 97, 103, 203letrd 11132 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
20597leabsd 15126 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
20698, 97, 100, 204, 205letrd 11132 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
207206adantrr 714 . . . . 5 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
20882, 95, 97, 40, 207o1le 15364 . . . 4 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1))
20922selberglem1 26693 . . . 4 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
210 o1add 15323 . . . 4 (((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
211208, 209, 210sylancl 586 . . 3 (⊤ → ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
21281, 211eqeltrrd 2840 . 2 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
213212mptru 1546 1 (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  w3a 1086   = wceq 1539  wtru 1540  wcel 2106  wne 2943  Vcvv 3432  wss 3887   class class class wbr 5074  cmpt 5157  cfv 6433  (class class class)co 7275  f cof 7531  Fincfn 8733  cc 10869  cr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009  cle 11010  cmin 11205   / cdiv 11632  cn 11973  2c2 12028  0cn0 12233  cz 12319  +crp 12730  ...cfz 13239  cfl 13510  cexp 13782  !cfa 13987  chash 14044  abscabs 14945  𝑟 crli 15194  𝑂(1)co1 15195  Σcsu 15397  logclog 25710  μcmu 26244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949  ax-addf 10950  ax-mulf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-disj 5040  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-oadd 8301  df-er 8498  df-map 8617  df-pm 8618  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-fi 9170  df-sup 9201  df-inf 9202  df-oi 9269  df-dju 9659  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-xnn0 12306  df-z 12320  df-dec 12438  df-uz 12583  df-q 12689  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-ioo 13083  df-ioc 13084  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-fl 13512  df-mod 13590  df-seq 13722  df-exp 13783  df-fac 13988  df-bc 14017  df-hash 14045  df-shft 14778  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-limsup 15180  df-clim 15197  df-rlim 15198  df-o1 15199  df-lo1 15200  df-sum 15398  df-ef 15777  df-e 15778  df-sin 15779  df-cos 15780  df-tan 15781  df-pi 15782  df-dvds 15964  df-gcd 16202  df-prm 16377  df-pc 16538  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-hom 16986  df-cco 16987  df-rest 17133  df-topn 17134  df-0g 17152  df-gsum 17153  df-topgen 17154  df-pt 17155  df-prds 17158  df-xrs 17213  df-qtop 17218  df-imas 17219  df-xps 17221  df-mre 17295  df-mrc 17296  df-acs 17298  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-mulg 18701  df-cntz 18923  df-cmn 19388  df-psmet 20589  df-xmet 20590  df-met 20591  df-bl 20592  df-mopn 20593  df-fbas 20594  df-fg 20595  df-cnfld 20598  df-top 22043  df-topon 22060  df-topsp 22082  df-bases 22096  df-cld 22170  df-ntr 22171  df-cls 22172  df-nei 22249  df-lp 22287  df-perf 22288  df-cn 22378  df-cnp 22379  df-haus 22466  df-cmp 22538  df-tx 22713  df-hmeo 22906  df-fil 22997  df-fm 23089  df-flim 23090  df-flf 23091  df-xms 23473  df-ms 23474  df-tms 23475  df-cncf 24041  df-limc 25030  df-dv 25031  df-ulm 25536  df-log 25712  df-cxp 25713  df-atan 26017  df-em 26142  df-mu 26250
This theorem is referenced by:  selberglem3  26695  selberg  26696
  Copyright terms: Public domain W3C validator