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

Theorem pntrlog2bndlem4 25576
Description: Lemma for pntrlog2bnd 25580. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Hypotheses
Ref Expression
pntsval.1 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
pntrlog2bnd.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
pntrlog2bnd.t 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))
Assertion
Ref Expression
pntrlog2bndlem4 (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)
Distinct variable groups:   𝑖,𝑎,𝑛,𝑥   𝑆,𝑛,𝑥   𝑅,𝑛,𝑥   𝑇,𝑛
Allowed substitution hints:   𝑅(𝑖,𝑎)   𝑆(𝑖,𝑎)   𝑇(𝑥,𝑖,𝑎)

Proof of Theorem pntrlog2bndlem4
Dummy variables 𝑐 𝑚 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elioore 12414 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
21adantl 473 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
3 1rp 12039 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ+
43a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ+)
5 1red 10298 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
6 eliooord 12442 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
76adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥𝑥 < +∞))
87simpld 488 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
95, 2, 8ltled 10444 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
102, 4, 9rpgecld 12116 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ+)
1110rprege0d 12084 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
12 flge0nn0 12836 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ0)
14 nn0p1nn 11584 . . . . . . . . . . . . . . . . . . . 20 ((⌊‘𝑥) ∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ)
1513, 14syl 17 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℕ)
1615nnrpd 12075 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℝ+)
1710, 16rpdivcld 12094 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ+)
18 pntrlog2bnd.r . . . . . . . . . . . . . . . . . 18 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
1918pntrval 25558 . . . . . . . . . . . . . . . . 17 ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ+ → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
2017, 19syl 17 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
212, 15nndivred 11331 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ)
22 2re 11351 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
2322a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
24 flltp1 12816 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → 𝑥 < ((⌊‘𝑥) + 1))
252, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < ((⌊‘𝑥) + 1))
2615nncnd 11297 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℂ)
2726mulid1d 10315 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) · 1) = ((⌊‘𝑥) + 1))
2825, 27breqtrrd 4839 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < (((⌊‘𝑥) + 1) · 1))
292, 5, 16ltdivmuld 12128 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) < 1 ↔ 𝑥 < (((⌊‘𝑥) + 1) · 1)))
3028, 29mpbird 248 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 1)
31 1lt2 11454 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3231a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 2)
3321, 5, 23, 30, 32lttrd 10457 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 2)
34 chpeq0 25240 . . . . . . . . . . . . . . . . . . 19 ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2))
3521, 34syl 17 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2))
3633, 35mpbird 248 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0)
3736oveq1d 6861 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
3820, 37eqtrd 2799 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
3938fveq2d 6383 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))))
40 0red 10301 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ∈ ℝ)
4117rpge0d 12081 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 / ((⌊‘𝑥) + 1)))
4240, 21, 41abssuble0d 14472 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))) = ((𝑥 / ((⌊‘𝑥) + 1)) − 0))
4321recnd 10326 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℂ)
4443subid1d 10640 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) − 0) = (𝑥 / ((⌊‘𝑥) + 1)))
4539, 42, 443eqtrd 2803 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (𝑥 / ((⌊‘𝑥) + 1)))
4613nn0red 11604 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ)
47 pntsval.1 . . . . . . . . . . . . . . . . 17 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
4847pntsval2 25572 . . . . . . . . . . . . . . . 16 ((⌊‘𝑥) ∈ ℝ → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
4946, 48syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
5013nn0cnd 11605 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℂ)
51 1cnd 10292 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
5250, 51pncand 10652 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
5352fveq2d 6383 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘(⌊‘𝑥)))
5447pntsval2 25572 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝑆𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
552, 54syl 17 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
56 flidm 12825 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
572, 56syl 17 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
5857oveq2d 6862 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘(⌊‘𝑥))) = (1...(⌊‘𝑥)))
5958sumeq1d 14732 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
6055, 59eqtr4d 2802 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆𝑥) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
6149, 53, 603eqtr4d 2809 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆𝑥))
6252fveq2d 6383 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(((⌊‘𝑥) + 1) − 1)) = (𝑇‘(⌊‘𝑥)))
6362oveq2d 6862 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))) = (2 · (𝑇‘(⌊‘𝑥))))
6461, 63oveq12d 6864 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))) = ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))
6545, 64oveq12d 6864 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
662recnd 10326 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
6766div1d 11052 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / 1) = 𝑥)
6867fveq2d 6383 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) = (𝑅𝑥))
6918pntrf 25559 . . . . . . . . . . . . . . . . . . 19 𝑅:ℝ+⟶ℝ
7069ffvelrni 6552 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ+ → (𝑅𝑥) ∈ ℝ)
7110, 70syl 17 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅𝑥) ∈ ℝ)
7268, 71eqeltrd 2844 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℝ)
7372recnd 10326 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℂ)
7473abscld 14476 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℝ)
7574recnd 10326 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℂ)
7675mul01d 10494 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / 1))) · 0) = 0)
7765, 76oveq12d 6864 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0))
7847pntsf 25569 . . . . . . . . . . . . . . . . 17 𝑆:ℝ⟶ℝ
7978ffvelrni 6552 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → (𝑆𝑥) ∈ ℝ)
802, 79syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆𝑥) ∈ ℝ)
81 pntrlog2bnd.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))
82 relogcl 24629 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℝ+ → (log‘𝑎) ∈ ℝ)
83 remulcl 10278 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ℝ ∧ (log‘𝑎) ∈ ℝ) → (𝑎 · (log‘𝑎)) ∈ ℝ)
8482, 83sylan2 586 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+) → (𝑎 · (log‘𝑎)) ∈ ℝ)
85 0red 10301 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ ∧ ¬ 𝑎 ∈ ℝ+) → 0 ∈ ℝ)
8684, 85ifclda 4279 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) ∈ ℝ)
8781, 86fmpti 6576 . . . . . . . . . . . . . . . . . 18 𝑇:ℝ⟶ℝ
8887ffvelrni 6552 . . . . . . . . . . . . . . . . 17 ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
8946, 88syl 17 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
9023, 89remulcld 10328 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℝ)
9180, 90resubcld 10717 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℝ)
9221, 91remulcld 10328 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℝ)
9392recnd 10326 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℂ)
9493subid1d 10640 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
9577, 94eqtrd 2799 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
962flcld 12814 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℤ)
97 fzval3 12752 . . . . . . . . . . . . . 14 ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9896, 97syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9998eqcomd 2771 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
10010adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
101 elfznn 12584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
102101adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
103102nnrpd 12075 . . . . . . . . . . . . . . . . . . . . 21 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
104100, 103rpdivcld 12094 . . . . . . . . . . . . . . . . . . . 20 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
10569ffvelrni 6552 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . 19 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
107106recnd 10326 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ)
108107abscld 14476 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
109108recnd 10326 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
1103a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ+)
111103, 110rpaddcld 12092 . . . . . . . . . . . . . . . . . . . . 21 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℝ+)
112100, 111rpdivcld 12094 . . . . . . . . . . . . . . . . . . . 20 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / (𝑛 + 1)) ∈ ℝ+)
11369ffvelrni 6552 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 / (𝑛 + 1)) ∈ ℝ+ → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
114112, 113syl 17 . . . . . . . . . . . . . . . . . . 19 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
115114recnd 10326 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ)
116115abscld 14476 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ)
117116recnd 10326 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℂ)
118109, 117negsubdi2d 10667 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) = ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))))
119118eqcomd 2771 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))))
120102nncnd 11297 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
121 1cnd 10292 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
122120, 121pncand 10652 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
123122fveq2d 6383 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘((𝑛 + 1) − 1)) = (𝑆𝑛))
124122fveq2d 6383 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑇𝑛))
125 rpre 12043 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ+𝑛 ∈ ℝ)
126 eleq1 2832 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑛 → (𝑎 ∈ ℝ+𝑛 ∈ ℝ+))
127 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑛𝑎 = 𝑛)
128 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛))
129127, 128oveq12d 6864 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛)))
130126, 129ifbieq1d 4268 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑛 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
131 ovex 6878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 · (log‘𝑛)) ∈ V
132 c0ex 10291 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
133131, 132ifex 4293 . . . . . . . . . . . . . . . . . . . . 21 if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0) ∈ V
134130, 81, 133fvmpt 6475 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ → (𝑇𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
135125, 134syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ → (𝑇𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
136 iftrue 4251 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ → if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0) = (𝑛 · (log‘𝑛)))
137135, 136eqtrd 2799 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ+ → (𝑇𝑛) = (𝑛 · (log‘𝑛)))
138103, 137syl 17 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇𝑛) = (𝑛 · (log‘𝑛)))
139124, 138eqtrd 2799 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑛 · (log‘𝑛)))
140139oveq2d 6862 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑛 · (log‘𝑛))))
141123, 140oveq12d 6864 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))
142119, 141oveq12d 6864 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
143108, 116resubcld 10717 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ)
144143recnd 10326 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ)
145102nnred 11296 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
14678ffvelrni 6552 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑆𝑛) ∈ ℝ)
147145, 146syl 17 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆𝑛) ∈ ℝ)
14822a1i 11 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
149103relogcld 24676 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
150145, 149remulcld 10328 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (log‘𝑛)) ∈ ℝ)
151148, 150remulcld 10328 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑛 · (log‘𝑛))) ∈ ℝ)
152147, 151resubcld 10717 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℝ)
153152recnd 10326 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℂ)
154144, 153mulneg1d 10742 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
155142, 154eqtrd 2799 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
15699, 155sumeq12rdv 14739 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
157 fzfid 12987 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
158143, 152remulcld 10328 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
159158recnd 10326 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
160157, 159fsumneg 14819 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
161156, 160eqtrd 2799 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
16295, 161oveq12d 6864 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))))
163 oveq2 6854 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝑥 / 𝑚) = (𝑥 / 𝑛))
164163fveq2d 6383 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 𝑛)))
165164fveq2d 6383 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))))
166 fvoveq1 6869 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (𝑆‘(𝑚 − 1)) = (𝑆‘(𝑛 − 1)))
167 fvoveq1 6869 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝑇‘(𝑚 − 1)) = (𝑇‘(𝑛 − 1)))
168167oveq2d 6862 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(𝑛 − 1))))
169166, 168oveq12d 6864 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))
170165, 169jca 507 . . . . . . . . . . 11 (𝑚 = 𝑛 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
171 oveq2 6854 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 + 1) → (𝑥 / 𝑚) = (𝑥 / (𝑛 + 1)))
172171fveq2d 6383 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / (𝑛 + 1))))
173172fveq2d 6383 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))
174 fvoveq1 6869 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘((𝑛 + 1) − 1)))
175 fvoveq1 6869 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘((𝑛 + 1) − 1)))
176175oveq2d 6862 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘((𝑛 + 1) − 1))))
177174, 176oveq12d 6864 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))
178173, 177jca 507 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))))
179 oveq2 6854 . . . . . . . . . . . . . 14 (𝑚 = 1 → (𝑥 / 𝑚) = (𝑥 / 1))
180179fveq2d 6383 . . . . . . . . . . . . 13 (𝑚 = 1 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 1)))
181180fveq2d 6383 . . . . . . . . . . . 12 (𝑚 = 1 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))))
182 oveq1 6853 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
183 1m1e0 11349 . . . . . . . . . . . . . . . . 17 (1 − 1) = 0
184182, 183syl6eq 2815 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑚 − 1) = 0)
185184fveq2d 6383 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = (𝑆‘0))
186 0re 10299 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
187 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 0 → (⌊‘𝑎) = (⌊‘0))
188 0z 11640 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℤ
189 flid 12824 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ ℤ → (⌊‘0) = 0)
190188, 189ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (⌊‘0) = 0
191187, 190syl6eq 2815 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 0 → (⌊‘𝑎) = 0)
192191oveq2d 6862 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 0 → (1...(⌊‘𝑎)) = (1...0))
193 fz10 12576 . . . . . . . . . . . . . . . . . . . 20 (1...0) = ∅
194192, 193syl6eq 2815 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 0 → (1...(⌊‘𝑎)) = ∅)
195194sumeq1d 14732 . . . . . . . . . . . . . . . . . 18 (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
196 sum0 14753 . . . . . . . . . . . . . . . . . 18 Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0
197195, 196syl6eq 2815 . . . . . . . . . . . . . . . . 17 (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0)
198197, 47, 132fvmpt 6475 . . . . . . . . . . . . . . . 16 (0 ∈ ℝ → (𝑆‘0) = 0)
199186, 198ax-mp 5 . . . . . . . . . . . . . . 15 (𝑆‘0) = 0
200185, 199syl6eq 2815 . . . . . . . . . . . . . 14 (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = 0)
201184fveq2d 6383 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = (𝑇‘0))
202 rpne0 12053 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℝ+𝑎 ≠ 0)
203202necon2bi 2967 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 0 → ¬ 𝑎 ∈ ℝ+)
204203iffalsed 4256 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 0 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = 0)
205204, 81, 132fvmpt 6475 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → (𝑇‘0) = 0)
206186, 205ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑇‘0) = 0
207201, 206syl6eq 2815 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = 0)
208207oveq2d 6862 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = (2 · 0))
209 2t0e0 11452 . . . . . . . . . . . . . . 15 (2 · 0) = 0
210208, 209syl6eq 2815 . . . . . . . . . . . . . 14 (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = 0)
211200, 210oveq12d 6864 . . . . . . . . . . . . 13 (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = (0 − 0))
212 0m0e0 11404 . . . . . . . . . . . . 13 (0 − 0) = 0
213211, 212syl6eq 2815 . . . . . . . . . . . 12 (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0)
214181, 213jca 507 . . . . . . . . . . 11 (𝑚 = 1 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0))
215 oveq2 6854 . . . . . . . . . . . . . 14 (𝑚 = ((⌊‘𝑥) + 1) → (𝑥 / 𝑚) = (𝑥 / ((⌊‘𝑥) + 1)))
216215fveq2d 6383 . . . . . . . . . . . . 13 (𝑚 = ((⌊‘𝑥) + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))))
217216fveq2d 6383 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))))
218 fvoveq1 6869 . . . . . . . . . . . . 13 (𝑚 = ((⌊‘𝑥) + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘(((⌊‘𝑥) + 1) − 1)))
219 fvoveq1 6869 . . . . . . . . . . . . . 14 (𝑚 = ((⌊‘𝑥) + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘(((⌊‘𝑥) + 1) − 1)))
220219oveq2d 6862 . . . . . . . . . . . . 13 (𝑚 = ((⌊‘𝑥) + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))
221218, 220oveq12d 6864 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))))
222217, 221jca 507 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))))
223 nnuz 11930 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
22415, 223syl6eleq 2854 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ (ℤ‘1))
22510adantr 472 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑥 ∈ ℝ+)
226 elfznn 12584 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
227226adantl 473 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
228227nnrpd 12075 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ+)
229225, 228rpdivcld 12094 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑥 / 𝑚) ∈ ℝ+)
23069ffvelrni 6552 . . . . . . . . . . . . . . 15 ((𝑥 / 𝑚) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
231229, 230syl 17 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
232231recnd 10326 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℂ)
233232abscld 14476 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℝ)
234233recnd 10326 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℂ)
235227nnred 11296 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
236 1red 10298 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 1 ∈ ℝ)
237235, 236resubcld 10717 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
23878ffvelrni 6552 . . . . . . . . . . . . . 14 ((𝑚 − 1) ∈ ℝ → (𝑆‘(𝑚 − 1)) ∈ ℝ)
239237, 238syl 17 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑆‘(𝑚 − 1)) ∈ ℝ)
24022a1i 11 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 2 ∈ ℝ)
24187ffvelrni 6552 . . . . . . . . . . . . . . 15 ((𝑚 − 1) ∈ ℝ → (𝑇‘(𝑚 − 1)) ∈ ℝ)
242237, 241syl 17 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑇‘(𝑚 − 1)) ∈ ℝ)
243240, 242remulcld 10328 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (2 · (𝑇‘(𝑚 − 1))) ∈ ℝ)
244239, 243resubcld 10717 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℝ)
245244recnd 10326 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℂ)
246170, 178, 214, 222, 224, 234, 245fsumparts 14838 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))))
247147recnd 10326 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆𝑛) ∈ ℂ)
24887ffvelrni 6552 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑇𝑛) ∈ ℝ)
249145, 248syl 17 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇𝑛) ∈ ℝ)
250148, 249remulcld 10328 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇𝑛)) ∈ ℝ)
251250recnd 10326 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇𝑛)) ∈ ℂ)
252 1red 10298 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
253145, 252resubcld 10717 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
25478ffvelrni 6552 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) ∈ ℝ → (𝑆‘(𝑛 − 1)) ∈ ℝ)
255253, 254syl 17 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ)
256255recnd 10326 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ)
25787ffvelrni 6552 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℝ → (𝑇‘(𝑛 − 1)) ∈ ℝ)
258253, 257syl 17 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ)
259148, 258remulcld 10328 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℝ)
260259recnd 10326 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℂ)
261247, 251, 256, 260sub4d 10700 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (2 · (𝑇𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
262124oveq2d 6862 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑇𝑛)))
263123, 262oveq12d 6864 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆𝑛) − (2 · (𝑇𝑛))))
264263oveq1d 6861 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆𝑛) − (2 · (𝑇𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
265 2cnd 11355 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
266249recnd 10326 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇𝑛) ∈ ℂ)
267258recnd 10326 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℂ)
268265, 266, 267subdid 10745 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) = ((2 · (𝑇𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))
269268oveq2d 6862 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) = (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
270261, 264, 2693eqtr4d 2809 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
271270oveq2d 6862 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
27299, 271sumeq12rdv 14739 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
273246, 272eqtr3d 2801 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
274157, 159fsumcl 14765 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
27593, 274subnegd 10658 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))))
276162, 273, 2753eqtr3rd 2808 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
27710relogcld 24676 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
278277recnd 10326 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
27966, 278mulcomd 10319 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) = ((log‘𝑥) · 𝑥))
280276, 279oveq12d 6864 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
281147, 255resubcld 10717 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℝ)
282249, 258resubcld 10717 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℝ)
283148, 282remulcld 10328 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
284281, 283resubcld 10717 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℝ)
285108, 284remulcld 10328 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
286157, 285fsumrecl 14766 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
287286recnd 10326 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
2882, 8rplogcld 24682 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ+)
289288rpne0d 12082 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
29010rpne0d 12082 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
291287, 278, 66, 289, 290divdiv1d 11091 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
292280, 291eqtr4d 2802 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥))
293292oveq2d 6862 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥)))
29471recnd 10326 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅𝑥) ∈ ℂ)
295294abscld 14476 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅𝑥)) ∈ ℝ)
296295, 277remulcld 10328 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅𝑥)) · (log‘𝑥)) ∈ ℝ)
297108, 281remulcld 10328 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
298157, 297fsumrecl 14766 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
299298, 288rerpdivcld 12108 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℝ)
300296, 299resubcld 10717 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℝ)
301300recnd 10326 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℂ)
302287, 278, 289divcld 11060 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) ∈ ℂ)
303301, 302, 66, 290divdird 11098 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) / 𝑥) = (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥)))
304296recnd 10326 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅𝑥)) · (log‘𝑥)) ∈ ℂ)
305299recnd 10326 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℂ)
306304, 305, 302subsubd 10679 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) = ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))))
307 2cnd 11355 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
308266, 267subcld 10651 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℂ)
309109, 308mulcld 10318 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
310157, 307, 309fsummulc2 14816 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
311281recnd 10326 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℂ)
312265, 308mulcld 10318 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
313311, 312nncand 10656 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) = (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))
314313oveq2d 6862 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
315284recnd 10326 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℂ)
316109, 311, 315subdid 10745 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))))
317109, 265, 308mul12d 10504 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
318314, 316, 3173eqtr3d 2807 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
319318sumeq2dv 14734 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
320297recnd 10326 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
321285recnd 10326 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
322157, 320, 321fsumsub 14820 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))))
323310, 319, 3223eqtr2rd 2806 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
324323oveq1d 6861 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)))
325298recnd 10326 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
326325, 287, 278, 289divsubdird 11099 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))))
327108, 282remulcld 10328 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
328157, 327fsumrecl 14766 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
329328recnd 10326 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
330307, 329, 278, 289div23d 11097 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
331324, 326, 3303eqtr3d 2807 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
332331oveq2d 6862 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) = (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
333306, 332eqtr3d 2801 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
334333oveq1d 6861 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) / 𝑥) = ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥))
335293, 303, 3343eqtr2d 2805 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥))
336335mpteq2dva 4905 . . 3 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) = (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)))
337300, 10rerpdivcld 12108 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ)
338157, 158fsumrecl 14766 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
33992, 338readdcld 10327 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ)
34010, 288rpmulcld 12093 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ+)
341339, 340rerpdivcld 12108 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
34247, 18pntrlog2bndlem1 25573 . . . . 5 (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)
343342a1i 11 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1))
344340rpcnd 12079 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
345340rpne0d 12082 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0)
34693, 274, 344, 345divdird 11098 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
34791recnd 10326 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℂ)
34843, 347, 344, 345divassd 11095 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) = ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))))
349348oveq1d 6861 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
350346, 349eqtrd 2799 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
351350mpteq2dva 4905 . . . . 5 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))))
35291, 340rerpdivcld 12108 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
35321, 352remulcld 10328 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ℝ)
354338, 340rerpdivcld 12108 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
355 ioossre 12444 . . . . . . . . 9 (1(,)+∞) ⊆ ℝ
356355a1i 11 . . . . . . . 8 (⊤ → (1(,)+∞) ⊆ ℝ)
357 1red 10298 . . . . . . . 8 (⊤ → 1 ∈ ℝ)
35821, 5, 30ltled 10444 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
359358adantrr 708 . . . . . . . 8 ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
360356, 21, 357, 357, 359ello1d 14555 . . . . . . 7 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (𝑥 / ((⌊‘𝑥) + 1))) ∈ ≤𝑂(1))
36180recnd 10326 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆𝑥) ∈ ℂ)
36290recnd 10326 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℂ)
363361, 362, 344, 345divsubdird 11099 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) = (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))))
364363mpteq2dva 4905 . . . . . . . . 9 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))))
36580, 340rerpdivcld 12108 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) / (𝑥 · (log‘𝑥))) ∈ ℝ)
36690, 340rerpdivcld 12108 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
367 2cnd 11355 . . . . . . . . . . . 12 (⊤ → 2 ∈ ℂ)
368 o1const 14651 . . . . . . . . . . . 12 (((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
369355, 367, 368sylancr 581 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
370365recnd 10326 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) / (𝑥 · (log‘𝑥))) ∈ ℂ)
37180, 10rerpdivcld 12108 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) / 𝑥) ∈ ℝ)
372371recnd 10326 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) / 𝑥) ∈ ℂ)
373307, 278mulcld 10318 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ)
374372, 373, 278, 289divsubdird 11099 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))))
37523, 277remulcld 10328 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ)
376371, 375resubcld 10717 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℝ)
377376recnd 10326 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℂ)
378377, 278, 289divrecd 11063 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
379361, 66, 278, 290, 289divdiv1d 11091 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) / 𝑥) / (log‘𝑥)) = ((𝑆𝑥) / (𝑥 · (log‘𝑥))))
380307, 278, 289divcan4d 11066 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (log‘𝑥)) / (log‘𝑥)) = 2)
381379, 380oveq12d 6864 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))) = (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − 2))
382374, 378, 3813eqtr3rd 2808 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − 2) = ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
383382mpteq2dva 4905 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − 2)) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))))
3845, 288rerpdivcld 12108 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
38510ex 401 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ+))
386385ssrdv 3769 . . . . . . . . . . . . . . 15 (⊤ → (1(,)+∞) ⊆ ℝ+)
38747selbergs 25570 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ+ ↦ (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
388387a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ℝ+ ↦ (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
389386, 388o1res2 14595 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
390 divlogrlim 24688 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0
391 rlimo1 14648 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
392390, 391mp1i 13 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
393376, 384, 389, 392o1mul2 14656 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
394383, 393eqeltrd 2844 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − 2)) ∈ 𝑂(1))
395370, 307, 394o1dif 14661 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((𝑆𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1)))
396369, 395mpbird 248 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑆𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
39722a1i 11 . . . . . . . . . . . 12 (⊤ → 2 ∈ ℝ)
3982, 277remulcld 10328 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ)
399 2rp 12040 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
400399a1i 11 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ+)
401400rpge0d 12081 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ 2)
402 flge1nn 12837 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
4032, 9, 402syl2anc 579 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ)
404403nnrpd 12075 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ+)
405 rpre 12043 . . . . . . . . . . . . . . . . . . 19 ((⌊‘𝑥) ∈ ℝ+ → (⌊‘𝑥) ∈ ℝ)
406 eleq1 2832 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (⌊‘𝑥) → (𝑎 ∈ ℝ+ ↔ (⌊‘𝑥) ∈ ℝ+))
407 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (⌊‘𝑥) → 𝑎 = (⌊‘𝑥))
408 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (⌊‘𝑥) → (log‘𝑎) = (log‘(⌊‘𝑥)))
409407, 408oveq12d 6864 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (⌊‘𝑥) → (𝑎 · (log‘𝑎)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
410406, 409ifbieq1d 4268 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (⌊‘𝑥) → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
411 ovex 6878 . . . . . . . . . . . . . . . . . . . . 21 ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ∈ V
412411, 132ifex 4293 . . . . . . . . . . . . . . . . . . . 20 if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) ∈ V
413410, 81, 412fvmpt 6475 . . . . . . . . . . . . . . . . . . 19 ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
414405, 413syl 17 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑥) ∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
415 iftrue 4251 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑥) ∈ ℝ+ → if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
416414, 415eqtrd 2799 . . . . . . . . . . . . . . . . 17 ((⌊‘𝑥) ∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
417404, 416syl 17 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
418404relogcld 24676 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ∈ ℝ)
41913nn0ge0d 11606 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (⌊‘𝑥))
420403nnge1d 11325 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ (⌊‘𝑥))
42146, 420logge0d 24683 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (log‘(⌊‘𝑥)))
422 flle 12815 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
4232, 422syl 17 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ≤ 𝑥)
424404, 10logled 24680 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) ≤ 𝑥 ↔ (log‘(⌊‘𝑥)) ≤ (log‘𝑥)))
425423, 424mpbid 223 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ≤ (log‘𝑥))
42646, 2, 418, 277, 419, 421, 423, 425lemul12ad 11225 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ≤ (𝑥 · (log‘𝑥)))
427417, 426eqbrtrd 4833 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ≤ (𝑥 · (log‘𝑥)))
42889, 398, 23, 401, 427lemul2ad 11223 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥))))
42990, 23, 340ledivmul2d 12131 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2 ↔ (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥)))))
430428, 429mpbird 248 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2)
431430adantrr 708 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2)
432356, 366, 357, 397, 431ello1d 14555 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
433 0red 10301 . . . . . . . . . . . 12 (⊤ → 0 ∈ ℝ)
43446, 418, 419, 421mulge0d 10863 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
435434, 417breqtrrd 4839 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑇‘(⌊‘𝑥)))
43623, 89, 401, 435mulge0d 10863 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (2 · (𝑇‘(⌊‘𝑥))))
43790, 340, 436divge0d 12117 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))
438366, 433, 437o1lo12 14570 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1)))
439432, 438mpbird 248 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
440365, 366, 396, 439o1sub2 14657 . . . . . . . . 9 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1))
441364, 440eqeltrd 2844 . . . . . . . 8 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
442352, 441o1lo1d 14571 . . . . . . 7 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
44321, 352, 360, 442, 41lo1mul 14659 . . . . . 6 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
44447selbergsb 25571 . . . . . . . 8 𝑐 ∈ ℝ+𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐
445 simpl 474 . . . . . . . . . 10 ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → 𝑐 ∈ ℝ+)
446 simpr 477 . . . . . . . . . 10 ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐)
44747, 18, 445, 446pntrlog2bndlem3 25575 . . . . . . . . 9 ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
448447rexlimiva 3175 . . . . . . . 8 (∃𝑐 ∈ ℝ+𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
449444, 448mp1i 13 . . . . . . 7 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
450354, 449o1lo1d 14571 . . . . . 6 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
451353, 354, 443, 450lo1add 14658 . . . . 5 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
452351, 451eqeltrd 2844 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
453337, 341, 343, 452lo1add 14658 . . 3 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
454336, 453eqeltrrd 2845 . 2 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1))
455454mptru 1660 1 (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wa 384   = wceq 1652  wtru 1653  wcel 2155  wral 3055  wrex 3056  {crab 3059  wss 3734  c0 4081  ifcif 4245   class class class wbr 4811  cmpt 4890  cfv 6070  (class class class)co 6846  cc 10191  cr 10192  0cc0 10193  1c1 10194   + caddc 10196   · cmul 10198  +∞cpnf 10329   < clt 10332  cle 10333  cmin 10525  -cneg 10526   / cdiv 10943  cn 11279  2c2 11332  0cn0 11543  cz 11629  cuz 11893  +crp 12035  (,)cioo 12384  [,)cico 12386  ...cfz 12540  ..^cfzo 12680  cfl 12806  abscabs 14275  𝑟 crli 14517  𝑂(1)co1 14518  ≤𝑂(1)clo1 14519  Σcsu 14717  cdvds 15281  logclog 24608  Λcvma 25125  ψcchp 25126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271  ax-addf 10272  ax-mulf 10273
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-disj 4780  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-of 7099  df-om 7268  df-1st 7370  df-2nd 7371  df-supp 7502  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-ixp 8118  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fsupp 8487  df-fi 8528  df-sup 8559  df-inf 8560  df-oi 8626  df-card 9020  df-cda 9247  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10527  df-neg 10528  df-div 10944  df-nn 11280  df-2 11340  df-3 11341  df-4 11342  df-5 11343  df-6 11344  df-7 11345  df-8 11346  df-9 11347  df-n0 11544  df-xnn0 11616  df-z 11630  df-dec 11747  df-uz 11894  df-q 11997  df-rp 12036  df-xneg 12153  df-xadd 12154  df-xmul 12155  df-ioo 12388  df-ioc 12389  df-ico 12390  df-icc 12391  df-fz 12541  df-fzo 12681  df-fl 12808  df-mod 12884  df-seq 13016  df-exp 13075  df-fac 13272  df-bc 13301  df-hash 13329  df-shft 14108  df-cj 14140  df-re 14141  df-im 14142  df-sqrt 14276  df-abs 14277  df-limsup 14503  df-clim 14520  df-rlim 14521  df-o1 14522  df-lo1 14523  df-sum 14718  df-ef 15096  df-e 15097  df-sin 15098  df-cos 15099  df-pi 15101  df-dvds 15282  df-gcd 15514  df-prm 15682  df-pc 15837  df-struct 16148  df-ndx 16149  df-slot 16150  df-base 16152  df-sets 16153  df-ress 16154  df-plusg 16243  df-mulr 16244  df-starv 16245  df-sca 16246  df-vsca 16247  df-ip 16248  df-tset 16249  df-ple 16250  df-ds 16252  df-unif 16253  df-hom 16254  df-cco 16255  df-rest 16365  df-topn 16366  df-0g 16384  df-gsum 16385  df-topgen 16386  df-pt 16387  df-prds 16390  df-xrs 16444  df-qtop 16449  df-imas 16450  df-xps 16452  df-mre 16528  df-mrc 16529  df-acs 16531  df-mgm 17524  df-sgrp 17566  df-mnd 17577  df-submnd 17618  df-mulg 17824  df-cntz 18029  df-cmn 18477  df-psmet 20027  df-xmet 20028  df-met 20029  df-bl 20030  df-mopn 20031  df-fbas 20032  df-fg 20033  df-cnfld 20036  df-top 20994  df-topon 21011  df-topsp 21033  df-bases 21046  df-cld 21119  df-ntr 21120  df-cls 21121  df-nei 21198  df-lp 21236  df-perf 21237  df-cn 21327  df-cnp 21328  df-haus 21415  df-cmp 21486  df-tx 21661  df-hmeo 21854  df-fil 21945  df-fm 22037  df-flim 22038  df-flf 22039  df-xms 22420  df-ms 22421  df-tms 22422  df-cncf 22976  df-limc 23937  df-dv 23938  df-log 24610  df-cxp 24611  df-em 25026  df-cht 25130  df-vma 25131  df-chp 25132  df-ppi 25133  df-mu 25134
This theorem is referenced by:  pntrlog2bndlem5  25577
  Copyright terms: Public domain W3C validator