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

Theorem pntrlog2bndlem4 27425
Description: Lemma for pntrlog2bnd 27429. 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 13361 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
21adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
3 1rp 12985 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ+
43a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ+)
5 1red 11222 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
6 eliooord 13390 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
76adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥𝑥 < +∞))
87simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
95, 2, 8ltled 11369 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
102, 4, 9rpgecld 13062 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ+)
1110rprege0d 13030 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
12 flge0nn0 13792 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ0)
14 nn0p1nn 12518 . . . . . . . . . . . . . . . . . . . 20 ((⌊‘𝑥) ∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ)
1513, 14syl 17 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℕ)
1615nnrpd 13021 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℝ+)
1710, 16rpdivcld 13040 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ+)
18 pntrlog2bnd.r . . . . . . . . . . . . . . . . . 18 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
1918pntrval 27407 . . . . . . . . . . . . . . . . 17 ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ+ → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
2017, 19syl 17 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
212, 15nndivred 12273 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ)
22 2re 12293 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
2322a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
24 flltp1 13772 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → 𝑥 < ((⌊‘𝑥) + 1))
252, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < ((⌊‘𝑥) + 1))
2615nncnd 12235 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℂ)
2726mulridd 11238 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) · 1) = ((⌊‘𝑥) + 1))
2825, 27breqtrrd 5176 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < (((⌊‘𝑥) + 1) · 1))
292, 5, 16ltdivmuld 13074 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) < 1 ↔ 𝑥 < (((⌊‘𝑥) + 1) · 1)))
3028, 29mpbird 257 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 1)
31 1lt2 12390 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3231a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 2)
3321, 5, 23, 30, 32lttrd 11382 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 2)
34 chpeq0 27053 . . . . . . . . . . . . . . . . . . 19 ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2))
3521, 34syl 17 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2))
3633, 35mpbird 257 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0)
3736oveq1d 7427 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
3820, 37eqtrd 2771 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
3938fveq2d 6895 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))))
40 0red 11224 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ∈ ℝ)
4117rpge0d 13027 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 / ((⌊‘𝑥) + 1)))
4240, 21, 41abssuble0d 15386 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))) = ((𝑥 / ((⌊‘𝑥) + 1)) − 0))
4321recnd 11249 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℂ)
4443subid1d 11567 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) − 0) = (𝑥 / ((⌊‘𝑥) + 1)))
4539, 42, 443eqtrd 2775 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (𝑥 / ((⌊‘𝑥) + 1)))
4613nn0red 12540 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ)
47 pntsval.1 . . . . . . . . . . . . . . . . 17 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
4847pntsval2 27421 . . . . . . . . . . . . . . . 16 ((⌊‘𝑥) ∈ ℝ → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
4946, 48syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
5013nn0cnd 12541 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℂ)
51 1cnd 11216 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
5250, 51pncand 11579 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
5352fveq2d 6895 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘(⌊‘𝑥)))
5447pntsval2 27421 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝑆𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
552, 54syl 17 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
56 flidm 13781 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
572, 56syl 17 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
5857oveq2d 7428 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘(⌊‘𝑥))) = (1...(⌊‘𝑥)))
5958sumeq1d 15654 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
6055, 59eqtr4d 2774 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆𝑥) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
6149, 53, 603eqtr4d 2781 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆𝑥))
6252fveq2d 6895 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(((⌊‘𝑥) + 1) − 1)) = (𝑇‘(⌊‘𝑥)))
6362oveq2d 7428 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))) = (2 · (𝑇‘(⌊‘𝑥))))
6461, 63oveq12d 7430 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))) = ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))
6545, 64oveq12d 7430 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
662recnd 11249 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
6766div1d 11989 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / 1) = 𝑥)
6867fveq2d 6895 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) = (𝑅𝑥))
6918pntrf 27408 . . . . . . . . . . . . . . . . . . 19 𝑅:ℝ+⟶ℝ
7069ffvelcdmi 7085 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ+ → (𝑅𝑥) ∈ ℝ)
7110, 70syl 17 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅𝑥) ∈ ℝ)
7268, 71eqeltrd 2832 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℝ)
7372recnd 11249 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℂ)
7473abscld 15390 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℝ)
7574recnd 11249 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℂ)
7675mul01d 11420 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / 1))) · 0) = 0)
7765, 76oveq12d 7430 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0))
7847pntsf 27418 . . . . . . . . . . . . . . . . 17 𝑆:ℝ⟶ℝ
7978ffvelcdmi 7085 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → (𝑆𝑥) ∈ ℝ)
802, 79syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆𝑥) ∈ ℝ)
81 pntrlog2bnd.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))
82 relogcl 26423 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℝ+ → (log‘𝑎) ∈ ℝ)
83 remulcl 11201 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ℝ ∧ (log‘𝑎) ∈ ℝ) → (𝑎 · (log‘𝑎)) ∈ ℝ)
8482, 83sylan2 592 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+) → (𝑎 · (log‘𝑎)) ∈ ℝ)
85 0red 11224 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ ∧ ¬ 𝑎 ∈ ℝ+) → 0 ∈ ℝ)
8684, 85ifclda 4563 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) ∈ ℝ)
8781, 86fmpti 7113 . . . . . . . . . . . . . . . . . 18 𝑇:ℝ⟶ℝ
8887ffvelcdmi 7085 . . . . . . . . . . . . . . . . 17 ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
8946, 88syl 17 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
9023, 89remulcld 11251 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℝ)
9180, 90resubcld 11649 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℝ)
9221, 91remulcld 11251 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℝ)
9392recnd 11249 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℂ)
9493subid1d 11567 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
9577, 94eqtrd 2771 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
962flcld 13770 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℤ)
97 fzval3 13708 . . . . . . . . . . . . . 14 ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9896, 97syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9998eqcomd 2737 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
10010adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
101 elfznn 13537 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
102101adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
103102nnrpd 13021 . . . . . . . . . . . . . . . . . . . . 21 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
104100, 103rpdivcld 13040 . . . . . . . . . . . . . . . . . . . 20 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
10569ffvelcdmi 7085 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . 19 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
107106recnd 11249 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ)
108107abscld 15390 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
109108recnd 11249 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
1103a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ+)
111103, 110rpaddcld 13038 . . . . . . . . . . . . . . . . . . . . 21 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℝ+)
112100, 111rpdivcld 13040 . . . . . . . . . . . . . . . . . . . 20 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / (𝑛 + 1)) ∈ ℝ+)
11369ffvelcdmi 7085 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 / (𝑛 + 1)) ∈ ℝ+ → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
114112, 113syl 17 . . . . . . . . . . . . . . . . . . 19 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
115114recnd 11249 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ)
116115abscld 15390 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ)
117116recnd 11249 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℂ)
118109, 117negsubdi2d 11594 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) = ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))))
119118eqcomd 2737 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))))
120102nncnd 12235 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
121 1cnd 11216 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
122120, 121pncand 11579 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
123122fveq2d 6895 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘((𝑛 + 1) − 1)) = (𝑆𝑛))
124122fveq2d 6895 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑇𝑛))
125 rpre 12989 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ+𝑛 ∈ ℝ)
126 eleq1 2820 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑛 → (𝑎 ∈ ℝ+𝑛 ∈ ℝ+))
127 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑛𝑎 = 𝑛)
128 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛))
129127, 128oveq12d 7430 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛)))
130126, 129ifbieq1d 4552 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑛 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
131 ovex 7445 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 · (log‘𝑛)) ∈ V
132 c0ex 11215 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
133131, 132ifex 4578 . . . . . . . . . . . . . . . . . . . . 21 if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0) ∈ V
134130, 81, 133fvmpt 6998 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ → (𝑇𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
135125, 134syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ → (𝑇𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
136 iftrue 4534 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ → if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0) = (𝑛 · (log‘𝑛)))
137135, 136eqtrd 2771 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ+ → (𝑇𝑛) = (𝑛 · (log‘𝑛)))
138103, 137syl 17 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇𝑛) = (𝑛 · (log‘𝑛)))
139124, 138eqtrd 2771 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑛 · (log‘𝑛)))
140139oveq2d 7428 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑛 · (log‘𝑛))))
141123, 140oveq12d 7430 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))
142119, 141oveq12d 7430 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
143108, 116resubcld 11649 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ)
144143recnd 11249 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ)
145102nnred 12234 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
14678ffvelcdmi 7085 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑆𝑛) ∈ ℝ)
147145, 146syl 17 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆𝑛) ∈ ℝ)
14822a1i 11 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
149103relogcld 26470 . . . . . . . . . . . . . . . . . 18 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
150145, 149remulcld 11251 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (log‘𝑛)) ∈ ℝ)
151148, 150remulcld 11251 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑛 · (log‘𝑛))) ∈ ℝ)
152147, 151resubcld 11649 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℝ)
153152recnd 11249 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℂ)
154144, 153mulneg1d 11674 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
155142, 154eqtrd 2771 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
15699, 155sumeq12rdv 15660 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
157 fzfid 13945 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
158143, 152remulcld 11251 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
159158recnd 11249 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
160157, 159fsumneg 15740 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
161156, 160eqtrd 2771 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))))
16295, 161oveq12d 7430 . . . . . . . . 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 7420 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝑥 / 𝑚) = (𝑥 / 𝑛))
164163fveq2d 6895 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 𝑛)))
165164fveq2d 6895 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))))
166 fvoveq1 7435 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (𝑆‘(𝑚 − 1)) = (𝑆‘(𝑛 − 1)))
167 fvoveq1 7435 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝑇‘(𝑚 − 1)) = (𝑇‘(𝑛 − 1)))
168167oveq2d 7428 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(𝑛 − 1))))
169166, 168oveq12d 7430 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))
170165, 169jca 511 . . . . . . . . . . 11 (𝑚 = 𝑛 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
171 oveq2 7420 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 + 1) → (𝑥 / 𝑚) = (𝑥 / (𝑛 + 1)))
172171fveq2d 6895 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / (𝑛 + 1))))
173172fveq2d 6895 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))
174 fvoveq1 7435 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘((𝑛 + 1) − 1)))
175 fvoveq1 7435 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘((𝑛 + 1) − 1)))
176175oveq2d 7428 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘((𝑛 + 1) − 1))))
177174, 176oveq12d 7430 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))
178173, 177jca 511 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))))
179 oveq2 7420 . . . . . . . . . . . . . 14 (𝑚 = 1 → (𝑥 / 𝑚) = (𝑥 / 1))
180179fveq2d 6895 . . . . . . . . . . . . 13 (𝑚 = 1 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 1)))
181180fveq2d 6895 . . . . . . . . . . . 12 (𝑚 = 1 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))))
182 oveq1 7419 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
183 1m1e0 12291 . . . . . . . . . . . . . . . . 17 (1 − 1) = 0
184182, 183eqtrdi 2787 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑚 − 1) = 0)
185184fveq2d 6895 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = (𝑆‘0))
186 0re 11223 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
187 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 0 → (⌊‘𝑎) = (⌊‘0))
188 0z 12576 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℤ
189 flid 13780 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ ℤ → (⌊‘0) = 0)
190188, 189ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (⌊‘0) = 0
191187, 190eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 0 → (⌊‘𝑎) = 0)
192191oveq2d 7428 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 0 → (1...(⌊‘𝑎)) = (1...0))
193 fz10 13529 . . . . . . . . . . . . . . . . . . . 20 (1...0) = ∅
194192, 193eqtrdi 2787 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 0 → (1...(⌊‘𝑎)) = ∅)
195194sumeq1d 15654 . . . . . . . . . . . . . . . . . 18 (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
196 sum0 15674 . . . . . . . . . . . . . . . . . 18 Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0
197195, 196eqtrdi 2787 . . . . . . . . . . . . . . . . 17 (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0)
198197, 47, 132fvmpt 6998 . . . . . . . . . . . . . . . 16 (0 ∈ ℝ → (𝑆‘0) = 0)
199186, 198ax-mp 5 . . . . . . . . . . . . . . 15 (𝑆‘0) = 0
200185, 199eqtrdi 2787 . . . . . . . . . . . . . 14 (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = 0)
201184fveq2d 6895 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = (𝑇‘0))
202 rpne0 12997 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℝ+𝑎 ≠ 0)
203202necon2bi 2970 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 0 → ¬ 𝑎 ∈ ℝ+)
204203iffalsed 4539 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 0 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = 0)
205204, 81, 132fvmpt 6998 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → (𝑇‘0) = 0)
206186, 205ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑇‘0) = 0
207201, 206eqtrdi 2787 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = 0)
208207oveq2d 7428 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = (2 · 0))
209 2t0e0 12388 . . . . . . . . . . . . . . 15 (2 · 0) = 0
210208, 209eqtrdi 2787 . . . . . . . . . . . . . 14 (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = 0)
211200, 210oveq12d 7430 . . . . . . . . . . . . 13 (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = (0 − 0))
212 0m0e0 12339 . . . . . . . . . . . . 13 (0 − 0) = 0
213211, 212eqtrdi 2787 . . . . . . . . . . . 12 (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0)
214181, 213jca 511 . . . . . . . . . . 11 (𝑚 = 1 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0))
215 oveq2 7420 . . . . . . . . . . . . . 14 (𝑚 = ((⌊‘𝑥) + 1) → (𝑥 / 𝑚) = (𝑥 / ((⌊‘𝑥) + 1)))
216215fveq2d 6895 . . . . . . . . . . . . 13 (𝑚 = ((⌊‘𝑥) + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))))
217216fveq2d 6895 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))))
218 fvoveq1 7435 . . . . . . . . . . . . 13 (𝑚 = ((⌊‘𝑥) + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘(((⌊‘𝑥) + 1) − 1)))
219 fvoveq1 7435 . . . . . . . . . . . . . 14 (𝑚 = ((⌊‘𝑥) + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘(((⌊‘𝑥) + 1) − 1)))
220219oveq2d 7428 . . . . . . . . . . . . 13 (𝑚 = ((⌊‘𝑥) + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))
221218, 220oveq12d 7430 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))))
222217, 221jca 511 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))))
223 nnuz 12872 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
22415, 223eleqtrdi 2842 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ (ℤ‘1))
22510adantr 480 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑥 ∈ ℝ+)
226 elfznn 13537 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
227226adantl 481 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
228227nnrpd 13021 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ+)
229225, 228rpdivcld 13040 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑥 / 𝑚) ∈ ℝ+)
23069ffvelcdmi 7085 . . . . . . . . . . . . . . 15 ((𝑥 / 𝑚) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
231229, 230syl 17 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
232231recnd 11249 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℂ)
233232abscld 15390 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℝ)
234233recnd 11249 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℂ)
235227nnred 12234 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
236 1red 11222 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 1 ∈ ℝ)
237235, 236resubcld 11649 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
23878ffvelcdmi 7085 . . . . . . . . . . . . . 14 ((𝑚 − 1) ∈ ℝ → (𝑆‘(𝑚 − 1)) ∈ ℝ)
239237, 238syl 17 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑆‘(𝑚 − 1)) ∈ ℝ)
24022a1i 11 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 2 ∈ ℝ)
24187ffvelcdmi 7085 . . . . . . . . . . . . . . 15 ((𝑚 − 1) ∈ ℝ → (𝑇‘(𝑚 − 1)) ∈ ℝ)
242237, 241syl 17 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑇‘(𝑚 − 1)) ∈ ℝ)
243240, 242remulcld 11251 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (2 · (𝑇‘(𝑚 − 1))) ∈ ℝ)
244239, 243resubcld 11649 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℝ)
245244recnd 11249 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℂ)
246170, 178, 214, 222, 224, 234, 245fsumparts 15759 . . . . . . . . . 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 11249 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆𝑛) ∈ ℂ)
24887ffvelcdmi 7085 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑇𝑛) ∈ ℝ)
249145, 248syl 17 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇𝑛) ∈ ℝ)
250148, 249remulcld 11251 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇𝑛)) ∈ ℝ)
251250recnd 11249 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇𝑛)) ∈ ℂ)
252 1red 11222 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
253145, 252resubcld 11649 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
25478ffvelcdmi 7085 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) ∈ ℝ → (𝑆‘(𝑛 − 1)) ∈ ℝ)
255253, 254syl 17 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ)
256255recnd 11249 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ)
25787ffvelcdmi 7085 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℝ → (𝑇‘(𝑛 − 1)) ∈ ℝ)
258253, 257syl 17 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ)
259148, 258remulcld 11251 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℝ)
260259recnd 11249 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℂ)
261247, 251, 256, 260sub4d 11627 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (2 · (𝑇𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
262124oveq2d 7428 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑇𝑛)))
263123, 262oveq12d 7430 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆𝑛) − (2 · (𝑇𝑛))))
264263oveq1d 7427 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆𝑛) − (2 · (𝑇𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
265 2cnd 12297 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
266249recnd 11249 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇𝑛) ∈ ℂ)
267258recnd 11249 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℂ)
268265, 266, 267subdid 11677 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) = ((2 · (𝑇𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))
269268oveq2d 7428 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) = (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
270261, 264, 2693eqtr4d 2781 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
271270oveq2d 7428 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
27299, 271sumeq12rdv 15660 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
273246, 272eqtr3d 2773 . . . . . . . . 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 15686 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
27593, 274subnegd 11585 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))))
276162, 273, 2753eqtr3rd 2780 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
27710relogcld 26470 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
278277recnd 11249 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
27966, 278mulcomd 11242 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) = ((log‘𝑥) · 𝑥))
280276, 279oveq12d 7430 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
281147, 255resubcld 11649 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℝ)
282249, 258resubcld 11649 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℝ)
283148, 282remulcld 11251 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
284281, 283resubcld 11649 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℝ)
285108, 284remulcld 11251 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
286157, 285fsumrecl 15687 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
287286recnd 11249 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
2882, 8rplogcld 26476 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ+)
289288rpne0d 13028 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
29010rpne0d 13028 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
291287, 278, 66, 289, 290divdiv1d 12028 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
292280, 291eqtr4d 2774 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥))
293292oveq2d 7428 . . . . 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 11249 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅𝑥) ∈ ℂ)
295294abscld 15390 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅𝑥)) ∈ ℝ)
296295, 277remulcld 11251 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅𝑥)) · (log‘𝑥)) ∈ ℝ)
297108, 281remulcld 11251 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
298157, 297fsumrecl 15687 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
299298, 288rerpdivcld 13054 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℝ)
300296, 299resubcld 11649 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℝ)
301300recnd 11249 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℂ)
302287, 278, 289divcld 11997 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) ∈ ℂ)
303301, 302, 66, 290divdird 12035 . . . . 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 11249 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅𝑥)) · (log‘𝑥)) ∈ ℂ)
305299recnd 11249 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℂ)
306304, 305, 302subsubd 11606 . . . . . . 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 12297 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
308266, 267subcld 11578 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℂ)
309109, 308mulcld 11241 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
310157, 307, 309fsummulc2 15737 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
311281recnd 11249 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℂ)
312265, 308mulcld 11241 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
313311, 312nncand 11583 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) = (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))
314313oveq2d 7428 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
315284recnd 11249 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℂ)
316109, 311, 315subdid 11677 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))))
317109, 265, 308mul12d 11430 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
318314, 316, 3173eqtr3d 2779 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
319318sumeq2dv 15656 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
320297recnd 11249 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
321285recnd 11249 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
322157, 320, 321fsumsub 15741 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))))
323310, 319, 3223eqtr2rd 2778 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
324323oveq1d 7427 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)))
325298recnd 11249 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
326325, 287, 278, 289divsubdird 12036 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))))
327108, 282remulcld 11251 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
328157, 327fsumrecl 15687 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
329328recnd 11249 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
330307, 329, 278, 289div23d 12034 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
331324, 326, 3303eqtr3d 2779 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))))
332331oveq2d 7428 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) = (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
333306, 332eqtr3d 2773 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
334333oveq1d 7427 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) / 𝑥) = ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥))
335293, 303, 3343eqtr2d 2777 . . . 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 5248 . . 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 13054 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ)
338157, 158fsumrecl 15687 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
33992, 338readdcld 11250 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ)
34010, 288rpmulcld 13039 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ+)
341339, 340rerpdivcld 13054 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
34247, 18pntrlog2bndlem1 27422 . . . . 5 (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)
343342a1i 11 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1))
344340rpcnd 13025 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
345340rpne0d 13028 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0)
34693, 274, 344, 345divdird 12035 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
34791recnd 11249 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℂ)
34843, 347, 344, 345divassd 12032 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) = ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))))
349348oveq1d 7427 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
350346, 349eqtrd 2771 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
351350mpteq2dva 5248 . . . . 5 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))))
35291, 340rerpdivcld 13054 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
35321, 352remulcld 11251 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ℝ)
354338, 340rerpdivcld 13054 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
355 ioossre 13392 . . . . . . . . 9 (1(,)+∞) ⊆ ℝ
356355a1i 11 . . . . . . . 8 (⊤ → (1(,)+∞) ⊆ ℝ)
357 1red 11222 . . . . . . . 8 (⊤ → 1 ∈ ℝ)
35821, 5, 30ltled 11369 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
359358adantrr 714 . . . . . . . 8 ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
360356, 21, 357, 357, 359ello1d 15474 . . . . . . 7 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (𝑥 / ((⌊‘𝑥) + 1))) ∈ ≤𝑂(1))
36180recnd 11249 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆𝑥) ∈ ℂ)
36290recnd 11249 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℂ)
363361, 362, 344, 345divsubdird 12036 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) = (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))))
364363mpteq2dva 5248 . . . . . . . . 9 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))))
36580, 340rerpdivcld 13054 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) / (𝑥 · (log‘𝑥))) ∈ ℝ)
36690, 340rerpdivcld 13054 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
367 2cnd 12297 . . . . . . . . . . . 12 (⊤ → 2 ∈ ℂ)
368 o1const 15571 . . . . . . . . . . . 12 (((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
369355, 367, 368sylancr 586 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
370365recnd 11249 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) / (𝑥 · (log‘𝑥))) ∈ ℂ)
37180, 10rerpdivcld 13054 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) / 𝑥) ∈ ℝ)
372371recnd 11249 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆𝑥) / 𝑥) ∈ ℂ)
373307, 278mulcld 11241 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ)
374372, 373, 278, 289divsubdird 12036 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))))
37523, 277remulcld 11251 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ)
376371, 375resubcld 11649 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℝ)
377376recnd 11249 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℂ)
378377, 278, 289divrecd 12000 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
379361, 66, 278, 290, 289divdiv1d 12028 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) / 𝑥) / (log‘𝑥)) = ((𝑆𝑥) / (𝑥 · (log‘𝑥))))
380307, 278, 289divcan4d 12003 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (log‘𝑥)) / (log‘𝑥)) = 2)
381379, 380oveq12d 7430 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))) = (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − 2))
382374, 378, 3813eqtr3rd 2780 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − 2) = ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
383382mpteq2dva 5248 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − 2)) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))))
3845, 288rerpdivcld 13054 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
38510ex 412 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ+))
386385ssrdv 3988 . . . . . . . . . . . . . . 15 (⊤ → (1(,)+∞) ⊆ ℝ+)
38747selbergs 27419 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ+ ↦ (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
388387a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ℝ+ ↦ (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
389386, 388o1res2 15514 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
390 divlogrlim 26482 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0
391 rlimo1 15568 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
392390, 391mp1i 13 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
393376, 384, 389, 392o1mul2 15576 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
394383, 393eqeltrd 2832 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − 2)) ∈ 𝑂(1))
395370, 307, 394o1dif 15581 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((𝑆𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1)))
396369, 395mpbird 257 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑆𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
39722a1i 11 . . . . . . . . . . . 12 (⊤ → 2 ∈ ℝ)
3982, 277remulcld 11251 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ)
399 2rp 12986 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
400399a1i 11 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ+)
401400rpge0d 13027 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ 2)
402 flge1nn 13793 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
4032, 9, 402syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ)
404403nnrpd 13021 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ+)
405 rpre 12989 . . . . . . . . . . . . . . . . . . 19 ((⌊‘𝑥) ∈ ℝ+ → (⌊‘𝑥) ∈ ℝ)
406 eleq1 2820 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (⌊‘𝑥) → (𝑎 ∈ ℝ+ ↔ (⌊‘𝑥) ∈ ℝ+))
407 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (⌊‘𝑥) → 𝑎 = (⌊‘𝑥))
408 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (⌊‘𝑥) → (log‘𝑎) = (log‘(⌊‘𝑥)))
409407, 408oveq12d 7430 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (⌊‘𝑥) → (𝑎 · (log‘𝑎)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
410406, 409ifbieq1d 4552 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (⌊‘𝑥) → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
411 ovex 7445 . . . . . . . . . . . . . . . . . . . . 21 ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ∈ V
412411, 132ifex 4578 . . . . . . . . . . . . . . . . . . . 20 if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) ∈ V
413410, 81, 412fvmpt 6998 . . . . . . . . . . . . . . . . . . 19 ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
414405, 413syl 17 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑥) ∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
415 iftrue 4534 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑥) ∈ ℝ+ → if((⌊‘𝑥) ∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
416414, 415eqtrd 2771 . . . . . . . . . . . . . . . . 17 ((⌊‘𝑥) ∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
417404, 416syl 17 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
418404relogcld 26470 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ∈ ℝ)
41913nn0ge0d 12542 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (⌊‘𝑥))
420403nnge1d 12267 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ (⌊‘𝑥))
42146, 420logge0d 26477 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (log‘(⌊‘𝑥)))
422 flle 13771 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
4232, 422syl 17 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ≤ 𝑥)
424404, 10logled 26474 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) ≤ 𝑥 ↔ (log‘(⌊‘𝑥)) ≤ (log‘𝑥)))
425423, 424mpbid 231 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ≤ (log‘𝑥))
42646, 2, 418, 277, 419, 421, 423, 425lemul12ad 12163 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ≤ (𝑥 · (log‘𝑥)))
427417, 426eqbrtrd 5170 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ≤ (𝑥 · (log‘𝑥)))
42889, 398, 23, 401, 427lemul2ad 12161 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥))))
42990, 23, 340ledivmul2d 13077 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2 ↔ (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥)))))
430428, 429mpbird 257 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2)
431430adantrr 714 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2)
432356, 366, 357, 397, 431ello1d 15474 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
433 0red 11224 . . . . . . . . . . . 12 (⊤ → 0 ∈ ℝ)
43446, 418, 419, 421mulge0d 11798 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
435434, 417breqtrrd 5176 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑇‘(⌊‘𝑥)))
43623, 89, 401, 435mulge0d 11798 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (2 · (𝑇‘(⌊‘𝑥))))
43790, 340, 436divge0d 13063 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))
438366, 433, 437o1lo12 15489 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1)))
439432, 438mpbird 257 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
440365, 366, 396, 439o1sub2 15577 . . . . . . . . 9 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1))
441364, 440eqeltrd 2832 . . . . . . . 8 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
442352, 441o1lo1d 15490 . . . . . . 7 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
44321, 352, 360, 442, 41lo1mul 15579 . . . . . 6 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
44447selbergsb 27420 . . . . . . . 8 𝑐 ∈ ℝ+𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐
445 simpl 482 . . . . . . . . . 10 ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → 𝑐 ∈ ℝ+)
446 simpr 484 . . . . . . . . . 10 ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐)
44747, 18, 445, 446pntrlog2bndlem3 27424 . . . . . . . . 9 ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
448447rexlimiva 3146 . . . . . . . 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 15490 . . . . . 6 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
451353, 354, 443, 450lo1add 15578 . . . . 5 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
452351, 451eqeltrd 2832 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
453337, 341, 343, 452lo1add 15578 . . 3 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
454336, 453eqeltrrd 2833 . 2 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1))
455454mptru 1547 1 (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 395   = wceq 1540  wtru 1541  wcel 2105  wral 3060  wrex 3069  {crab 3431  wss 3948  c0 4322  ifcif 4528   class class class wbr 5148  cmpt 5231  cfv 6543  (class class class)co 7412  cc 11114  cr 11115  0cc0 11116  1c1 11117   + caddc 11119   · cmul 11121  +∞cpnf 11252   < clt 11255  cle 11256  cmin 11451  -cneg 11452   / cdiv 11878  cn 12219  2c2 12274  0cn0 12479  cz 12565  cuz 12829  +crp 12981  (,)cioo 13331  [,)cico 13333  ...cfz 13491  ..^cfzo 13634  cfl 13762  abscabs 15188  𝑟 crli 15436  𝑂(1)co1 15437  ≤𝑂(1)clo1 15438  Σcsu 15639  cdvds 16204  logclog 26402  Λcvma 26936  ψcchp 26937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9642  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194  ax-addf 11195
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8152  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-2o 8473  df-oadd 8476  df-er 8709  df-map 8828  df-pm 8829  df-ixp 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9368  df-fi 9412  df-sup 9443  df-inf 9444  df-oi 9511  df-dju 9902  df-card 9940  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12480  df-xnn0 12552  df-z 12566  df-dec 12685  df-uz 12830  df-q 12940  df-rp 12982  df-xneg 13099  df-xadd 13100  df-xmul 13101  df-ioo 13335  df-ioc 13336  df-ico 13337  df-icc 13338  df-fz 13492  df-fzo 13635  df-fl 13764  df-mod 13842  df-seq 13974  df-exp 14035  df-fac 14241  df-bc 14270  df-hash 14298  df-shft 15021  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190  df-limsup 15422  df-clim 15439  df-rlim 15440  df-o1 15441  df-lo1 15442  df-sum 15640  df-ef 16018  df-e 16019  df-sin 16020  df-cos 16021  df-tan 16022  df-pi 16023  df-dvds 16205  df-gcd 16443  df-prm 16616  df-pc 16777  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-rest 17375  df-topn 17376  df-0g 17394  df-gsum 17395  df-topgen 17396  df-pt 17397  df-prds 17400  df-xrs 17455  df-qtop 17460  df-imas 17461  df-xps 17463  df-mre 17537  df-mrc 17538  df-acs 17540  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-submnd 18712  df-mulg 18994  df-cntz 19229  df-cmn 19698  df-psmet 21224  df-xmet 21225  df-met 21226  df-bl 21227  df-mopn 21228  df-fbas 21229  df-fg 21230  df-cnfld 21233  df-top 22715  df-topon 22732  df-topsp 22754  df-bases 22768  df-cld 22842  df-ntr 22843  df-cls 22844  df-nei 22921  df-lp 22959  df-perf 22960  df-cn 23050  df-cnp 23051  df-haus 23138  df-cmp 23210  df-tx 23385  df-hmeo 23578  df-fil 23669  df-fm 23761  df-flim 23762  df-flf 23763  df-xms 24145  df-ms 24146  df-tms 24147  df-cncf 24717  df-limc 25714  df-dv 25715  df-ulm 26227  df-log 26404  df-cxp 26405  df-atan 26712  df-em 26837  df-cht 26941  df-vma 26942  df-chp 26943  df-ppi 26944  df-mu 26945
This theorem is referenced by:  pntrlog2bndlem5  27426
  Copyright terms: Public domain W3C validator