Metamath Proof Explorer

Theorem pntrlog2bndlem5

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 ) )
pntrlog2bndlem5.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
pntrlog2bndlem5.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 )
Assertion pntrlog2bndlem5 ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 pntsval.1 ⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2 pntrlog2bnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
3 pntrlog2bnd.t ⊢ 𝑇 = ( 𝑎 ∈ ℝ ↦ if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) )
4 pntrlog2bndlem5.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
5 pntrlog2bndlem5.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 )
6 elioore ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
8 1rp ⊢ 1 ∈ ℝ+
9 8 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
10 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
11 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
13 12 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
14 10 7 13 ltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
15 7 9 14 rpgecld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
16 2 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
17 16 ffvelcdmi ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
18 15 17 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
19 18 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℂ )
20 19 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ℝ )
21 20 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ℂ )
22 15 relogcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
23 22 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
24 21 23 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
25 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ )
26 7 13 rplogcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
27 26 rpne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
28 25 23 27 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℂ )
29 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
30 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
31 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
32 31 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
33 32 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
34 30 33 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
35 16 ffvelcdmi ⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
36 34 35 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
37 36 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
38 37 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
39 33 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
40 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
41 39 40 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ 𝑛 ) + 1 ) ∈ ℝ )
42 38 41 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ∈ ℝ )
43 42 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ∈ ℂ )
44 29 43 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ∈ ℂ )
45 28 44 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ∈ ℂ )
46 24 45 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) ∈ ℂ )
47 38 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
48 29 47 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
49 28 48 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
50 7 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
51 15 rpne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
52 46 49 50 51 divdird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑥 ) = ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) / 𝑥 ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) )
53 20 22 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
54 53 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
55 54 45 49 subsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
56 28 44 48 subdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
57 29 43 47 fsumsub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) )
58 41 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ 𝑛 ) + 1 ) ∈ ℂ )
59 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
60 47 58 59 subdid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( log ‘ 𝑛 ) + 1 ) − 1 ) ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · 1 ) ) )
61 39 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
62 61 59 pncand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ 𝑛 ) + 1 ) − 1 ) = ( log ‘ 𝑛 ) )
63 62 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( ( log ‘ 𝑛 ) + 1 ) − 1 ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
64 47 mulridd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · 1 ) = ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) )
65 64 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · 1 ) ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) )
66 60 63 65 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
67 66 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
68 57 67 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
69 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
70 56 69 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
71 70 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
72 55 71 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
73 72 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑥 ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) )
74 52 73 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) / 𝑥 ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) )
75 74 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) / 𝑥 ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) )
76 2re ⊢ 2 ∈ ℝ
77 76 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ )
78 77 26 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ )
79 29 42 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ∈ ℝ )
80 78 79 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ∈ ℝ )
81 53 80 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) ∈ ℝ )
82 81 15 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) / 𝑥 ) ∈ ℝ )
83 29 38 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
84 78 83 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
85 84 15 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ )
86 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
87 1 2 3 pntrlog2bndlem4 ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1)
88 87 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )
89 32 nnred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
90 simpl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+ ) → 𝑎 ∈ ℝ )
91 simpr ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+ ) → 𝑎 ∈ ℝ+ )
92 91 relogcld ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+ ) → ( log ‘ 𝑎 ) ∈ ℝ )
93 90 92 remulcld ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+ ) → ( 𝑎 · ( log ‘ 𝑎 ) ) ∈ ℝ )
94 0red ⊢ ( ( 𝑎 ∈ ℝ ∧ ¬ 𝑎 ∈ ℝ+ ) → 0 ∈ ℝ )
95 93 94 ifclda ⊢ ( 𝑎 ∈ ℝ → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) ∈ ℝ )
96 3 95 fmpti ⊢ 𝑇 : ℝ ⟶ ℝ
97 96 ffvelcdmi ⊢ ( 𝑛 ∈ ℝ → ( 𝑇 ‘ 𝑛 ) ∈ ℝ )
98 89 97 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ 𝑛 ) ∈ ℝ )
99 89 40 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℝ )
100 96 ffvelcdmi ⊢ ( ( 𝑛 − 1 ) ∈ ℝ → ( 𝑇 ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
101 99 100 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
102 98 101 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
103 38 102 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
104 29 103 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
105 78 104 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ∈ ℝ )
106 53 105 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) ∈ ℝ )
107 106 15 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) ∈ ℝ )
108 2rp ⊢ 2 ∈ ℝ+
109 108 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ+ )
110 109 rpge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 2 )
111 77 26 110 divge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 2 / ( log ‘ 𝑥 ) ) )
112 37 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) )
113 33 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → 𝑛 ∈ ℝ+ )
114 113 rpcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → 𝑛 ∈ ℂ )
115 61 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( log ‘ 𝑛 ) ∈ ℂ )
116 114 115 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑛 · ( log ‘ 𝑛 ) ) ∈ ℂ )
117 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → 1 < 𝑛 )
118 1re ⊢ 1 ∈ ℝ
119 113 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → 𝑛 ∈ ℝ )
120 difrp ⊢ ( ( 1 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 1 < 𝑛 ↔ ( 𝑛 − 1 ) ∈ ℝ+ ) )
121 118 119 120 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 1 < 𝑛 ↔ ( 𝑛 − 1 ) ∈ ℝ+ ) )
122 117 121 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑛 − 1 ) ∈ ℝ+ )
123 122 relogcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( log ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
124 123 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( log ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
125 114 124 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) ∈ ℂ )
126 116 125 124 subsubd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 · ( log ‘ 𝑛 ) ) − ( ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) = ( ( ( 𝑛 · ( log ‘ 𝑛 ) ) − ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) )
127 rpre ⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ )
128 eleq1 ⊢ ( 𝑎 = 𝑛 → ( 𝑎 ∈ ℝ+ ↔ 𝑛 ∈ ℝ+ ) )
129 id ⊢ ( 𝑎 = 𝑛 → 𝑎 = 𝑛 )
130 fveq2 ⊢ ( 𝑎 = 𝑛 → ( log ‘ 𝑎 ) = ( log ‘ 𝑛 ) )
131 129 130 oveq12d ⊢ ( 𝑎 = 𝑛 → ( 𝑎 · ( log ‘ 𝑎 ) ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
132 128 131 ifbieq1d ⊢ ( 𝑎 = 𝑛 → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) = if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) )
133 ovex ⊢ ( 𝑛 · ( log ‘ 𝑛 ) ) ∈ V
134 c0ex ⊢ 0 ∈ V
135 133 134 ifex ⊢ if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) ∈ V
136 132 3 135 fvmpt ⊢ ( 𝑛 ∈ ℝ → ( 𝑇 ‘ 𝑛 ) = if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) )
137 127 136 syl ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑇 ‘ 𝑛 ) = if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) )
138 iftrue ⊢ ( 𝑛 ∈ ℝ+ → if ( 𝑛 ∈ ℝ+ , ( 𝑛 · ( log ‘ 𝑛 ) ) , 0 ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
139 137 138 eqtrd ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑇 ‘ 𝑛 ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
140 113 139 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑇 ‘ 𝑛 ) = ( 𝑛 · ( log ‘ 𝑛 ) ) )
141 rpre ⊢ ( ( 𝑛 − 1 ) ∈ ℝ+ → ( 𝑛 − 1 ) ∈ ℝ )
142 eleq1 ⊢ ( 𝑎 = ( 𝑛 − 1 ) → ( 𝑎 ∈ ℝ+ ↔ ( 𝑛 − 1 ) ∈ ℝ+ ) )
143 id ⊢ ( 𝑎 = ( 𝑛 − 1 ) → 𝑎 = ( 𝑛 − 1 ) )
144 fveq2 ⊢ ( 𝑎 = ( 𝑛 − 1 ) → ( log ‘ 𝑎 ) = ( log ‘ ( 𝑛 − 1 ) ) )
145 143 144 oveq12d ⊢ ( 𝑎 = ( 𝑛 − 1 ) → ( 𝑎 · ( log ‘ 𝑎 ) ) = ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) )
146 142 145 ifbieq1d ⊢ ( 𝑎 = ( 𝑛 − 1 ) → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) = if ( ( 𝑛 − 1 ) ∈ ℝ+ , ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) , 0 ) )
147 ovex ⊢ ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) ∈ V
148 147 134 ifex ⊢ if ( ( 𝑛 − 1 ) ∈ ℝ+ , ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) , 0 ) ∈ V
149 146 3 148 fvmpt ⊢ ( ( 𝑛 − 1 ) ∈ ℝ → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = if ( ( 𝑛 − 1 ) ∈ ℝ+ , ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) , 0 ) )
150 141 149 syl ⊢ ( ( 𝑛 − 1 ) ∈ ℝ+ → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = if ( ( 𝑛 − 1 ) ∈ ℝ+ , ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) , 0 ) )
151 iftrue ⊢ ( ( 𝑛 − 1 ) ∈ ℝ+ → if ( ( 𝑛 − 1 ) ∈ ℝ+ , ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) , 0 ) = ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) )
152 150 151 eqtrd ⊢ ( ( 𝑛 − 1 ) ∈ ℝ+ → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) )
153 122 152 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) )
154 1cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → 1 ∈ ℂ )
155 114 154 124 subdird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 − 1 ) · ( log ‘ ( 𝑛 − 1 ) ) ) = ( ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) − ( 1 · ( log ‘ ( 𝑛 − 1 ) ) ) ) )
156 124 mullidd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 1 · ( log ‘ ( 𝑛 − 1 ) ) ) = ( log ‘ ( 𝑛 − 1 ) ) )
157 156 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) − ( 1 · ( log ‘ ( 𝑛 − 1 ) ) ) ) = ( ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) − ( log ‘ ( 𝑛 − 1 ) ) ) )
158 153 155 157 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = ( ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) − ( log ‘ ( 𝑛 − 1 ) ) ) )
159 140 158 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) = ( ( 𝑛 · ( log ‘ 𝑛 ) ) − ( ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) )
160 114 115 124 subdid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) = ( ( 𝑛 · ( log ‘ 𝑛 ) ) − ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) ) )
161 160 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) = ( ( ( 𝑛 · ( log ‘ 𝑛 ) ) − ( 𝑛 · ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) )
162 126 159 161 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) = ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) )
163 113 relogcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( log ‘ 𝑛 ) ∈ ℝ )
164 163 123 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
165 164 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ∈ ℂ )
166 114 154 165 subdird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 − 1 ) · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) = ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) − ( 1 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) ) )
167 165 mullidd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 1 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) = ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) )
168 167 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) − ( 1 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) ) = ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) − ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) )
169 119 164 remulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
170 169 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℂ )
171 170 115 124 subsub3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) − ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) = ( ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) − ( log ‘ 𝑛 ) ) )
172 166 168 171 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 − 1 ) · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) = ( ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) − ( log ‘ 𝑛 ) ) )
173 114 154 npcand ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
174 173 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( log ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( log ‘ 𝑛 ) )
175 174 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( log ‘ ( ( 𝑛 − 1 ) + 1 ) ) − ( log ‘ ( 𝑛 − 1 ) ) ) = ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) )
176 logdifbnd ⊢ ( ( 𝑛 − 1 ) ∈ ℝ+ → ( ( log ‘ ( ( 𝑛 − 1 ) + 1 ) ) − ( log ‘ ( 𝑛 − 1 ) ) ) ≤ ( 1 / ( 𝑛 − 1 ) ) )
177 122 176 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( log ‘ ( ( 𝑛 − 1 ) + 1 ) ) − ( log ‘ ( 𝑛 − 1 ) ) ) ≤ ( 1 / ( 𝑛 − 1 ) ) )
178 175 177 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ≤ ( 1 / ( 𝑛 − 1 ) ) )
179 1red ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → 1 ∈ ℝ )
180 164 179 122 lemuldiv2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( ( 𝑛 − 1 ) · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) ≤ 1 ↔ ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ≤ ( 1 / ( 𝑛 − 1 ) ) ) )
181 178 180 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 − 1 ) · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) ≤ 1 )
182 172 181 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) − ( log ‘ 𝑛 ) ) ≤ 1 )
183 169 123 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
184 183 163 179 lesubadd2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) − ( log ‘ 𝑛 ) ) ≤ 1 ↔ ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) ≤ ( ( log ‘ 𝑛 ) + 1 ) ) )
185 182 184 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑛 · ( ( log ‘ 𝑛 ) − ( log ‘ ( 𝑛 − 1 ) ) ) ) + ( log ‘ ( 𝑛 − 1 ) ) ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
186 162 185 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 < 𝑛 ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
187 fveq2 ⊢ ( 𝑛 = 1 → ( 𝑇 ‘ 𝑛 ) = ( 𝑇 ‘ 1 ) )
188 id ⊢ ( 𝑎 = 1 → 𝑎 = 1 )
189 188 8 eqeltrdi ⊢ ( 𝑎 = 1 → 𝑎 ∈ ℝ+ )
190 189 iftrued ⊢ ( 𝑎 = 1 → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) = ( 𝑎 · ( log ‘ 𝑎 ) ) )
191 fveq2 ⊢ ( 𝑎 = 1 → ( log ‘ 𝑎 ) = ( log ‘ 1 ) )
192 log1 ⊢ ( log ‘ 1 ) = 0
193 191 192 eqtrdi ⊢ ( 𝑎 = 1 → ( log ‘ 𝑎 ) = 0 )
194 188 193 oveq12d ⊢ ( 𝑎 = 1 → ( 𝑎 · ( log ‘ 𝑎 ) ) = ( 1 · 0 ) )
195 ax-1cn ⊢ 1 ∈ ℂ
196 195 mul01i ⊢ ( 1 · 0 ) = 0
197 194 196 eqtrdi ⊢ ( 𝑎 = 1 → ( 𝑎 · ( log ‘ 𝑎 ) ) = 0 )
198 190 197 eqtrd ⊢ ( 𝑎 = 1 → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) = 0 )
199 198 3 134 fvmpt ⊢ ( 1 ∈ ℝ → ( 𝑇 ‘ 1 ) = 0 )
200 118 199 ax-mp ⊢ ( 𝑇 ‘ 1 ) = 0
201 187 200 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝑇 ‘ 𝑛 ) = 0 )
202 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 − 1 ) = ( 1 − 1 ) )
203 1m1e0 ⊢ ( 1 − 1 ) = 0
204 202 203 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝑛 − 1 ) = 0 )
205 204 fveq2d ⊢ ( 𝑛 = 1 → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = ( 𝑇 ‘ 0 ) )
206 0re ⊢ 0 ∈ ℝ
207 rpne0 ⊢ ( 𝑎 ∈ ℝ+ → 𝑎 ≠ 0 )
208 207 necon2bi ⊢ ( 𝑎 = 0 → ¬ 𝑎 ∈ ℝ+ )
209 208 iffalsed ⊢ ( 𝑎 = 0 → if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) = 0 )
210 209 3 134 fvmpt ⊢ ( 0 ∈ ℝ → ( 𝑇 ‘ 0 ) = 0 )
211 206 210 ax-mp ⊢ ( 𝑇 ‘ 0 ) = 0
212 205 211 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = 0 )
213 201 212 oveq12d ⊢ ( 𝑛 = 1 → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) = ( 0 − 0 ) )
214 0m0e0 ⊢ ( 0 − 0 ) = 0
215 213 214 eqtrdi ⊢ ( 𝑛 = 1 → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) = 0 )
216 215 eqcoms ⊢ ( 1 = 𝑛 → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) = 0 )
217 216 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 = 𝑛 ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) = 0 )
218 0red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ∈ ℝ )
219 32 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ 𝑛 )
220 89 219 logge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( log ‘ 𝑛 ) )
221 39 lep1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
222 218 39 41 220 221 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( log ‘ 𝑛 ) + 1 ) )
223 222 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 = 𝑛 ) → 0 ≤ ( ( log ‘ 𝑛 ) + 1 ) )
224 217 223 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 1 = 𝑛 ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
225 elfzle1 ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 1 ≤ 𝑛 )
226 225 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ 𝑛 )
227 40 89 leloed ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ≤ 𝑛 ↔ ( 1 < 𝑛 ∨ 1 = 𝑛 ) ) )
228 226 227 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 < 𝑛 ∨ 1 = 𝑛 ) )
229 186 224 228 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
230 102 41 38 112 229 lemul2ad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ≤ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) )
231 29 103 42 230 fsumle ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) )
232 104 79 78 111 231 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ≤ ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) )
233 105 80 53 232 lesub2dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) ≤ ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) )
234 81 106 15 233 lediv1dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) / 𝑥 ) ≤ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) )
235 234 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) / 𝑥 ) ≤ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑇 ‘ 𝑛 ) − ( 𝑇 ‘ ( 𝑛 − 1 ) ) ) ) ) ) / 𝑥 ) )
236 86 88 107 82 235 lo1le ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )
237 108 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
238 237 4 rpmulcld ⊢ ( 𝜑 → ( 2 · 𝐵 ) ∈ ℝ+ )
239 238 rpred ⊢ ( 𝜑 → ( 2 · 𝐵 ) ∈ ℝ )
240 239 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · 𝐵 ) ∈ ℝ )
241 10 26 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℝ )
242 10 241 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
243 ioossre ⊢ ( 1 (,) +∞ ) ⊆ ℝ
244 lo1const ⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ ( 2 · 𝐵 ) ∈ ℝ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 2 · 𝐵 ) ) ∈ ≤𝑂(1) )
245 243 239 244 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 2 · 𝐵 ) ) ∈ ≤𝑂(1) )
246 lo1const ⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 1 ∈ ℝ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ ≤𝑂(1) )
247 243 86 246 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ ≤𝑂(1) )
248 divlogrlim ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0
249 rlimo1 ⊢ ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
250 248 249 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
251 241 250 o1lo1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ ≤𝑂(1) )
252 10 241 247 251 lo1add ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ ≤𝑂(1) )
253 238 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · 𝐵 ) ∈ ℝ+ )
254 253 rpge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 2 · 𝐵 ) )
255 240 242 245 252 254 lo1mul ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 2 · 𝐵 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ) ∈ ≤𝑂(1) )
256 240 242 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · 𝐵 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
257 83 15 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ∈ ℝ )
258 22 10 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℝ )
259 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐵 ∈ ℝ+ )
260 259 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐵 ∈ ℝ )
261 258 260 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) + 1 ) · 𝐵 ) ∈ ℝ )
262 32 nnrecred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
263 29 262 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ∈ ℝ )
264 263 260 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) · 𝐵 ) ∈ ℝ )
265 38 30 rerpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ∈ ℝ )
266 260 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐵 ∈ ℝ )
267 262 266 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 / 𝑛 ) · 𝐵 ) ∈ ℝ )
268 34 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℂ )
269 34 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ≠ 0 )
270 37 268 269 absdivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( abs ‘ ( 𝑥 / 𝑛 ) ) ) )
271 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
272 271 32 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
273 34 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( 𝑥 / 𝑛 ) )
274 272 273 absidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑥 / 𝑛 ) ) = ( 𝑥 / 𝑛 ) )
275 274 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( abs ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( 𝑥 / 𝑛 ) ) )
276 270 275 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( 𝑥 / 𝑛 ) ) )
277 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
278 89 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
279 51 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ≠ 0 )
280 32 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
281 47 277 278 279 280 divdiv2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( 𝑥 / 𝑛 ) ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · 𝑛 ) / 𝑥 ) )
282 47 278 277 279 div23d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · 𝑛 ) / 𝑥 ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) · 𝑛 ) )
283 276 281 282 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) · 𝑛 ) )
284 fveq2 ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( 𝑅 ‘ 𝑦 ) = ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) )
285 id ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → 𝑦 = ( 𝑥 / 𝑛 ) )
286 284 285 oveq12d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) = ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) )
287 286 fveq2d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) = ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) )
288 287 breq1d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 ↔ ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) ≤ 𝐵 ) )
289 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 )
290 288 289 34 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) ≤ 𝐵 )
291 283 290 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) · 𝑛 ) ≤ 𝐵 )
292 265 266 33 lemuldivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) · 𝑛 ) ≤ 𝐵 ↔ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ≤ ( 𝐵 / 𝑛 ) ) )
293 291 292 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ≤ ( 𝐵 / 𝑛 ) )
294 266 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐵 ∈ ℂ )
295 294 278 280 divrec2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐵 / 𝑛 ) = ( ( 1 / 𝑛 ) · 𝐵 ) )
296 293 295 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ≤ ( ( 1 / 𝑛 ) · 𝐵 ) )
297 29 265 267 296 fsumle ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 / 𝑛 ) · 𝐵 ) )
298 29 50 47 51 fsumdivc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) )
299 259 rpcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐵 ∈ ℂ )
300 262 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
301 29 299 300 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) · 𝐵 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 / 𝑛 ) · 𝐵 ) )
302 297 298 301 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) · 𝐵 ) )
303 259 rpge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 𝐵 )
304 harmonicubnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
305 7 14 304 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
306 263 258 260 303 305 lemul1ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) · 𝐵 ) ≤ ( ( ( log ‘ 𝑥 ) + 1 ) · 𝐵 ) )
307 257 264 261 302 306 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ≤ ( ( ( log ‘ 𝑥 ) + 1 ) · 𝐵 ) )
308 257 261 78 111 307 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ) ≤ ( ( 2 / ( log ‘ 𝑥 ) ) · ( ( ( log ‘ 𝑥 ) + 1 ) · 𝐵 ) ) )
309 28 48 50 51 divassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) = ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / 𝑥 ) ) )
310 242 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ∈ ℂ )
311 25 299 310 mul32d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · 𝐵 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) = ( ( 2 · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) · 𝐵 ) )
312 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℂ )
313 23 312 23 27 divdird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) + 1 ) / ( log ‘ 𝑥 ) ) = ( ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) + ( 1 / ( log ‘ 𝑥 ) ) ) )
314 23 27 dividd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) = 1 )
315 314 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) + ( 1 / ( log ‘ 𝑥 ) ) ) = ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) )
316 313 315 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) = ( ( ( log ‘ 𝑥 ) + 1 ) / ( log ‘ 𝑥 ) ) )
317 316 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) = ( 2 · ( ( ( log ‘ 𝑥 ) + 1 ) / ( log ‘ 𝑥 ) ) ) )
318 23 312 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℂ )
319 25 23 318 27 div32d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) + 1 ) ) = ( 2 · ( ( ( log ‘ 𝑥 ) + 1 ) / ( log ‘ 𝑥 ) ) ) )
320 317 319 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) + 1 ) ) )
321 320 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) · 𝐵 ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) + 1 ) ) · 𝐵 ) )
322 28 318 299 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) + 1 ) ) · 𝐵 ) = ( ( 2 / ( log ‘ 𝑥 ) ) · ( ( ( log ‘ 𝑥 ) + 1 ) · 𝐵 ) ) )
323 311 321 322 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · 𝐵 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · ( ( ( log ‘ 𝑥 ) + 1 ) · 𝐵 ) ) )
324 308 309 323 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ≤ ( ( 2 · 𝐵 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) )
325 324 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ≤ ( ( 2 · 𝐵 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) )
326 86 255 256 85 325 lo1le ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )
327 82 85 236 326 lo1add ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( log ‘ 𝑛 ) + 1 ) ) ) ) / 𝑥 ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ) ∈ ≤𝑂(1) )
328 75 327 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )