Metamath Proof Explorer

Theorem mulog2sumlem3

Description: Lemma for mulog2sum . (Contributed by Mario Carneiro, 13-May-2016)

Ref Expression
Hypotheses logdivsum.1 ⊢ 𝐹 = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) )
mulog2sumlem.1 ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 )
Assertion mulog2sumlem3 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 logdivsum.1 ⊢ 𝐹 = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) )
2 mulog2sumlem.1 ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 )
3 2cn ⊢ 2 ∈ ℂ
4 3 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
5 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
6 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
7 6 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
8 mucl ⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ )
9 7 8 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
10 9 zred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
11 10 7 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
12 11 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
14 6 nnrpd ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
15 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
16 13 14 15 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
17 16 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
18 17 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
19 18 sqcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ∈ ℂ )
20 19 halfcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ∈ ℂ )
21 12 20 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ∈ ℂ )
22 5 21 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ∈ ℂ )
23 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
25 24 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
26 4 22 25 subdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
27 5 4 21 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) )
28 3 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ )
29 28 12 20 mul12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) )
30 2ne0 ⊢ 2 ≠ 0
31 30 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ≠ 0 )
32 19 28 31 divcan2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) = ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) )
33 32 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) )
34 29 33 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) )
35 34 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) )
36 27 35 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) )
37 36 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
38 26 37 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
39 38 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
40 22 25 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
41 rpssre ⊢ ℝ+ ⊆ ℝ
42 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) )
43 41 3 42 mp2an ⊢ ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1)
44 43 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) )
45 emre ⊢ γ ∈ ℝ
46 45 recni ⊢ γ ∈ ℂ
47 mulcl ⊢ ( ( γ ∈ ℂ ∧ ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ ) → ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
48 46 18 47 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
49 rlimcl ⊢ ( 𝐹 ⇝𝑟 𝐿 → 𝐿 ∈ ℂ )
50 2 49 syl ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
51 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐿 ∈ ℂ )
52 48 51 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ∈ ℂ )
53 20 52 addcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ∈ ℂ )
54 12 53 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) ∈ ℂ )
55 5 54 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) ∈ ℂ )
56 12 52 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ∈ ℂ )
57 5 56 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ∈ ℂ )
58 55 25 57 sub32d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( log ‘ 𝑥 ) ) )
59 5 54 56 fsumsub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) )
60 12 53 52 subdid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) − ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) )
61 20 52 pncand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) − ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) = ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) )
62 61 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) − ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) )
63 60 62 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) )
64 63 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) )
65 59 64 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) )
66 65 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) )
67 58 66 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) )
68 67 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) ) )
69 55 25 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
70 eqid ⊢ ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) = ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) )
71 eqid ⊢ ( ( ( 1 / 2 ) + ( γ + ( abs ‘ 𝐿 ) ) ) + Σ 𝑚 ∈ ( 1 ... 2 ) ( ( log ‘ ( e / 𝑚 ) ) / 𝑚 ) ) = ( ( ( 1 / 2 ) + ( γ + ( abs ‘ 𝐿 ) ) ) + Σ 𝑚 ∈ ( 1 ... 2 ) ( ( log ‘ ( e / 𝑚 ) ) / 𝑚 ) )
72 1 2 70 71 mulog2sumlem2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
73 46 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → γ ∈ ℂ )
74 12 18 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
75 5 73 74 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( γ · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
76 50 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐿 ∈ ℂ )
77 5 76 12 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) )
78 75 77 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( γ · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) )
79 mulcl ⊢ ( ( γ ∈ ℂ ∧ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) → ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
80 46 74 79 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
81 12 51 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ∈ ℂ )
82 5 80 81 fsumsub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) )
83 46 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → γ ∈ ℂ )
84 83 12 18 mul12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
85 84 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) )
86 12 48 51 subdid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) )
87 85 86 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) )
88 87 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( γ · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) )
89 78 82 88 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( γ · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) )
90 89 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( γ · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) )
91 5 74 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
92 mulcl ⊢ ( ( γ ∈ ℂ ∧ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) → ( γ · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
93 46 91 92 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( γ · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
94 5 12 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
95 94 76 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ∈ ℂ )
96 46 a1i ⊢ ( 𝜑 → γ ∈ ℂ )
97 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ γ ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ γ ) ∈ 𝑂(1) )
98 41 96 97 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ γ ) ∈ 𝑂(1) )
99 mulogsum ⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1)
100 99 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1) )
101 73 91 98 100 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( γ · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) )
102 mudivsum ⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1)
103 102 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1) )
104 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ 𝐿 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 𝐿 ) ∈ 𝑂(1) )
105 41 50 104 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 𝐿 ) ∈ 𝑂(1) )
106 94 76 103 105 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) ∈ 𝑂(1) )
107 93 95 101 106 o1sub2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( γ · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝐿 ) ) ) ∈ 𝑂(1) )
108 90 107 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) ∈ 𝑂(1) )
109 69 57 72 108 o1sub2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) − ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) ) ) ) ∈ 𝑂(1) )
110 68 109 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
111 4 40 44 110 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
112 39 111 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )