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

Theorem selberg34r 25829
Description: The sum of selberg3r 25827 and selberg4r 25828. (Contributed by Mario Carneiro, 31-May-2016.)
Hypothesis
Ref Expression
pntrval.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
Assertion
Ref Expression
selberg34r (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)
Distinct variable groups:   𝑚,𝑎,𝑛,𝑥   𝑦,𝑚,𝑅,𝑛,𝑥
Allowed substitution hint:   𝑅(𝑎)

Proof of Theorem selberg34r
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 2re 11559 . . . . . . . . . 10 2 ∈ ℝ
21a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
3 elioore 12618 . . . . . . . . . . . . 13 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
43adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
5 1rp 12243 . . . . . . . . . . . . 13 1 ∈ ℝ+
65a1i 11 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ+)
7 1red 10488 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
8 eliooord 12646 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
98adantl 482 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥𝑥 < +∞))
109simpld 495 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
117, 4, 10ltled 10635 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
124, 6, 11rpgecld 12320 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ+)
13 pntrval.r . . . . . . . . . . . . 13 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
1413pntrf 25821 . . . . . . . . . . . 12 𝑅:ℝ+⟶ℝ
1514ffvelrni 6715 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑅𝑥) ∈ ℝ)
1612, 15syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅𝑥) ∈ ℝ)
1712relogcld 24887 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
1816, 17remulcld 10517 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑅𝑥) · (log‘𝑥)) ∈ ℝ)
192, 18remulcld 10517 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((𝑅𝑥) · (log‘𝑥))) ∈ ℝ)
2019recnd 10515 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((𝑅𝑥) · (log‘𝑥))) ∈ ℂ)
214, 10rplogcld 24893 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ+)
222, 21rerpdivcld 12312 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℝ)
2322recnd 10515 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℂ)
24 fzfid 13191 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
2512adantr 481 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
26 elfznn 12786 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
2726adantl 482 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
2827nnrpd 12279 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
2925, 28rpdivcld 12298 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
3014ffvelrni 6715 . . . . . . . . . . . 12 ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
3129, 30syl 17 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
32 fzfid 13191 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...𝑛) ∈ Fin)
33 dvdsssfz1 15501 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦𝑛} ⊆ (1...𝑛))
3427, 33syl 17 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦𝑛} ⊆ (1...𝑛))
3532, 34ssfid 8587 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦𝑛} ∈ Fin)
36 ssrab2 3977 . . . . . . . . . . . . . . . 16 {𝑦 ∈ ℕ ∣ 𝑦𝑛} ⊆ ℕ
37 simpr 485 . . . . . . . . . . . . . . . 16 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})
3836, 37sseldi 3887 . . . . . . . . . . . . . . 15 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → 𝑚 ∈ ℕ)
39 vmacl 25377 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
4038, 39syl 17 . . . . . . . . . . . . . 14 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → (Λ‘𝑚) ∈ ℝ)
41 dvdsdivcl 15499 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})
4227, 41sylan 580 . . . . . . . . . . . . . . . 16 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})
4336, 42sseldi 3887 . . . . . . . . . . . . . . 15 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → (𝑛 / 𝑚) ∈ ℕ)
44 vmacl 25377 . . . . . . . . . . . . . . 15 ((𝑛 / 𝑚) ∈ ℕ → (Λ‘(𝑛 / 𝑚)) ∈ ℝ)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → (Λ‘(𝑛 / 𝑚)) ∈ ℝ)
4640, 45remulcld 10517 . . . . . . . . . . . . 13 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ)
4735, 46fsumrecl 14924 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ)
48 vmacl 25377 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
4927, 48syl 17 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
5028relogcld 24887 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
5149, 50remulcld 10517 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (log‘𝑛)) ∈ ℝ)
5247, 51resubcld 10916 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))) ∈ ℝ)
5331, 52remulcld 10517 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈ ℝ)
5424, 53fsumrecl 14924 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈ ℝ)
5554recnd 10515 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈ ℂ)
5623, 55mulcld 10507 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈ ℂ)
5720, 56subcld 10845 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) ∈ ℂ)
584recnd 10515 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
59 2cnd 11563 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
6012rpne0d 12286 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
61 2ne0 11589 . . . . . . 7 2 ≠ 0
6261a1i 11 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ≠ 0)
6357, 58, 59, 60, 62divdiv32d 11289 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) / 2) = ((((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 2) / 𝑥))
6457, 58, 60divcld 11264 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) ∈ ℂ)
6564, 59, 62divrecd 11267 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) / 2) = ((((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) · (1 / 2)))
6620, 56, 59, 62divsubdird 11303 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 2) = (((2 · ((𝑅𝑥) · (log‘𝑥))) / 2) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / 2)))
6718recnd 10515 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑅𝑥) · (log‘𝑥)) ∈ ℂ)
6867, 59, 62divcan3d 11269 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) / 2) = ((𝑅𝑥) · (log‘𝑥)))
6921rpcnd 12283 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
7021rpne0d 12286 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
7159, 69, 55, 70div32d 11287 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))
7271oveq1d 7031 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / 2) = ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 2))
7354, 21rerpdivcld 12312 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈ ℝ)
7473recnd 10515 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈ ℂ)
7574, 59, 62divcan3d 11269 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))
7672, 75eqtrd 2831 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))
7768, 76oveq12d 7034 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅𝑥) · (log‘𝑥))) / 2) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / 2)) = (((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))
7866, 77eqtrd 2831 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 2) = (((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))
7978oveq1d 7031 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 2) / 𝑥) = ((((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))
8063, 65, 793eqtr3d 2839 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) · (1 / 2)) = ((((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))
8180mpteq2dva 5055 . . 3 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) · (1 / 2))) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)))
8222, 54remulcld 10517 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈ ℝ)
8319, 82resubcld 10916 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) ∈ ℝ)
8483, 12rerpdivcld 12312 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) ∈ ℝ)
857rehalfcld 11732 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 / 2) ∈ ℝ)
8631recnd 10515 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ)
8747recnd 10515 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℂ)
8849recnd 10515 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
8950recnd 10515 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℂ)
9088, 89mulcld 10507 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (log‘𝑛)) ∈ ℂ)
9186, 87, 90subdid 10944 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) = (((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑛) · (log‘𝑛)))))
9286, 88, 89mul12d 10696 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑛) · (log‘𝑛))) = ((Λ‘𝑛) · ((𝑅‘(𝑥 / 𝑛)) · (log‘𝑛))))
9388, 86, 89mulassd 10510 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) = ((Λ‘𝑛) · ((𝑅‘(𝑥 / 𝑛)) · (log‘𝑛))))
9492, 93eqtr4d 2834 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑛) · (log‘𝑛))) = (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))
9594oveq2d 7032 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑛) · (log‘𝑛)))) = (((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
9691, 95eqtrd 2831 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) = (((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
9796sumeq2dv 14893 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
9886, 87mulcld 10507 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) ∈ ℂ)
9988, 86mulcld 10507 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
10099, 89mulcld 10507 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
10124, 98, 100fsumsub 14976 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
10246recnd 10515 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℂ)
10335, 86, 102fsummulc2 14972 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
104103sumeq2dv 14893 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
105 oveq2 7024 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (𝑚 · 𝑘) → (𝑥 / 𝑛) = (𝑥 / (𝑚 · 𝑘)))
106105fveq2d 6542 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑚 · 𝑘) → (𝑅‘(𝑥 / 𝑛)) = (𝑅‘(𝑥 / (𝑚 · 𝑘))))
107 fvoveq1 7039 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (𝑚 · 𝑘) → (Λ‘(𝑛 / 𝑚)) = (Λ‘((𝑚 · 𝑘) / 𝑚)))
108107oveq2d 7032 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑚 · 𝑘) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) = ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚))))
109106, 108oveq12d 7034 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑚 · 𝑘) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = ((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))))
11031adantrr 713 . . . . . . . . . . . . . . . . . . 19 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
11140anasss 467 . . . . . . . . . . . . . . . . . . . 20 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})) → (Λ‘𝑚) ∈ ℝ)
11245anasss 467 . . . . . . . . . . . . . . . . . . . 20 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})) → (Λ‘(𝑛 / 𝑚)) ∈ ℝ)
113111, 112remulcld 10517 . . . . . . . . . . . . . . . . . . 19 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ)
114110, 113remulcld 10517 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) ∈ ℝ)
115114recnd 10515 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛})) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) ∈ ℂ)
116109, 4, 115dvdsflsumcom 25447 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))))
11758ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑥 ∈ ℂ)
118 elfznn 12786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ (1...(⌊‘𝑥)) → 𝑚 ∈ ℕ)
119118adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ)
120119nnrpd 12279 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ+)
121120adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑚 ∈ ℝ+)
122121rpcnd 12283 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑚 ∈ ℂ)
123 elfznn 12786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚))) → 𝑘 ∈ ℕ)
124123adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑘 ∈ ℕ)
125124nncnd 11502 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑘 ∈ ℂ)
126121rpne0d 12286 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑚 ≠ 0)
127124nnne0d 11535 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑘 ≠ 0)
128117, 122, 125, 126, 127divdiv1d 11295 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑥 / 𝑚) / 𝑘) = (𝑥 / (𝑚 · 𝑘)))
129128eqcomd 2801 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑥 / (𝑚 · 𝑘)) = ((𝑥 / 𝑚) / 𝑘))
130129fveq2d 6542 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑅‘(𝑥 / (𝑚 · 𝑘))) = (𝑅‘((𝑥 / 𝑚) / 𝑘)))
131125, 122, 126divcan3d 11269 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑚 · 𝑘) / 𝑚) = 𝑘)
132131fveq2d 6542 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘((𝑚 · 𝑘) / 𝑚)) = (Λ‘𝑘))
133132oveq2d 7032 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚))) = ((Λ‘𝑚) · (Λ‘𝑘)))
134130, 133oveq12d 7034 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = ((𝑅‘((𝑥 / 𝑚) / 𝑘)) · ((Λ‘𝑚) · (Λ‘𝑘))))
13512ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑥 ∈ ℝ+)
136135, 121rpdivcld 12298 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑥 / 𝑚) ∈ ℝ+)
137124nnrpd 12279 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑘 ∈ ℝ+)
138136, 137rpdivcld 12298 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑥 / 𝑚) / 𝑘) ∈ ℝ+)
13914ffvelrni 6715 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 / 𝑚) / 𝑘) ∈ ℝ+ → (𝑅‘((𝑥 / 𝑚) / 𝑘)) ∈ ℝ)
140138, 139syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑅‘((𝑥 / 𝑚) / 𝑘)) ∈ ℝ)
141140recnd 10515 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑅‘((𝑥 / 𝑚) / 𝑘)) ∈ ℂ)
142119, 39syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℝ)
143142recnd 10515 . . . . . . . . . . . . . . . . . . . . . . 23 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℂ)
144143adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑚) ∈ ℂ)
145 vmacl 25377 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℕ → (Λ‘𝑘) ∈ ℝ)
146124, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑘) ∈ ℝ)
147146recnd 10515 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑘) ∈ ℂ)
148144, 147mulcld 10507 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((Λ‘𝑚) · (Λ‘𝑘)) ∈ ℂ)
149141, 148mulcomd 10508 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑅‘((𝑥 / 𝑚) / 𝑘)) · ((Λ‘𝑚) · (Λ‘𝑘))) = (((Λ‘𝑚) · (Λ‘𝑘)) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))
150144, 147, 141mulassd 10510 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (((Λ‘𝑚) · (Λ‘𝑘)) · (𝑅‘((𝑥 / 𝑚) / 𝑘))) = ((Λ‘𝑚) · ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
151134, 149, 1503eqtrd 2835 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = ((Λ‘𝑚) · ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
152151sumeq2dv 14893 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑚) · ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
153 fzfid 13191 . . . . . . . . . . . . . . . . . . 19 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑚))) ∈ Fin)
154146, 140remulcld 10517 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))) ∈ ℝ)
155154recnd 10515 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))) ∈ ℂ)
156153, 143, 155fsummulc2 14972 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) = Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑚) · ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
157152, 156eqtr4d 2834 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = ((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
158157sumeq2dv 14893 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
159104, 116, 1583eqtrd 2835 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
160159oveq1d 7031 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
16197, 101, 1603eqtrd 2835 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
162161oveq2d 7032 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = ((2 / (log‘𝑥)) · (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
163153, 154fsumrecl 14924 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))) ∈ ℝ)
164142, 163remulcld 10517 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) ∈ ℝ)
16524, 164fsumrecl 14924 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) ∈ ℝ)
166165recnd 10515 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) ∈ ℂ)
16749, 31remulcld 10517 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
168167, 50remulcld 10517 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
16924, 168fsumrecl 14924 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
170169recnd 10515 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
17123, 166, 170subdid 10944 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) = (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
172162, 171eqtrd 2831 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
173172oveq2d 7032 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) = ((2 · ((𝑅𝑥) · (log‘𝑥))) − (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))))
17423, 166mulcld 10507 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) ∈ ℂ)
17522, 169remulcld 10517 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℝ)
176175recnd 10515 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℂ)
17720, 174, 176subsub3d 10875 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) − (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))) = (((2 · ((𝑅𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))))
178173, 177eqtrd 2831 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) = (((2 · ((𝑅𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))))
179672timesd 11728 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((𝑅𝑥) · (log‘𝑥))) = (((𝑅𝑥) · (log‘𝑥)) + ((𝑅𝑥) · (log‘𝑥))))
180179oveq1d 7031 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) = ((((𝑅𝑥) · (log‘𝑥)) + ((𝑅𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
18167, 176, 67add32d 10714 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + ((𝑅𝑥) · (log‘𝑥))) = ((((𝑅𝑥) · (log‘𝑥)) + ((𝑅𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
182180, 181eqtr4d 2834 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) = ((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + ((𝑅𝑥) · (log‘𝑥))))
183182oveq1d 7031 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) = (((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))))
18418, 175readdcld 10516 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ∈ ℝ)
185184recnd 10515 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ∈ ℂ)
186185, 67, 174addsubassd 10865 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) = ((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + (((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))))))
187178, 183, 1863eqtrd 2835 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) = ((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + (((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))))))
188187oveq1d 7031 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) = (((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + (((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))))) / 𝑥))
18967, 174subcld 10845 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) ∈ ℂ)
190185, 189, 58, 60divdird 11302 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + (((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))))) / 𝑥) = (((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) + ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥)))
191188, 190eqtrd 2831 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) = (((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) + ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥)))
192191mpteq2dva 5055 . . . . 5 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥)) = (𝑥 ∈ (1(,)+∞) ↦ (((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) + ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥))))
193184, 12rerpdivcld 12312 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) ∈ ℝ)
19422, 165remulcld 10517 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) ∈ ℝ)
19518, 194resubcld 10916 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) ∈ ℝ)
196195, 12rerpdivcld 12312 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥) ∈ ℝ)
19713selberg3r 25827 . . . . . . 7 (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ 𝑂(1)
198197a1i 11 . . . . . 6 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ 𝑂(1))
19913selberg4r 25828 . . . . . . 7 (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥)) ∈ 𝑂(1)
200199a1i 11 . . . . . 6 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥)) ∈ 𝑂(1))
201193, 196, 198, 200o1add2 14814 . . . . 5 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((𝑅𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) + ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥))) ∈ 𝑂(1))
202192, 201eqeltrd 2883 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥)) ∈ 𝑂(1))
203 ioossre 12648 . . . . 5 (1(,)+∞) ⊆ ℝ
204 1cnd 10482 . . . . . 6 (⊤ → 1 ∈ ℂ)
205204halfcld 11730 . . . . 5 (⊤ → (1 / 2) ∈ ℂ)
206 o1const 14810 . . . . 5 (((1(,)+∞) ⊆ ℝ ∧ (1 / 2) ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ (1 / 2)) ∈ 𝑂(1))
207203, 205, 206sylancr 587 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (1 / 2)) ∈ 𝑂(1))
20884, 85, 202, 207o1mul2 14815 . . 3 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((2 · ((𝑅𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) · (1 / 2))) ∈ 𝑂(1))
20981, 208eqeltrrd 2884 . 2 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1))
210209mptru 1529 1 (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1522  wtru 1523  wcel 2081  wne 2984  {crab 3109  wss 3859   class class class wbr 4962  cmpt 5041  cfv 6225  (class class class)co 7016  cc 10381  cr 10382  0cc0 10383  1c1 10384   + caddc 10386   · cmul 10388  +∞cpnf 10518   < clt 10521  cmin 10717   / cdiv 11145  cn 11486  2c2 11540  +crp 12239  (,)cioo 12588  ...cfz 12742  cfl 13010  𝑂(1)co1 14677  Σcsu 14876  cdvds 15440  logclog 24819  Λcvma 25351  ψcchp 25352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461  ax-addf 10462  ax-mulf 10463
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-disj 4931  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-of 7267  df-om 7437  df-1st 7545  df-2nd 7546  df-supp 7682  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-2o 7954  df-oadd 7957  df-er 8139  df-map 8258  df-pm 8259  df-ixp 8311  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-fsupp 8680  df-fi 8721  df-sup 8752  df-inf 8753  df-oi 8820  df-dju 9176  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-4 11550  df-5 11551  df-6 11552  df-7 11553  df-8 11554  df-9 11555  df-n0 11746  df-xnn0 11816  df-z 11830  df-dec 11948  df-uz 12094  df-q 12198  df-rp 12240  df-xneg 12357  df-xadd 12358  df-xmul 12359  df-ioo 12592  df-ioc 12593  df-ico 12594  df-icc 12595  df-fz 12743  df-fzo 12884  df-fl 13012  df-mod 13088  df-seq 13220  df-exp 13280  df-fac 13484  df-bc 13513  df-hash 13541  df-shft 14260  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-limsup 14662  df-clim 14679  df-rlim 14680  df-o1 14681  df-lo1 14682  df-sum 14877  df-ef 15254  df-e 15255  df-sin 15256  df-cos 15257  df-tan 15258  df-pi 15259  df-dvds 15441  df-gcd 15677  df-prm 15845  df-pc 16003  df-struct 16314  df-ndx 16315  df-slot 16316  df-base 16318  df-sets 16319  df-ress 16320  df-plusg 16407  df-mulr 16408  df-starv 16409  df-sca 16410  df-vsca 16411  df-ip 16412  df-tset 16413  df-ple 16414  df-ds 16416  df-unif 16417  df-hom 16418  df-cco 16419  df-rest 16525  df-topn 16526  df-0g 16544  df-gsum 16545  df-topgen 16546  df-pt 16547  df-prds 16550  df-xrs 16604  df-qtop 16609  df-imas 16610  df-xps 16612  df-mre 16686  df-mrc 16687  df-acs 16689  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-submnd 17775  df-mulg 17982  df-cntz 18188  df-cmn 18635  df-psmet 20219  df-xmet 20220  df-met 20221  df-bl 20222  df-mopn 20223  df-fbas 20224  df-fg 20225  df-cnfld 20228  df-top 21186  df-topon 21203  df-topsp 21225  df-bases 21238  df-cld 21311  df-ntr 21312  df-cls 21313  df-nei 21390  df-lp 21428  df-perf 21429  df-cn 21519  df-cnp 21520  df-haus 21607  df-cmp 21679  df-tx 21854  df-hmeo 22047  df-fil 22138  df-fm 22230  df-flim 22231  df-flf 22232  df-xms 22613  df-ms 22614  df-tms 22615  df-cncf 23169  df-limc 24147  df-dv 24148  df-ulm 24648  df-log 24821  df-cxp 24822  df-atan 25126  df-em 25252  df-cht 25356  df-vma 25357  df-chp 25358  df-ppi 25359  df-mu 25360
This theorem is referenced by:  pntrlog2bndlem1  25835
  Copyright terms: Public domain W3C validator