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) )