Metamath Proof Explorer

Theorem pntrlog2bndlem4

Description: Lemma for pntrlog2bnd . Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypotheses pntsval.1 ⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
pntrlog2bnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntrlog2bnd.t ⊢ 𝑇 = ( 𝑎 ∈ ℝ ↦ if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) )
Assertion pntrlog2bndlem4 ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1)

Proof

Step Hyp Ref Expression
1 pntsval.1 ⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2 pntrlog2bnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
3 pntrlog2bnd.t ⊢ 𝑇 = ( 𝑎 ∈ ℝ ↦ if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) )
4 elioore ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
5 4 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
6 1rp ⊢ 1 ∈ ℝ+
7 6 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
8 1red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
9 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
10 9 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
11 10 simpld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
12 8 5 11 ltled ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
13 5 7 12 rpgecld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
14 13 rprege0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
15 flge0nn0 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
16 14 15 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
17 nn0p1nn ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
18 16 17 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
19 18 nnrpd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ+ )
20 13 19 rpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ+ )
21 2 pntrval ⊢ ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
22 20 21 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
23 5 18 nndivred ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ )
24 2re ⊢ 2 ∈ ℝ
25 24 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ )
26 flltp1 ⊢ ( 𝑥 ∈ ℝ → 𝑥 < ( ( ⌊ ‘ 𝑥 ) + 1 ) )
27 5 26 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 < ( ( ⌊ ‘ 𝑥 ) + 1 ) )
28 18 nncnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℂ )
29 28 mulridd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · 1 ) = ( ( ⌊ ‘ 𝑥 ) + 1 ) )
30 27 29 breqtrrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 < ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · 1 ) )
31 5 8 19 ltdivmuld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 1 ↔ 𝑥 < ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · 1 ) ) )
32 30 31 mpbird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 1 )
33 1lt2 ⊢ 1 < 2
34 33 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 2 )
35 23 8 25 32 34 lttrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 2 )
36 chpeq0 ⊢ ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ → ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = 0 ↔ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 2 ) )
37 23 36 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = 0 ↔ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 2 ) )
38 35 37 mpbird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = 0 )
39 38 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( 0 − ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
40 22 39 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( 0 − ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
41 40 fveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) = ( abs ‘ ( 0 − ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) )
42 0red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ∈ ℝ )
43 20 rpge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
44 42 23 43 abssuble0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 0 − ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) = ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 0 ) )
45 23 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℂ )
46 45 subid1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 0 ) = ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
47 41 44 46 3eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) = ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
48 16 nn0red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
49 1 pntsval2 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ → ( 𝑆 ‘ ( ⌊ ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( ⌊ ‘ 𝑥 ) ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
50 48 49 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑆 ‘ ( ⌊ ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( ⌊ ‘ 𝑥 ) ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
51 16 nn0cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℂ )
52 1cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℂ )
53 51 52 pncand ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑥 ) )
54 53 fveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( 𝑆 ‘ ( ⌊ ‘ 𝑥 ) ) )
55 1 pntsval2 ⊢ ( 𝑥 ∈ ℝ → ( 𝑆 ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
56 5 55 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑆 ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
57 flidm ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ ( ⌊ ‘ 𝑥 ) ) = ( ⌊ ‘ 𝑥 ) )
58 5 57 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ ( ⌊ ‘ 𝑥 ) ) = ( ⌊ ‘ 𝑥 ) )
59 58 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ ( ⌊ ‘ 𝑥 ) ) ) = ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
60 59 sumeq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( ⌊ ‘ 𝑥 ) ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
61 56 60 eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑆 ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( ⌊ ‘ 𝑥 ) ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
62 50 54 61 3eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( 𝑆 ‘ 𝑥 ) )
63 53 fveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) )
64 63 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) = ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) )
65 62 64 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) ) = ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) )
66 47 65 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) · ( ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) ) ) = ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) )
67 5 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
68 67 div1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 1 ) = 𝑥 )
69 68 fveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ ( 𝑥 / 1 ) ) = ( 𝑅 ‘ 𝑥 ) )
70 2 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
71 70 ffvelcdmi ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
72 13 71 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
73 69 72 eqeltrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ ( 𝑥 / 1 ) ) ∈ ℝ )
74 73 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ ( 𝑥 / 1 ) ) ∈ ℂ )
75 74 abscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 1 ) ) ) ∈ ℝ )
76 75 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 1 ) ) ) ∈ ℂ )
77 76 mul01d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 1 ) ) ) · 0 ) = 0 )
78 66 77 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) · ( ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) ) ) − ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 1 ) ) ) · 0 ) ) = ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) − 0 ) )
79 1 pntsf ⊢ 𝑆 : ℝ ⟶ ℝ
80 79 ffvelcdmi ⊢ ( 𝑥 ∈ ℝ → ( 𝑆 ‘ 𝑥 ) ∈ ℝ )
81 5 80 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ℝ )
82 relogcl ⊢ ( 𝑎 ∈ ℝ+ → ( log ‘ 𝑎 ) ∈ ℝ )
83 remulcl ⊢ ( ( 𝑎 ∈ ℝ ∧ ( log ‘ 𝑎 ) ∈ ℝ ) → ( 𝑎 · ( log ‘ 𝑎 ) ) ∈ ℝ )
84 82 83 sylan2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+ ) → ( 𝑎 · ( log ‘ 𝑎 ) ) ∈ ℝ )
85 0red ⊢ ( ( 𝑎 ∈ ℝ ∧ ¬ 𝑎 ∈ ℝ+ ) → 0 ∈ ℝ )
86 84 85 ifclda ⊢ ( 𝑎 ∈ ℝ → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) ∈ ℝ )
87 3 86 fmpti ⊢ 𝑇 : ℝ ⟶ ℝ
88 87 ffvelcdmi ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ → ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℝ )
89 48 88 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℝ )
90 25 89 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℝ )
91 81 90 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ∈ ℝ )
92 23 91 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) ∈ ℝ )
93 92 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) ∈ ℂ )
94 93 subid1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) − 0 ) = ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) )
95 78 94 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) · ( ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) ) ) − ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 1 ) ) ) · 0 ) ) = ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) )
96 5 flcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
97 fzval3 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℤ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
98 96 97 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
99 98 eqcomd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) = ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
100 13 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
101 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
102 101 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
103 102 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
104 100 103 rpdivcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
105 70 ffvelcdmi ⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
106 104 105 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
107 106 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
108 107 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
109 108 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
110 6 a1i ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ+ )
111 103 110 rpaddcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ∈ ℝ+ )
112 100 111 rpdivcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ+ )
113 70 ffvelcdmi ⊢ ( ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
114 112 113 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
115 114 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℂ )
116 115 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
117 116 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ∈ ℂ )
118 109 117 negsubdi2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → - ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) )
119 118 eqcomd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) = - ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
120 102 nncnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
121 1cnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
122 120 121 pncand ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
123 122 fveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑆 ‘ 𝑛 ) )
124 122 fveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑇 ‘ 𝑛 ) )
125 rpre ⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ )
126 eleq1 ⊢ ( 𝑎 = 𝑛 → ( 𝑎 ∈ ℝ+ ↔ 𝑛 ∈ ℝ+ ) )
127 id ⊢ ( 𝑎 = 𝑛 → 𝑎 = 𝑛 )
128 fveq2 ⊢ ( 𝑎 = 𝑛 → ( log ‘ 𝑎 ) = ( log ‘ 𝑛 ) )
129 127 128 oveq12d ⊢ ( 𝑎 = 𝑛 → ( 𝑎 · ( log ‘ 𝑎 ) ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
130 126 129 ifbieq1d ⊢ ( 𝑎 = 𝑛 → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) = if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) )
131 ovex ⊢ ( 𝑛 · ( log ‘ 𝑛 ) ) ∈ V
132 c0ex ⊢ 0 ∈ V
133 131 132 ifex ⊢ if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) ∈ V
134 130 3 133 fvmpt ⊢ ( 𝑛 ∈ ℝ → ( 𝑇 ‘ 𝑛 ) = if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) )
135 125 134 syl ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑇 ‘ 𝑛 ) = if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) )
136 iftrue ⊢ ( 𝑛 ∈ ℝ+ → if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
137 135 136 eqtrd ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑇 ‘ 𝑛 ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
138 103 137 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ 𝑛 ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
139 124 138 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
140 139 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) = ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) )
141 123 140 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) = ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) )
142 119 141 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) ) = ( - ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) )
143 108 116 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ∈ ℝ )
144 143 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ∈ ℂ )
145 102 nnred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
146 79 ffvelcdmi ⊢ ( 𝑛 ∈ ℝ → ( 𝑆 ‘ 𝑛 ) ∈ ℝ )
147 145 146 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ 𝑛 ) ∈ ℝ )
148 24 a1i ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℝ )
149 103 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
150 145 149 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( log ‘ 𝑛 ) ) ∈ ℝ )
151 148 150 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
152 147 151 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
153 152 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ )
154 144 153 mulneg1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( - ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) = - ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) )
155 142 154 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) ) = - ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) )
156 99 155 sumeq12rdv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) - ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) )
157 fzfid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
158 143 152 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
159 158 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℂ )
160 157 159 fsumneg ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) - ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) = - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) )
161 156 160 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) ) = - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) )
162 95 161 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 ⊢ ( 𝑚 = 𝑛 → ( 𝑥 / 𝑚 ) = ( 𝑥 / 𝑛 ) )
164 163 fveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) = ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) )
165 164 fveq2d ⊢ ( 𝑚 = 𝑛 → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) )
166 fvoveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑆 ‘ ( 𝑚 − 1 ) ) = ( 𝑆 ‘ ( 𝑛 − 1 ) ) )
167 fvoveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑇 ‘ ( 𝑚 − 1 ) ) = ( 𝑇 ‘ ( 𝑛 − 1 ) ) )
168 167 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) = ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) )
169 166 168 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) )
170 165 169 jca ⊢ ( 𝑚 = 𝑛 → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∧ ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
171 oveq2 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑥 / 𝑚 ) = ( 𝑥 / ( 𝑛 + 1 ) ) )
172 171 fveq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) = ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) )
173 172 fveq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
174 fvoveq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑆 ‘ ( 𝑚 − 1 ) ) = ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) )
175 fvoveq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑇 ‘ ( 𝑚 − 1 ) ) = ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) )
176 175 oveq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) = ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) )
177 174 176 oveq12d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) )
178 173 177 jca ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ∧ ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) ) )
179 oveq2 ⊢ ( 𝑚 = 1 → ( 𝑥 / 𝑚 ) = ( 𝑥 / 1 ) )
180 179 fveq2d ⊢ ( 𝑚 = 1 → ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) = ( 𝑅 ‘ ( 𝑥 / 1 ) ) )
181 180 fveq2d ⊢ ( 𝑚 = 1 → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 1 ) ) ) )
182 oveq1 ⊢ ( 𝑚 = 1 → ( 𝑚 − 1 ) = ( 1 − 1 ) )
183 1m1e0 ⊢ ( 1 − 1 ) = 0
184 182 183 eqtrdi ⊢ ( 𝑚 = 1 → ( 𝑚 − 1 ) = 0 )
185 184 fveq2d ⊢ ( 𝑚 = 1 → ( 𝑆 ‘ ( 𝑚 − 1 ) ) = ( 𝑆 ‘ 0 ) )
186 0re ⊢ 0 ∈ ℝ
187 fveq2 ⊢ ( 𝑎 = 0 → ( ⌊ ‘ 𝑎 ) = ( ⌊ ‘ 0 ) )
188 0z ⊢ 0 ∈ ℤ
189 flid ⊢ ( 0 ∈ ℤ → ( ⌊ ‘ 0 ) = 0 )
190 188 189 ax-mp ⊢ ( ⌊ ‘ 0 ) = 0
191 187 190 eqtrdi ⊢ ( 𝑎 = 0 → ( ⌊ ‘ 𝑎 ) = 0 )
192 191 oveq2d ⊢ ( 𝑎 = 0 → ( 1 ... ( ⌊ ‘ 𝑎 ) ) = ( 1 ... 0 ) )
193 fz10 ⊢ ( 1 ... 0 ) = ∅
194 192 193 eqtrdi ⊢ ( 𝑎 = 0 → ( 1 ... ( ⌊ ‘ 𝑎 ) ) = ∅ )
195 194 sumeq1d ⊢ ( 𝑎 = 0 → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) = Σ 𝑖 ∈ ∅ ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
196 sum0 ⊢ Σ 𝑖 ∈ ∅ ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) = 0
197 195 196 eqtrdi ⊢ ( 𝑎 = 0 → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) = 0 )
198 197 1 132 fvmpt ⊢ ( 0 ∈ ℝ → ( 𝑆 ‘ 0 ) = 0 )
199 186 198 ax-mp ⊢ ( 𝑆 ‘ 0 ) = 0
200 185 199 eqtrdi ⊢ ( 𝑚 = 1 → ( 𝑆 ‘ ( 𝑚 − 1 ) ) = 0 )
201 184 fveq2d ⊢ ( 𝑚 = 1 → ( 𝑇 ‘ ( 𝑚 − 1 ) ) = ( 𝑇 ‘ 0 ) )
202 rpne0 ⊢ ( 𝑎 ∈ ℝ+ → 𝑎 ≠ 0 )
203 202 necon2bi ⊢ ( 𝑎 = 0 → ¬ 𝑎 ∈ ℝ+ )
204 203 iffalsed ⊢ ( 𝑎 = 0 → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) = 0 )
205 204 3 132 fvmpt ⊢ ( 0 ∈ ℝ → ( 𝑇 ‘ 0 ) = 0 )
206 186 205 ax-mp ⊢ ( 𝑇 ‘ 0 ) = 0
207 201 206 eqtrdi ⊢ ( 𝑚 = 1 → ( 𝑇 ‘ ( 𝑚 − 1 ) ) = 0 )
208 207 oveq2d ⊢ ( 𝑚 = 1 → ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) = ( 2 · 0 ) )
209 2t0e0 ⊢ ( 2 · 0 ) = 0
210 208 209 eqtrdi ⊢ ( 𝑚 = 1 → ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) = 0 )
211 200 210 oveq12d ⊢ ( 𝑚 = 1 → ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = ( 0 − 0 ) )
212 0m0e0 ⊢ ( 0 − 0 ) = 0
213 211 212 eqtrdi ⊢ ( 𝑚 = 1 → ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = 0 )
214 181 213 jca ⊢ ( 𝑚 = 1 → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 1 ) ) ) ∧ ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = 0 ) )
215 oveq2 ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑥 / 𝑚 ) = ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
216 215 fveq2d ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) = ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
217 216 fveq2d ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) )
218 fvoveq1 ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑆 ‘ ( 𝑚 − 1 ) ) = ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) )
219 fvoveq1 ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑇 ‘ ( 𝑚 − 1 ) ) = ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) )
220 219 oveq2d ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) = ( 2 · ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) )
221 218 220 oveq12d ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = ( ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) ) )
222 217 221 jca ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) ∧ ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) = ( ( 𝑆 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) ) ) )
223 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
224 18 223 eleqtrdi ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
225 13 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑥 ∈ ℝ+ )
226 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → 𝑚 ∈ ℕ )
227 226 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℕ )
228 227 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℝ+ )
229 225 228 rpdivcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑥 / 𝑚 ) ∈ ℝ+ )
230 70 ffvelcdmi ⊢ ( ( 𝑥 / 𝑚 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ )
231 229 230 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ )
232 231 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ∈ ℂ )
233 232 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) ∈ ℝ )
234 233 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑚 ) ) ) ∈ ℂ )
235 227 nnred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℝ )
236 1red ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 1 ∈ ℝ )
237 235 236 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑚 − 1 ) ∈ ℝ )
238 79 ffvelcdmi ⊢ ( ( 𝑚 − 1 ) ∈ ℝ → ( 𝑆 ‘ ( 𝑚 − 1 ) ) ∈ ℝ )
239 237 238 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑆 ‘ ( 𝑚 − 1 ) ) ∈ ℝ )
240 24 a1i ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 2 ∈ ℝ )
241 87 ffvelcdmi ⊢ ( ( 𝑚 − 1 ) ∈ ℝ → ( 𝑇 ‘ ( 𝑚 − 1 ) ) ∈ ℝ )
242 237 241 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑇 ‘ ( 𝑚 − 1 ) ) ∈ ℝ )
243 240 242 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ∈ ℝ )
244 239 243 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) ∈ ℝ )
245 244 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ( 𝑆 ‘ ( 𝑚 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑚 − 1 ) ) ) ) ∈ ℂ )
246 170 178 214 222 224 234 245 fsumparts ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 ) ) ) ) ) ) )
247 147 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ 𝑛 ) ∈ ℂ )
248 87 ffvelcdmi ⊢ ( 𝑛 ∈ ℝ → ( 𝑇 ‘ 𝑛 ) ∈ ℝ )
249 145 248 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ 𝑛 ) ∈ ℝ )
250 148 249 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝑇 ‘ 𝑛 ) ) ∈ ℝ )
251 250 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝑇 ‘ 𝑛 ) ) ∈ ℂ )
252 1red ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
253 145 252 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℝ )
254 79 ffvelcdmi ⊢ ( ( 𝑛 − 1 ) ∈ ℝ → ( 𝑆 ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
255 253 254 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
256 255 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
257 87 ffvelcdmi ⊢ ( ( 𝑛 − 1 ) ∈ ℝ → ( 𝑇 ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
258 253 257 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
259 148 258 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
260 259 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ∈ ℂ )
261 247 251 256 260 sub4d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑇 ‘ 𝑛 ) ) ) − ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) = ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( ( 2 · ( 𝑇 ‘ 𝑛 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
262 124 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) = ( 2 · ( 𝑇 ‘ 𝑛 ) ) )
263 123 262 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) = ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑇 ‘ 𝑛 ) ) ) )
264 263 oveq1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) = ( ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑇 ‘ 𝑛 ) ) ) − ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
265 2cnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ )
266 249 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ 𝑛 ) ∈ ℂ )
267 258 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
268 265 266 267 subdid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) = ( ( 2 · ( 𝑇 ‘ 𝑛 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) )
269 268 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) = ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( ( 2 · ( 𝑇 ‘ 𝑛 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
270 261 264 269 3eqtr4d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) = ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
271 270 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) )
272 99 271 sumeq12rdv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( 2 · ( 𝑇 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) − ( 2 · ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) )
273 246 272 eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 ) ) ) ) ) ) )
274 157 159 fsumcl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℂ )
275 93 274 subnegd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) − - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) = ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) )
276 162 273 275 3eqtr3rd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) )
277 13 relogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
278 277 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
279 67 278 mulcomd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑥 ) · 𝑥 ) )
280 276 279 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( ( log ‘ 𝑥 ) · 𝑥 ) ) )
281 147 255 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
282 249 258 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
283 148 282 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
284 281 283 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ∈ ℝ )
285 108 284 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ∈ ℝ )
286 157 285 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ∈ ℝ )
287 286 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ∈ ℂ )
288 5 11 rplogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
289 288 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
290 13 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
291 287 278 67 289 290 divdiv1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( ( log ‘ 𝑥 ) · 𝑥 ) ) )
292 280 291 eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) )
293 292 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 ‘ 𝑥 ) ) / 𝑥 ) ) )
294 72 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℂ )
295 294 abscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ℝ )
296 295 277 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
297 108 281 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
298 157 297 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
299 298 288 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
300 296 299 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
301 300 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ℂ )
302 287 278 289 divcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
303 301 302 67 290 divdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 ‘ 𝑥 ) ) / 𝑥 ) ) )
304 296 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
305 299 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
306 304 305 302 subsubd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ )
308 266 267 subcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ∈ ℂ )
309 109 308 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℂ )
310 157 307 309 fsummulc2 ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
311 281 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ∈ ℂ )
312 265 308 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℂ )
313 311 312 nncand ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) = ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) )
314 313 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
315 284 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ∈ ℂ )
316 109 311 315 subdid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) − ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) )
317 109 265 308 mul12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) = ( 2 · ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
318 314 316 317 3eqtr3d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) − ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) = ( 2 · ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
319 318 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) − ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
320 297 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℂ )
321 285 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ∈ ℂ )
322 157 320 321 fsumsub ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) − ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) )
323 310 319 322 3eqtr2rd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) = ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
324 323 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) / ( log ‘ 𝑥 ) ) )
325 298 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℂ )
326 325 287 278 289 divsubdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) )
327 108 282 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
328 157 327 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
329 328 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℂ )
330 307 329 278 289 div23d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) / ( log ‘ 𝑥 ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
331 324 326 330 3eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) )
332 331 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) )
333 306 332 eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) )
334 333 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) − ( 2 · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) )
335 293 303 334 3eqtr2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) + ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) )
336 335 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) + ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) ) )
337 300 13 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℝ )
338 157 158 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
339 92 338 readdcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ∈ ℝ )
340 13 288 rpmulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
341 339 340 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
342 1 2 pntrlog2bndlem1 ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1)
343 342 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )
344 340 rpcnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ )
345 340 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ≠ 0 )
346 93 274 344 345 divdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
347 91 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ∈ ℂ )
348 45 347 344 345 divassd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
349 348 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
350 346 349 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
351 350 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) )
352 91 340 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
353 23 352 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
354 338 340 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
355 ioossre ⊢ ( 1 (,) +∞ ) ⊆ ℝ
356 355 a1i ⊢ ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ )
357 1red ⊢ ( ⊤ → 1 ∈ ℝ )
358 23 8 32 ltled ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ≤ 1 )
359 358 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ≤ 1 )
360 356 23 357 357 359 ello1d ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ∈ ≤𝑂(1) )
361 81 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ℂ )
362 90 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℂ )
363 361 362 344 345 divsubdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
364 363 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) )
365 81 340 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
366 90 340 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
367 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
368 o1const ⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) )
369 355 367 368 sylancr ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) )
370 365 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
371 81 13 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
372 371 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
373 307 278 mulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ )
374 372 373 278 289 divsubdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) / ( log ‘ 𝑥 ) ) − ( ( 2 · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) ) )
375 25 277 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℝ )
376 371 375 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
377 376 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
378 377 278 289 divrecd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) )
379 361 67 278 290 289 divdiv1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
380 307 278 289 divcan4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = 2 )
381 379 380 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) / ( log ‘ 𝑥 ) ) − ( ( 2 · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) ) = ( ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − 2 ) )
382 374 378 381 3eqtr3rd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − 2 ) = ( ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) )
383 382 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − 2 ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) )
384 8 288 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℝ )
385 13 ex ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) )
386 385 ssrdv ⊢ ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ+ )
387 1 selbergs ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
388 387 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
389 386 388 o1res2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
390 divlogrlim ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0
391 rlimo1 ⊢ ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
392 390 391 mp1i ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
393 376 384 389 392 o1mul2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
394 383 393 eqeltrd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − 2 ) ) ∈ 𝑂(1) )
395 370 307 394 o1dif ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) ) )
396 369 395 mpbird ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
397 24 a1i ⊢ ( ⊤ → 2 ∈ ℝ )
398 5 277 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ )
399 2rp ⊢ 2 ∈ ℝ+
400 399 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ+ )
401 400 rpge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 2 )
402 flge1nn ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
403 5 12 402 syl2anc ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
404 403 nnrpd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ+ )
405 rpre ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
406 eleq1 ⊢ ( 𝑎 = ( ⌊ ‘ 𝑥 ) → ( 𝑎 ∈ ℝ+ ↔ ( ⌊ ‘ 𝑥 ) ∈ ℝ+ ) )
407 id ⊢ ( 𝑎 = ( ⌊ ‘ 𝑥 ) → 𝑎 = ( ⌊ ‘ 𝑥 ) )
408 fveq2 ⊢ ( 𝑎 = ( ⌊ ‘ 𝑥 ) → ( log ‘ 𝑎 ) = ( log ‘ ( ⌊ ‘ 𝑥 ) ) )
409 407 408 oveq12d ⊢ ( 𝑎 = ( ⌊ ‘ 𝑥 ) → ( 𝑎 · ( log ‘ 𝑎 ) ) = ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) )
410 406 409 ifbieq1d ⊢ ( 𝑎 = ( ⌊ ‘ 𝑥 ) → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) = if ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ , ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) , 0 ) )
411 ovex ⊢ ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ V
412 411 132 ifex ⊢ if ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ , ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) , 0 ) ∈ V
413 410 3 412 fvmpt ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ → ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) = if ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ , ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) , 0 ) )
414 405 413 syl ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ → ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) = if ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ , ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) , 0 ) )
415 iftrue ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ → if ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ , ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) , 0 ) = ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) )
416 414 415 eqtrd ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ+ → ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) = ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) )
417 404 416 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) = ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) )
418 404 relogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℝ )
419 16 nn0ge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( ⌊ ‘ 𝑥 ) )
420 403 nnge1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ ( ⌊ ‘ 𝑥 ) )
421 48 420 logge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( log ‘ ( ⌊ ‘ 𝑥 ) ) )
422 flle ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
423 5 422 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
424 404 13 logled ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) ≤ 𝑥 ↔ ( log ‘ ( ⌊ ‘ 𝑥 ) ) ≤ ( log ‘ 𝑥 ) ) )
425 423 424 mpbid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ ( ⌊ ‘ 𝑥 ) ) ≤ ( log ‘ 𝑥 ) )
426 48 5 418 277 419 421 423 425 lemul12ad ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) ≤ ( 𝑥 · ( log ‘ 𝑥 ) ) )
427 417 426 eqbrtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ≤ ( 𝑥 · ( log ‘ 𝑥 ) ) )
428 89 398 25 401 427 lemul2ad ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ≤ ( 2 · ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
429 90 25 340 ledivmul2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ 2 ↔ ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ≤ ( 2 · ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
430 428 429 mpbird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ 2 )
431 430 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ 2 )
432 356 366 357 397 431 ello1d ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ≤𝑂(1) )
433 0red ⊢ ( ⊤ → 0 ∈ ℝ )
434 48 418 419 421 mulge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( ( ⌊ ‘ 𝑥 ) · ( log ‘ ( ⌊ ‘ 𝑥 ) ) ) )
435 434 417 breqtrrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) )
436 25 89 401 435 mulge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) )
437 90 340 436 divge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
438 366 433 437 o1lo12 ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ≤𝑂(1) ) )
439 432 438 mpbird ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
440 365 366 396 439 o1sub2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑆 ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
441 364 440 eqeltrd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
442 352 441 o1lo1d ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ≤𝑂(1) )
443 23 352 360 442 43 lo1mul ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) ∈ ≤𝑂(1) )
444 1 selbergsb ⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐
445 simpl ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → 𝑐 ∈ ℝ+ )
446 simpr ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 )
447 1 2 445 446 pntrlog2bndlem3 ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
448 447 rexlimiva ⊢ ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
449 444 448 mp1i ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
450 354 449 o1lo1d ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ≤𝑂(1) )
451 353 354 443 450 lo1add ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) ∈ ≤𝑂(1) )
452 351 451 eqeltrd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ≤𝑂(1) )
453 337 341 343 452 lo1add ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) + ( ( ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( 𝑆 ‘ 𝑥 ) − ( 2 · ( 𝑇 ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) ∈ ≤𝑂(1) )
454 336 453 eqeltrrd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )
455 454 mptru ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1)