Metamath Proof Explorer

Theorem pntrlog2bndlem1

Description: The sum of selberg3r and selberg4r . (Contributed by Mario Carneiro, 31-May-2016)

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

Proof

Step Hyp Ref Expression
1 pntsval.1 ⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2 pntrlog2bnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
3 1red ⊢ ( ⊤ → 1 ∈ ℝ )
4 2 selberg34r ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ 𝑂(1)
5 elioore ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
6 5 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
7 1rp ⊢ 1 ∈ ℝ+
8 7 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
9 1red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
10 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
11 10 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
12 11 simpld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
13 9 6 12 ltled ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
14 6 8 13 rpgecld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
15 2 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
16 15 ffvelrni ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
17 14 16 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
18 14 relogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
19 17 18 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
20 fzfid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
21 14 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
22 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
23 22 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
24 23 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
25 21 24 rpdivcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
26 15 ffvelrni ⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
27 25 26 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
28 fzfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... 𝑛 ) ∈ Fin )
29 dvdsssfz1 ⊢ ( 𝑛 ∈ ℕ → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
30 23 29 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
31 28 30 ssfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ∈ Fin )
32 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ℕ
33 simpr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
34 32 33 sseldi ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 𝑚 ∈ ℕ )
35 vmacl ⊢ ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ )
36 34 35 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
37 dvdsdivcl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
38 23 37 sylan ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
39 32 38 sseldi ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ ℕ )
40 vmacl ⊢ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( Λ ‘ ( 𝑛 / 𝑚 ) ) ∈ ℝ )
41 39 40 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( Λ ‘ ( 𝑛 / 𝑚 ) ) ∈ ℝ )
42 36 41 remulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℝ )
43 31 42 fsumrecl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℝ )
44 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
45 23 44 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
46 24 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
47 45 46 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
48 43 47 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
49 27 48 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
50 20 49 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
51 6 12 rplogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
52 50 51 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
53 19 52 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
54 53 14 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℝ )
55 54 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℂ )
56 55 lo1o12 ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( abs ‘ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∈ ≤𝑂(1) ) )
57 4 56 mpbii ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( abs ‘ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∈ ≤𝑂(1) )
58 55 abscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ ℝ )
59 17 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℂ )
60 59 abscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ℝ )
61 60 18 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
62 27 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
63 62 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
64 23 nnred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
65 1 pntsf ⊢ 𝑆 : ℝ ⟶ ℝ
66 65 ffvelrni ⊢ ( 𝑛 ∈ ℝ → ( 𝑆 ‘ 𝑛 ) ∈ ℝ )
67 64 66 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ 𝑛 ) ∈ ℝ )
68 1red ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
69 64 68 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℝ )
70 65 ffvelrni ⊢ ( ( 𝑛 − 1 ) ∈ ℝ → ( 𝑆 ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
71 69 70 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
72 67 71 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ∈ ℝ )
73 63 72 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
74 20 73 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) ∈ ℝ )
75 74 51 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
76 61 75 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
77 76 14 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℝ )
78 18 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
79 59 78 mulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
80 50 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ )
81 51 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
82 80 78 81 divcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
83 79 82 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ℂ )
84 83 abscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
85 80 abscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
86 85 51 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
87 61 86 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
88 49 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ )
89 88 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
90 20 89 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
91 20 88 fsumabs ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) )
92 48 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
93 62 92 absmuld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( abs ‘ ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) )
94 92 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
95 62 absge0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) )
96 43 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℂ )
97 47 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
98 96 97 abs2dif2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ≤ ( ( abs ‘ Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) + ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) )
99 71 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
100 96 97 addcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
101 99 100 pncan2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) + ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) = ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
102 elfzuz ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
103 102 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
104 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → 𝑘 ∈ ℕ )
105 104 adantl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
106 vmacl ⊢ ( 𝑘 ∈ ℕ → ( Λ ‘ 𝑘 ) ∈ ℝ )
107 105 106 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( Λ ‘ 𝑘 ) ∈ ℝ )
108 105 nnrpd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℝ+ )
109 108 relogcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ 𝑘 ) ∈ ℝ )
110 107 109 remulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ∈ ℝ )
111 fzfid ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 1 ... 𝑘 ) ∈ Fin )
112 dvdsssfz1 ⊢ ( 𝑘 ∈ ℕ → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ( 1 ... 𝑘 ) )
113 105 112 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ( 1 ... 𝑘 ) )
114 111 113 ssfid ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ∈ Fin )
115 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ℕ
116 simpr ⊢ ( ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } )
117 115 116 sseldi ⊢ ( ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → 𝑚 ∈ ℕ )
118 117 35 syl ⊢ ( ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
119 dvdsdivcl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( 𝑘 / 𝑚 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } )
120 105 119 sylan ⊢ ( ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( 𝑘 / 𝑚 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } )
121 115 120 sseldi ⊢ ( ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( 𝑘 / 𝑚 ) ∈ ℕ )
122 vmacl ⊢ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( Λ ‘ ( 𝑘 / 𝑚 ) ) ∈ ℝ )
123 121 122 syl ⊢ ( ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( Λ ‘ ( 𝑘 / 𝑚 ) ) ∈ ℝ )
124 118 123 remulcld ⊢ ( ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ∈ ℝ )
125 114 124 fsumrecl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ∈ ℝ )
126 110 125 readdcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) ∈ ℝ )
127 126 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) ∈ ℂ )
128 fveq2 ⊢ ( 𝑘 = 𝑛 → ( Λ ‘ 𝑘 ) = ( Λ ‘ 𝑛 ) )
129 fveq2 ⊢ ( 𝑘 = 𝑛 → ( log ‘ 𝑘 ) = ( log ‘ 𝑛 ) )
130 128 129 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) )
131 breq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑦 ∥ 𝑘 ↔ 𝑦 ∥ 𝑛 ) )
132 131 rabbidv ⊢ ( 𝑘 = 𝑛 → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } = { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
133 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( Λ ‘ ( 𝑘 / 𝑚 ) ) = ( Λ ‘ ( 𝑛 / 𝑚 ) ) )
134 133 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) )
135 134 adantr ⊢ ( ( 𝑘 = 𝑛 ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) )
136 132 135 sumeq12rdv ⊢ ( 𝑘 = 𝑛 → Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) = Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) )
137 130 136 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
138 103 127 137 fsumm1 ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) + ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) ) )
139 1 pntsval2 ⊢ ( 𝑛 ∈ ℝ → ( 𝑆 ‘ 𝑛 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑛 ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) )
140 64 139 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ 𝑛 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑛 ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) )
141 23 nnzd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℤ )
142 flid ⊢ ( 𝑛 ∈ ℤ → ( ⌊ ‘ 𝑛 ) = 𝑛 )
143 141 142 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ 𝑛 ) = 𝑛 )
144 143 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ 𝑛 ) ) = ( 1 ... 𝑛 ) )
145 144 sumeq1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑛 ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) )
146 140 145 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ 𝑛 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) )
147 1 pntsval2 ⊢ ( ( 𝑛 − 1 ) ∈ ℝ → ( 𝑆 ‘ ( 𝑛 − 1 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑛 − 1 ) ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) )
148 69 147 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( 𝑛 − 1 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑛 − 1 ) ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) )
149 1zzd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℤ )
150 141 149 zsubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℤ )
151 flid ⊢ ( ( 𝑛 − 1 ) ∈ ℤ → ( ⌊ ‘ ( 𝑛 − 1 ) ) = ( 𝑛 − 1 ) )
152 150 151 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑛 − 1 ) ) = ( 𝑛 − 1 ) )
153 152 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑛 − 1 ) ) ) = ( 1 ... ( 𝑛 − 1 ) ) )
154 153 sumeq1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑛 − 1 ) ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) )
155 148 154 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( 𝑛 − 1 ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) )
156 96 97 addcomd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
157 155 156 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) + ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑘 / 𝑚 ) ) ) ) + ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) ) )
158 138 146 157 3eqtr4d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ 𝑛 ) = ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) + ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) )
159 158 oveq1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) = ( ( ( 𝑆 ‘ ( 𝑛 − 1 ) ) + ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) )
160 vmage0 ⊢ ( 𝑚 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑚 ) )
161 34 160 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 0 ≤ ( Λ ‘ 𝑚 ) )
162 vmage0 ⊢ ( ( 𝑛 / 𝑚 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 / 𝑚 ) ) )
163 39 162 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 0 ≤ ( Λ ‘ ( 𝑛 / 𝑚 ) ) )
164 36 41 161 163 mulge0d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 0 ≤ ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) )
165 31 42 164 fsumge0 ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) )
166 43 165 absidd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) = Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) )
167 vmage0 ⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
168 23 167 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
169 23 nnge1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ 𝑛 )
170 64 169 logge0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( log ‘ 𝑛 ) )
171 45 46 168 170 mulge0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) )
172 47 171 absidd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) )
173 166 172 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) + ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) = ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
174 101 159 173 3eqtr4d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) = ( ( abs ‘ Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) + ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) )
175 98 174 breqtrrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) )
176 94 72 63 95 175 lemul2ad ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( abs ‘ ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ≤ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) )
177 93 176 eqbrtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ≤ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) )
178 20 89 73 177 fsumle ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) )
179 85 90 74 91 178 letrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) )
180 85 74 51 179 lediv1dd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) )
181 86 75 61 180 lesub2dd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ≤ ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) )
182 59 78 absmuld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( abs ‘ ( log ‘ 𝑥 ) ) ) )
183 6 13 logge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( log ‘ 𝑥 ) )
184 18 183 absidd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( log ‘ 𝑥 ) ) = ( log ‘ 𝑥 ) )
185 184 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( abs ‘ ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) )
186 182 185 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) )
187 80 78 81 absdivd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( abs ‘ ( log ‘ 𝑥 ) ) ) )
188 184 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( abs ‘ ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) )
189 187 188 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) )
190 186 189 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) )
191 79 82 abs2difd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) )
192 190 191 eqbrtrrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) )
193 76 87 84 181 192 letrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) )
194 76 84 14 193 lediv1dd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ≤ ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) )
195 53 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ℂ )
196 6 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
197 14 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
198 195 196 197 absdivd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) = ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) / ( abs ‘ 𝑥 ) ) )
199 14 rpge0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 𝑥 )
200 6 199 absidd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ 𝑥 ) = 𝑥 )
201 200 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) / ( abs ‘ 𝑥 ) ) = ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) )
202 198 201 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) = ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) )
203 194 202 breqtrrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ≤ ( abs ‘ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) )
204 203 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ≤ ( abs ‘ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) )
205 3 57 58 77 204 lo1le ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )
206 205 mptru ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 𝑆 ‘ ( 𝑛 − 1 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1)