Metamath Proof Explorer

Theorem selberg34r

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

Ref Expression
Hypothesis pntrval.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
Assertion selberg34r ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 pntrval.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 2re ⊢ 2 ∈ ℝ
3 2 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ )
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 1 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
15 14 ffvelcdmi ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
16 13 15 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
17 13 relogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
18 16 17 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
19 3 18 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
20 19 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
21 5 11 rplogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
22 3 21 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ )
23 22 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℂ )
24 fzfid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
25 13 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
26 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
27 26 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
28 27 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
29 25 28 rpdivcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
30 14 ffvelcdmi ⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
31 29 30 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
32 fzfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... 𝑛 ) ∈ Fin )
33 dvdsssfz1 ⊢ ( 𝑛 ∈ ℕ → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
34 27 33 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
35 32 34 ssfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ∈ Fin )
36 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ℕ
37 simpr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
38 36 37 sselid ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 𝑚 ∈ ℕ )
39 vmacl ⊢ ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ )
40 38 39 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
41 dvdsdivcl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
42 27 41 sylan ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
43 36 42 sselid ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ ℕ )
44 vmacl ⊢ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( Λ ‘ ( 𝑛 / 𝑚 ) ) ∈ ℝ )
45 43 44 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( Λ ‘ ( 𝑛 / 𝑚 ) ) ∈ ℝ )
46 40 45 remulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℝ )
47 35 46 fsumrecl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℝ )
48 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
49 27 48 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
50 28 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
51 49 50 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
52 47 51 resubcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
53 31 52 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
54 24 53 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
55 54 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ )
56 23 55 mulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℂ )
57 20 56 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) ∈ ℂ )
58 5 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
59 2cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ )
60 13 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
61 2ne0 ⊢ 2 ≠ 0
62 61 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ≠ 0 )
63 57 58 59 60 62 divdiv32d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) / 2 ) = ( ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 2 ) / 𝑥 ) )
64 57 58 60 divcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) ∈ ℂ )
65 64 59 62 divrecd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) / 2 ) = ( ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) · ( 1 / 2 ) ) )
66 20 56 59 62 divsubdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 2 ) = ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 2 ) − ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / 2 ) ) )
67 18 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
68 67 59 62 divcan3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 2 ) = ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) )
69 21 rpcnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
70 21 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
71 59 69 55 70 div32d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) )
72 71 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / 2 ) = ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 2 ) )
73 54 21 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
74 73 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
75 74 59 62 divcan3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 2 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) )
76 72 75 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / 2 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) )
77 68 76 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 2 ) − ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) / 2 ) ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) )
78 66 77 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 2 ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) )
79 78 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 2 ) / 𝑥 ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
80 63 65 79 3eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) · ( 1 / 2 ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
81 80 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) · ( 1 / 2 ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) )
82 22 54 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
83 19 82 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) ∈ ℝ )
84 83 13 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) ∈ ℝ )
85 8 rehalfcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 / 2 ) ∈ ℝ )
86 31 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
87 47 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℂ )
88 49 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
89 50 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
90 88 89 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
91 86 87 90 subdid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) − ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) )
92 86 88 89 mul12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( ( Λ ‘ 𝑛 ) · ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) )
93 88 86 89 mulassd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = ( ( Λ ‘ 𝑛 ) · ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) )
94 92 93 eqtr4d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
95 94 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) − ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
96 91 95 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
97 96 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
98 86 87 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) ∈ ℂ )
99 88 86 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
100 99 89 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
101 24 98 100 fsumsub ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
102 46 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℂ )
103 35 86 102 fsummulc2 ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) = Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
104 103 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
105 oveq2 ⊢ ( 𝑛 = ( 𝑚 · 𝑘 ) → ( 𝑥 / 𝑛 ) = ( 𝑥 / ( 𝑚 · 𝑘 ) ) )
106 105 fveq2d ⊢ ( 𝑛 = ( 𝑚 · 𝑘 ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) = ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) )
107 fvoveq1 ⊢ ( 𝑛 = ( 𝑚 · 𝑘 ) → ( Λ ‘ ( 𝑛 / 𝑚 ) ) = ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) )
108 107 oveq2d ⊢ ( 𝑛 = ( 𝑚 · 𝑘 ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) )
109 106 108 oveq12d ⊢ ( 𝑛 = ( 𝑚 · 𝑘 ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) = ( ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) ) )
110 31 adantrr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
111 40 anasss ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
112 45 anasss ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( Λ ‘ ( 𝑛 / 𝑚 ) ) ∈ ℝ )
113 111 112 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℝ )
114 110 113 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) ∈ ℝ )
115 114 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) ∈ ℂ )
116 109 5 115 dvdsflsumcom ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) ) )
117 58 ad2antrr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑥 ∈ ℂ )
118 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ )
119 118 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
120 119 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ )
121 120 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑚 ∈ ℝ+ )
122 121 rpcnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑚 ∈ ℂ )
123 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) → 𝑘 ∈ ℕ )
124 123 adantl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑘 ∈ ℕ )
125 124 nncnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑘 ∈ ℂ )
126 121 rpne0d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑚 ≠ 0 )
127 124 nnne0d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑘 ≠ 0 )
128 117 122 125 126 127 divdiv1d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( 𝑥 / 𝑚 ) / 𝑘 ) = ( 𝑥 / ( 𝑚 · 𝑘 ) ) )
129 128 eqcomd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( 𝑥 / ( 𝑚 · 𝑘 ) ) = ( ( 𝑥 / 𝑚 ) / 𝑘 ) )
130 129 fveq2d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) = ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) )
131 125 122 126 divcan3d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( 𝑚 · 𝑘 ) / 𝑚 ) = 𝑘 )
132 131 fveq2d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) = ( Λ ‘ 𝑘 ) )
133 132 oveq2d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) )
134 130 133 oveq12d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) ) = ( ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) ) )
135 13 ad2antrr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑥 ∈ ℝ+ )
136 135 121 rpdivcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( 𝑥 / 𝑚 ) ∈ ℝ+ )
137 124 nnrpd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑘 ∈ ℝ+ )
138 136 137 rpdivcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( 𝑥 / 𝑚 ) / 𝑘 ) ∈ ℝ+ )
139 14 ffvelcdmi ⊢ ( ( ( 𝑥 / 𝑚 ) / 𝑘 ) ∈ ℝ+ → ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ∈ ℝ )
140 138 139 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ∈ ℝ )
141 140 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ∈ ℂ )
142 119 39 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
143 142 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ )
144 143 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ )
145 vmacl ⊢ ( 𝑘 ∈ ℕ → ( Λ ‘ 𝑘 ) ∈ ℝ )
146 124 145 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑘 ) ∈ ℝ )
147 146 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑘 ) ∈ ℂ )
148 144 147 mulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) ∈ ℂ )
149 141 148 mulcomd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) ) = ( ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) )
150 144 147 141 mulassd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) )
151 134 149 150 3eqtrd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) ) = ( ( Λ ‘ 𝑚 ) · ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) )
152 151 sumeq2dv ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) )
153 fzfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ Fin )
154 146 140 remulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ∈ ℝ )
155 154 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ∈ ℂ )
156 153 143 155 fsummulc2 ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) )
157 152 156 eqtr4d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) ) = ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) )
158 157 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( 𝑅 ‘ ( 𝑥 / ( 𝑚 · 𝑘 ) ) ) · ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) )
159 104 116 158 3eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) )
160 159 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
161 97 101 160 3eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
162 161 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
163 153 154 fsumrecl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ∈ ℝ )
164 142 163 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ∈ ℝ )
165 24 164 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ∈ ℝ )
166 165 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ∈ ℂ )
167 49 31 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
168 167 50 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
169 24 168 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
170 169 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
171 23 166 170 subdid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
172 162 171 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
173 172 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) = ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) ) )
174 23 166 mulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ∈ ℂ )
175 22 169 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
176 175 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
177 20 174 176 subsub3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) ) = ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) )
178 173 177 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) = ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) )
179 67 2timesd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
180 179 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
181 67 176 67 add32d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
182 180 181 eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
183 182 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) )
184 18 175 readdcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
185 184 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ )
186 185 67 174 addsubassd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) ) )
187 178 183 186 3eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) ) )
188 187 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) ) / 𝑥 ) )
189 67 174 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) ∈ ℂ )
190 185 189 58 60 divdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) ) / 𝑥 ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) / 𝑥 ) ) )
191 188 190 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) / 𝑥 ) ) )
192 191 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) / 𝑥 ) ) ) )
193 184 13 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ )
194 22 165 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ∈ ℝ )
195 18 194 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) ∈ ℝ )
196 195 13 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) / 𝑥 ) ∈ ℝ )
197 1 selberg3r ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)
198 197 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
199 1 selberg4r ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)
200 199 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
201 193 196 198 200 o1add2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑘 ) · ( 𝑅 ‘ ( ( 𝑥 / 𝑚 ) / 𝑘 ) ) ) ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1) )
202 192 201 eqeltrd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
203 ioossre ⊢ ( 1 (,) +∞ ) ⊆ ℝ
204 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
205 204 halfcld ⊢ ( ⊤ → ( 1 / 2 ) ∈ ℂ )
206 o1const ⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ ( 1 / 2 ) ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / 2 ) ) ∈ 𝑂(1) )
207 203 205 206 sylancr ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / 2 ) ) ∈ 𝑂(1) )
208 84 85 202 207 o1mul2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 · ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) ) ) / 𝑥 ) · ( 1 / 2 ) ) ) ∈ 𝑂(1) )
209 81 208 eqeltrrd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
210 209 mptru ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) · ( Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) − ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ 𝑂(1)