Theorem mulogsum

Description: Asymptotic formula for sum_ n <_ x , ( mmu ( n ) / n ) log ( x / n ) = O(1) . Equation 10.2.6 of Shapiro, p. 406. (Contributed by Mario Carneiro, 14-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		rpssre	⊢ ℝ+ ⊆ ℝ
2		ax-1cn	⊢ 1 ∈ ℂ
3		o1const	⊢ ( ( ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) )
4	1 2 3	mp2an	⊢ ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1)
5		1cnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
6		fzfid	⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
7		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
8	7	adantl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
9		mucl	⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ )
10	8 9	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
11	10	zred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
12	11 8	nndivred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
13	7	nnrpd	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
14		rpdivcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
15	13 14	sylan2	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
16	15	relogcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
17	12 16	remulcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
18	17	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
19	6 18	fsumcl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
20	19	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
21		mulogsumlem	⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1)
22		sumex	⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ V
23	22	a1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ V )
24	21	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) )
25	23 24	o1mptrcl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
26	5 20	subcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
27		1red	⊢ ( ⊤ → 1 ∈ ℝ )
28		fz1ssnn	⊢ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ℕ
29	28	a1i	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ℕ )
30	29	sselda	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
31	30 9	syl	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
32	31	zred	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
33	32 30	nndivred	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
34	33	recnd	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
35		fzfid	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin )
36		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ )
37	36	adantl	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ )
38	37	nnrpd	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ )
39	38	rpcnne0d	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
40		reccl	⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) → ( 1 / 𝑚 ) ∈ ℂ )
41	39 40	syl	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 1 / 𝑚 ) ∈ ℂ )
42	35 41	fsumcl	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ∈ ℂ )
43		simpl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 𝑥 ∈ ℝ+ )
44	43 13 14	syl2an	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
45	44	relogcld	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
46	45	recnd	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
47	34 42 46	subdid	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
48	47	sumeq2dv	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
49		fzfid	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
50	34 42	mulcld	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) ∈ ℂ )
51	18	adantlr	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
52	49 50 51	fsumsub	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
53		oveq2	⊢ ( 𝑘 = ( 𝑛 · 𝑚 ) → ( 1 / 𝑘 ) = ( 1 / ( 𝑛 · 𝑚 ) ) )
54	53	oveq2d	⊢ ( 𝑘 = ( 𝑛 · 𝑚 ) → ( ( μ ‘ 𝑛 ) · ( 1 / 𝑘 ) ) = ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) )
55		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
56	55	adantr	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
57		ssrab2	⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ℕ
58		simprr	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } )
59	57 58	sselid	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑛 ∈ ℕ )
60	59 9	syl	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
61	60	zcnd	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
62		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ ℕ )
63	62	adantl	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℕ )
64	63	nnrecred	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑘 ) ∈ ℝ )
65	64	recnd	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑘 ) ∈ ℂ )
66	65	adantrr	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( 1 / 𝑘 ) ∈ ℂ )
67	61 66	mulcld	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( ( μ ‘ 𝑛 ) · ( 1 / 𝑘 ) ) ∈ ℂ )
68	54 56 67	dvdsflsumcom	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( μ ‘ 𝑛 ) · ( 1 / 𝑘 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) )
69		oveq2	⊢ ( 𝑘 = 1 → ( 1 / 𝑘 ) = ( 1 / 1 ) )
70		1div1e1	⊢ ( 1 / 1 ) = 1
71	69 70	eqtrdi	⊢ ( 𝑘 = 1 → ( 1 / 𝑘 ) = 1 )
72		flge1nn	⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
73	55 72	sylan	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
74		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
75	73 74	eleqtrdi	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) )
76		eluzfz1	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
77	75 76	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
78	71 49 29 77 65	musumsum	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( μ ‘ 𝑛 ) · ( 1 / 𝑘 ) ) = 1 )
79	31	zcnd	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
80	79	adantr	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
81	30	adantr	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑛 ∈ ℕ )
82	81	nnrpd	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑛 ∈ ℝ+ )
83	82	rpcnne0d	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
84		divdiv1	⊢ ( ( ( μ ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) / 𝑚 ) = ( ( μ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) )
85	80 83 39 84	syl3anc	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) / 𝑚 ) = ( ( μ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) )
86	34	adantr	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
87	37	nncnd	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℂ )
88	37	nnne0d	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ≠ 0 )
89	86 87 88	divrecd	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) / 𝑚 ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) )
90		nnmulcl	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( 𝑛 · 𝑚 ) ∈ ℕ )
91	30 36 90	syl2an	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 · 𝑚 ) ∈ ℕ )
92	91	nncnd	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 · 𝑚 ) ∈ ℂ )
93	91	nnne0d	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 · 𝑚 ) ≠ 0 )
94	80 92 93	divrecd	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( μ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) = ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) )
95	85 89 94	3eqtr3rd	⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) )
96	95	sumeq2dv	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) )
97	35 34 41	fsummulc2	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) )
98	96 97	eqtr4d	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) )
99	98	sumeq2dv	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) )
100	68 78 99	3eqtr3rd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) = 1 )
101	100	oveq1d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
102	48 52 101	3eqtrd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
103	102	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
104	25 26 27 103	o1eq	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) ) )
105	21 104	mpbii	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) )
106	5 20 105	o1dif	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1) ) )
107	4 106	mpbii	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1) )
108	107	mptru	⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1)