Theorem mulogsumlem

Description: Lemma for mulogsum . (Contributed by Mario Carneiro, 14-May-2016)

	Ref	Expression
Assertion	mulogsumlem	⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
2		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
3	2	adantl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
4		mucl	⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ )
5	3 4	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
6	5	zred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
7	6 3	nndivred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
8	7	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
9	1 8	fsumcl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
10	9	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
11		emre	⊢ γ ∈ ℝ
12	11	recni	⊢ γ ∈ ℂ
13	12	a1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → γ ∈ ℂ )
14		mudivsum	⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1)
15	14	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1) )
16		rpssre	⊢ ℝ+ ⊆ ℝ
17		o1const	⊢ ( ( ℝ+ ⊆ ℝ ∧ γ ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ γ ) ∈ 𝑂(1) )
18	16 12 17	mp2an	⊢ ( 𝑥 ∈ ℝ+ ↦ γ ) ∈ 𝑂(1)
19	18	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ γ ) ∈ 𝑂(1) )
20	10 13 15 19	o1mul2	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) ∈ 𝑂(1) )
21		fzfid	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin )
22		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ )
23	22	adantl	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ )
24	23	nnrecred	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
25	21 24	fsumrecl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ∈ ℝ )
26	2	nnrpd	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
27		rpdivcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
28	26 27	sylan2	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
29	28	relogcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
30	25 29	resubcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
31	7 30	remulcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
32	1 31	fsumrecl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
33	32	recnd	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
34	33	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
35		mulcl	⊢ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ∧ γ ∈ ℂ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ∈ ℂ )
36	9 12 35	sylancl	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ∈ ℂ )
37	36	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ∈ ℂ )
38		nnrecre	⊢ ( 𝑚 ∈ ℕ → ( 1 / 𝑚 ) ∈ ℝ )
39	38	recnd	⊢ ( 𝑚 ∈ ℕ → ( 1 / 𝑚 ) ∈ ℂ )
40	23 39	syl	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 1 / 𝑚 ) ∈ ℂ )
41	21 40	fsumcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ∈ ℂ )
42	29	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
43	41 42	subcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
44	8 43	mulcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
45		mulcl	⊢ ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ∧ γ ∈ ℂ ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ∈ ℂ )
46	8 12 45	sylancl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ∈ ℂ )
47	1 44 46	fsumsub	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) )
48	12	a1i	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → γ ∈ ℂ )
49	41 42 48	subsub4d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) − γ ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) )
50	49	oveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) − γ ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) )
51	8 43 48	subdid	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) − γ ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) )
52	50 51	eqtr3d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) )
53	52	sumeq2dv	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) )
54	12	a1i	⊢ ( 𝑥 ∈ ℝ+ → γ ∈ ℂ )
55	1 54 8	fsummulc1	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) )
56	55	oveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) )
57	47 53 56	3eqtr4d	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) )
58	57	mpteq2ia	⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) )
59	16	a1i	⊢ ( ⊤ → ℝ+ ⊆ ℝ )
60	42 48	addcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ∈ ℂ )
61	41 60	subcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ∈ ℂ )
62	8 61	mulcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ∈ ℂ )
63	1 62	fsumcl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ∈ ℂ )
64	63	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ∈ ℂ )
65		1red	⊢ ( ⊤ → 1 ∈ ℝ )
66	63	abscld	⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ∈ ℝ )
67	62	abscld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ∈ ℝ )
68	1 67	fsumrecl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ∈ ℝ )
69		1red	⊢ ( 𝑥 ∈ ℝ+ → 1 ∈ ℝ )
70	1 62	fsumabs	⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) )
71		rprege0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
72		flge0nn0	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
73	71 72	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
74	73	nn0red	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
75		rerpdivcl	⊢ ( ( ( ⌊ ‘ 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
76	74 75	mpancom	⊢ ( 𝑥 ∈ ℝ+ → ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
77		rpreccl	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
78	77	adantr	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑥 ) ∈ ℝ+ )
79	78	rpred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑥 ) ∈ ℝ )
80	8	abscld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
81	3	nnrecred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
82	61	abscld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ∈ ℝ )
83		id	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ+ )
84		rpdivcl	⊢ ( ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑛 / 𝑥 ) ∈ ℝ+ )
85	26 83 84	syl2anr	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 / 𝑥 ) ∈ ℝ+ )
86	85	rpred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 / 𝑥 ) ∈ ℝ )
87	8	absge0d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
88	61	absge0d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) )
89	6	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
90	3	nncnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
91	3	nnne0d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
92	89 90 91	absdivd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑛 ) / 𝑛 ) ) = ( ( abs ‘ ( μ ‘ 𝑛 ) ) / ( abs ‘ 𝑛 ) ) )
93	3	nnrpd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
94		rprege0	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) )
95	93 94	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) )
96		absid	⊢ ( ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) → ( abs ‘ 𝑛 ) = 𝑛 )
97	95 96	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ 𝑛 ) = 𝑛 )
98	97	oveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑛 ) ) / ( abs ‘ 𝑛 ) ) = ( ( abs ‘ ( μ ‘ 𝑛 ) ) / 𝑛 ) )
99	92 98	eqtrd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑛 ) / 𝑛 ) ) = ( ( abs ‘ ( μ ‘ 𝑛 ) ) / 𝑛 ) )
100	89	abscld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑛 ) ) ∈ ℝ )
101		1red	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
102		mule1	⊢ ( 𝑛 ∈ ℕ → ( abs ‘ ( μ ‘ 𝑛 ) ) ≤ 1 )
103	3 102	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑛 ) ) ≤ 1 )
104	100 101 93 103	lediv1dd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑛 ) ) / 𝑛 ) ≤ ( 1 / 𝑛 ) )
105	99 104	eqbrtrd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 1 / 𝑛 ) )
106		harmonicbnd4	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ≤ ( 1 / ( 𝑥 / 𝑛 ) ) )
107	28 106	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ≤ ( 1 / ( 𝑥 / 𝑛 ) ) )
108		rpcnne0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
109	108	adantr	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
110		rpcnne0	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
111	93 110	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
112		recdiv	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( 1 / ( 𝑥 / 𝑛 ) ) = ( 𝑛 / 𝑥 ) )
113	109 111 112	syl2anc	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( 𝑥 / 𝑛 ) ) = ( 𝑛 / 𝑥 ) )
114	107 113	breqtrd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ≤ ( 𝑛 / 𝑥 ) )
115	80 81 82 86 87 88 105 114	lemul12ad	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ≤ ( ( 1 / 𝑛 ) · ( 𝑛 / 𝑥 ) ) )
116	8 61	absmuld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) = ( ( abs ‘ ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) )
117		1cnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
118		dmdcan	⊢ ( ( ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ 1 ∈ ℂ ) → ( ( 𝑛 / 𝑥 ) · ( 1 / 𝑛 ) ) = ( 1 / 𝑥 ) )
119	111 109 117 118	syl3anc	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 / 𝑥 ) · ( 1 / 𝑛 ) ) = ( 1 / 𝑥 ) )
120	85	rpcnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 / 𝑥 ) ∈ ℂ )
121	81	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
122	120 121	mulcomd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 / 𝑥 ) · ( 1 / 𝑛 ) ) = ( ( 1 / 𝑛 ) · ( 𝑛 / 𝑥 ) ) )
123	119 122	eqtr3d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑥 ) = ( ( 1 / 𝑛 ) · ( 𝑛 / 𝑥 ) ) )
124	115 116 123	3brtr4d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ≤ ( 1 / 𝑥 ) )
125	1 67 79 124	fsumle	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑥 ) )
126		hashfz1	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
127	73 126	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
128	127	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 1 / 𝑥 ) ) = ( ( ⌊ ‘ 𝑥 ) · ( 1 / 𝑥 ) ) )
129	77	rpcnd	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℂ )
130		fsumconst	⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( 1 / 𝑥 ) ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑥 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 1 / 𝑥 ) ) )
131	1 129 130	syl2anc	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑥 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 1 / 𝑥 ) ) )
132	73	nn0cnd	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℂ )
133		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
134		rpne0	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
135	132 133 134	divrecd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) = ( ( ⌊ ‘ 𝑥 ) · ( 1 / 𝑥 ) ) )
136	128 131 135	3eqtr4d	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑥 ) = ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) )
137	125 136	breqtrd	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ≤ ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) )
138		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
139		flle	⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
140	138 139	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
141	133	mulridd	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 · 1 ) = 𝑥 )
142	140 141	breqtrrd	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ≤ ( 𝑥 · 1 ) )
143		reflcl	⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
144	138 143	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
145		rpregt0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
146		ledivmul	⊢ ( ( ( ⌊ ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ≤ 1 ↔ ( ⌊ ‘ 𝑥 ) ≤ ( 𝑥 · 1 ) ) )
147	144 69 145 146	syl3anc	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ≤ 1 ↔ ( ⌊ ‘ 𝑥 ) ≤ ( 𝑥 · 1 ) ) )
148	142 147	mpbird	⊢ ( 𝑥 ∈ ℝ+ → ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ≤ 1 )
149	68 76 69 137 148	letrd	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ≤ 1 )
150	66 68 69 70 149	letrd	⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ≤ 1 )
151	150	ad2antrl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ≤ 1 )
152	59 64 65 65 151	elo1d	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( ( log ‘ ( 𝑥 / 𝑛 ) ) + γ ) ) ) ) ∈ 𝑂(1) )
153	58 152	eqeltrrid	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) ) ∈ 𝑂(1) )
154	34 37 153	o1dif	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) · γ ) ) ∈ 𝑂(1) ) )
155	20 154	mpbird	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) )
156	155	mptru	⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1)