Metamath Proof Explorer

Theorem dchrvmasumiflem2

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
dchrvmasumif.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
dchrvmasumif.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
dchrvmasumif.s ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
dchrvmasumif.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
dchrvmasumif.g ⊢ 𝐾 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) )
dchrvmasumif.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
dchrvmasumif.t ⊢ ( 𝜑 → seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
dchrvmasumif.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
Assertion dchrvmasumiflem2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
9 dchrvmasumif.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10 dchrvmasumif.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11 dchrvmasumif.s ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
12 dchrvmasumif.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
13 dchrvmasumif.g ⊢ 𝐾 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) )
14 dchrvmasumif.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
15 dchrvmasumif.t ⊢ ( 𝜑 → seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
16 dchrvmasumif.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
17 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
18 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
19 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
20 elfzelz ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℤ )
21 20 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℤ )
22 4 1 5 2 19 21 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
23 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
24 23 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
25 mucl ⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
26 24 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
27 26 zred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
28 27 24 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
29 28 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
30 22 29 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
31 18 30 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
32 climcl ⊢ ( seq 1 ( + , 𝐹 ) ⇝ 𝑆 → 𝑆 ∈ ℂ )
33 11 32 syl ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑆 ∈ ℂ )
35 31 34 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) ∈ ℂ )
36 0cnd ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → 0 ∈ ℂ )
37 df-ne ⊢ ( 𝑆 ≠ 0 ↔ ¬ 𝑆 = 0 )
38 climcl ⊢ ( seq 1 ( + , 𝐾 ) ⇝ 𝑇 → 𝑇 ∈ ℂ )
39 15 38 syl ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝑇 ∈ ℂ )
41 33 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝑆 ∈ ℂ )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝑆 ≠ 0 )
43 40 41 42 divcld ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ( 𝑇 / 𝑆 ) ∈ ℂ )
44 37 43 sylan2br ⊢ ( ( 𝜑 ∧ ¬ 𝑆 = 0 ) → ( 𝑇 / 𝑆 ) ∈ ℂ )
45 36 44 ifclda ⊢ ( 𝜑 → if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ∈ ℂ )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ∈ ℂ )
47 1 2 3 4 5 6 7 8 9 10 11 12 dchrmusum2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) ) ∈ 𝑂(1) )
48 rpssre ⊢ ℝ+ ⊆ ℝ
49 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ∈ 𝑂(1) )
50 48 45 49 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ∈ 𝑂(1) )
51 35 46 47 50 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) ∈ 𝑂(1) )
52 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ∈ Fin )
53 19 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑋 ∈ 𝐷 )
54 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) → 𝑘 ∈ ℤ )
55 54 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑘 ∈ ℤ )
56 4 1 5 2 53 55 dchrzrhcl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
58 23 nnrpd ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℝ+ )
59 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
60 57 58 59 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
61 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) → 𝑘 ∈ ℕ )
62 61 nnrpd ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) → 𝑘 ∈ ℝ+ )
63 ifcl ⊢ ( ( ( 𝑥 / 𝑑 ) ∈ ℝ+ ∧ 𝑘 ∈ ℝ+ ) → if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ∈ ℝ+ )
64 60 62 63 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ∈ ℝ+ )
65 64 relogcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) ∈ ℝ )
66 61 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑘 ∈ ℕ )
67 65 66 nndivred ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ∈ ℝ )
68 67 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ∈ ℂ )
69 56 68 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ∈ ℂ )
70 52 69 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ∈ ℂ )
71 30 70 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℂ )
72 18 71 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℂ )
73 35 46 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ∈ ℂ )
74 0cn ⊢ 0 ∈ ℂ
75 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑇 ∈ ℂ )
76 ifcl ⊢ ( ( 0 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ ℂ )
77 74 75 76 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ ℂ )
78 30 70 77 subdid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
79 78 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
80 30 77 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) ∈ ℂ )
81 18 71 80 fsumsub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
82 31 34 46 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝑆 · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) )
83 ovif2 ⊢ ( 𝑆 · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , ( 𝑆 · 0 ) , ( 𝑆 · ( 𝑇 / 𝑆 ) ) )
84 33 mul01d ⊢ ( 𝜑 → ( 𝑆 · 0 ) = 0 )
85 84 ifeq1d ⊢ ( 𝜑 → if ( 𝑆 = 0 , ( 𝑆 · 0 ) , ( 𝑆 · ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , ( 𝑆 · ( 𝑇 / 𝑆 ) ) ) )
86 40 41 42 divcan2d ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ( 𝑆 · ( 𝑇 / 𝑆 ) ) = 𝑇 )
87 37 86 sylan2br ⊢ ( ( 𝜑 ∧ ¬ 𝑆 = 0 ) → ( 𝑆 · ( 𝑇 / 𝑆 ) ) = 𝑇 )
88 87 ifeq2da ⊢ ( 𝜑 → if ( 𝑆 = 0 , 0 , ( 𝑆 · ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , 𝑇 ) )
89 85 88 eqtrd ⊢ ( 𝜑 → if ( 𝑆 = 0 , ( 𝑆 · 0 ) , ( 𝑆 · ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , 𝑇 ) )
90 83 89 eqtrid ⊢ ( 𝜑 → ( 𝑆 · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , 𝑇 ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑆 · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , 𝑇 ) )
92 91 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝑆 · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) )
93 74 39 76 sylancr ⊢ ( 𝜑 → if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ ℂ )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ ℂ )
95 18 94 30 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) )
96 82 92 95 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) = ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) )
97 96 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) )
98 79 81 97 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) )
99 98 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) ) )
100 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 dchrvmasumiflem1 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ) ∈ 𝑂(1) )
101 99 100 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) − ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) ) ∈ 𝑂(1) )
102 72 73 101 o1dif ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑆 ) · if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) ∈ 𝑂(1) ) )
103 51 102 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) ) ∈ 𝑂(1) )
104 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
105 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ )
106 105 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℤ )
107 4 1 5 2 104 106 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
108 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
109 108 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
110 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
111 nndivre ⊢ ( ( ( Λ ‘ 𝑛 ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
112 110 111 mpancom ⊢ ( 𝑛 ∈ ℕ → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
113 109 112 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
114 113 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
115 107 114 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
116 18 115 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
117 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
119 118 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
120 ifcl ⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ∈ ℂ )
121 119 74 120 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ∈ ℂ )
122 116 121 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ∈ ℂ )
123 122 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
124 123 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
125 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑁 ∈ ℕ )
126 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑋 ∈ 𝐷 )
127 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑋 ≠ 1 )
128 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
129 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
130 1 2 125 4 5 6 126 127 128 129 dchrvmasum2if ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) )
131 130 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) = ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) ) )
132 124 131 eqled ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ≤ ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) ) ) )
133 17 103 72 122 132 o1le ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )