mudivsum - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mudivsum		Structured version Visualization version GIF version

Theorem mudivsum 27481

Description: Asymptotic formula for Σ𝑛 ≤ 𝑥, μ(𝑛) / 𝑛 = 𝑂(1). Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.)

**Assertion**
Ref	Expression
mudivsum	⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)

Distinct variable group: 𝑥,𝑛

Proof of Theorem mudivsum Dummy variables 𝑘 𝑚 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1red 11245	. . 3 ⊢ (⊤ → 1 ∈ ℝ)
2		reex 11229	. . . . . . 7 ⊢ ℝ ∈ V
3		rpssre 13013	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℝ
4	2, 3	ssexi 5317	. . . . . 6 ⊢ ℝ⁺ ∈ V
5	4	a1i 11	. . . . 5 ⊢ (⊤ → ℝ⁺ ∈ V)
6		fzfid 13970	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (1...(⌊‘𝑥)) ∈ Fin)
7		rpre 13014	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
8		elfznn 13562	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
9		nndivre 12283	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ)
10	7, 8, 9	syl2an 594	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
11	10	recnd 11272	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
12		reflcl 13793	. . . . . . . . . . . 12 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
13	10, 12	syl 17	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
14	13	recnd 11272	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
15	11, 14	subcld 11601	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
16	8	adantl 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
17		mucl 27091	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
19	18	zcnd 12697	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
20	15, 19	mulcld 11264	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
21	6, 20	fsumcl 15711	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
22		rpcn 13016	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
23		rpne0 13022	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
24	21, 22, 23	divcld 12020	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
25	24	adantl 480	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
26		ovexd 7451	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (1 / 𝑥) ∈ V)
27		eqidd 2726	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)))
28		eqidd 2726	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)))
29	5, 25, 26, 27, 28	offval2 7702	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
30	3	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ⁺ ⊆ ℝ)
31	21	adantr 479	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
32	22	adantr 479	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℂ)
33	23	adantr 479	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ≠ 0)
34	31, 32, 33	absdivd 15434	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)))
35		rprege0 13021	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
36		absid 15275	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘𝑥) = 𝑥)
38	37	adantr 479	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
39	38	oveq2d 7432	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
40	34, 39	eqtrd 2765	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
41	31	abscld 15415	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
42		fzfid 13970	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ∈ Fin)
43	20	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
44	43	abscld 15415	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
45	42, 44	fsumrecl 15712	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
46	7	adantr 479	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ)
47	42, 43	fsumabs 15779	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))))
48		reflcl 13793	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
49	46, 48	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℝ)
50		1red 11245	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
51	15	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
52		fz1ssnn 13564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...(⌊‘𝑥)) ⊆ ℕ
53	52	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ⊆ ℕ)
54	53	sselda 3972	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
55	54, 17	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
56	55	zcnd 12697	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
57	51, 56	absmuld 15433	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) = ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))))
58	51	abscld 15415	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ∈ ℝ)
59	56	abscld 15415	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
60	51	absge0d 15423	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))))
61	56	absge0d 15423	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(μ‘𝑛)))
62		simpl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ⁺)
63	8	nnrpd 13046	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
64		rpdivcl 13031	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
65	62, 63, 64	syl2an 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
66	3, 65	sselid 3970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
67	66, 12	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
68		flle 13796	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
69	66, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
70	67, 66, 69	abssubge0d 15410	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))
71		fracle1 13800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
72	66, 71	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
73	70, 72	eqbrtrd 5165	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ≤ 1)
74		mule1 27098	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
75	54, 74	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
76	58, 50, 59, 50, 60, 61, 73, 75	lemul12ad 12186	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ (1 · 1))
77		1t1e1 12404	. . . . . . . . . . . . . . . 16 ⊢ (1 · 1) = 1
78	76, 77	breqtrdi 5184	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ 1)
79	57, 78	eqbrtrd 5165	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 1)
80	42, 44, 50, 79	fsumle 15777	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))1)
81		1cnd 11239	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ ℂ)
82		fsumconst 15768	. . . . . . . . . . . . . . 15 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((♯‘(1...(⌊‘𝑥))) · 1))
83	42, 81, 82	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((♯‘(1...(⌊‘𝑥))) · 1))
84		flge1nn 13818	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
85	7, 84	sylan 578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
86	85	nnnn0d 12562	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
87		hashfz1 14337	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
88	86, 87	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
89	88	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((♯‘(1...(⌊‘𝑥))) · 1) = ((⌊‘𝑥) · 1))
90	49	recnd 11272	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℂ)
91	90	mulridd 11261	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((⌊‘𝑥) · 1) = (⌊‘𝑥))
92	83, 89, 91	3eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = (⌊‘𝑥))
93	80, 92	breqtrd 5169	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (⌊‘𝑥))
94		flle 13796	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
95	46, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ≤ 𝑥)
96	45, 49, 46, 93, 95	letrd 11401	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
97	41, 45, 46, 47, 96	letrd 11401	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
98	32	mulridd 11261	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · 1) = 𝑥)
99	97, 98	breqtrrd 5171	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1))
100		1red 11245	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ ℝ)
101	41, 100, 62	ledivmuld 13101	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1 ↔ (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1)))
102	99, 101	mpbird 256	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1)
103	40, 102	eqbrtrd 5165	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
104	103	adantl 480	. . . . . 6 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
105	30, 25, 1, 1, 104	elo1d 15512	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1))
106		ax-1cn 11196	. . . . . . 7 ⊢ 1 ∈ ℂ
107		divrcnv 15830	. . . . . . 7 ⊢ (1 ∈ ℂ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0)
108	106, 107	ax-mp 5	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0
109		rlimo1 15593	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0 → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1))
110	108, 109	mp1i 13	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1))
111		o1add 15590	. . . . 5 ⊢ (((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))) ∈ 𝑂(1))
112	105, 110, 111	syl2anc 582	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))) ∈ 𝑂(1))
113	29, 112	eqeltrrd 2826	. . 3 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
114		ovexd 7451	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V)
115	18	zred 12696	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
116	115, 16	nndivred 12296	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
117	116	recnd 11272	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
118	6, 117	fsumcl 15711	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
119	118	adantl 480	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
120	118	adantr 479	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
121	120	abscld 15415	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ)
122	117	adantlr 713	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
123	42, 32, 122	fsummulc2 15762	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
124	14, 19	mulcld 11264	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
125	124	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
126	42, 43, 125	fsumadd 15718	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
127	11	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
128	14	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
129	127, 128	npcand 11605	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) = (𝑥 / 𝑛))
130	129	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((𝑥 / 𝑛) · (μ‘𝑛)))
131	51, 128, 56	adddird 11269	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
132	32	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
133	54	nnrpd 13046	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
134		rpcnne0 13024	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
135	133, 134	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
136		div23 11921	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = ((𝑥 / 𝑛) · (μ‘𝑛)))
137		divass 11920	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = (𝑥 · ((μ‘𝑛) / 𝑛)))
138	136, 137	eqtr3d 2767	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
139	132, 56, 135, 138	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
140	130, 131, 139	3eqtr3d 2773	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (𝑥 · ((μ‘𝑛) / 𝑛)))
141	140	sumeq2dv 15681	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
142		eqidd 2726	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → (μ‘𝑛) = (μ‘𝑛))
143		ssrab2 4069	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ
144		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})
145	143, 144	sselid 3970	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ)
146	145, 17	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ)
147	146	zcnd 12697	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℂ)
148	142, 46, 147	dvdsflsumcom 27138	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛))
149	147	3impb 1112	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (μ‘𝑛) ∈ ℂ)
150	149	mulridd 11261	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((μ‘𝑛) · 1) = (μ‘𝑛))
151	150	2sumeq2dv 15683	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛))
152		eqidd 2726	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → 1 = 1)
153		nnuz 12895	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
154	85, 153	eleqtrdi 2835	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ (ℤ_≥‘1))
155		eluzfz1 13540	. . . . . . . . . . . . . . 15 ⊢ ((⌊‘𝑥) ∈ (ℤ_≥‘1) → 1 ∈ (1...(⌊‘𝑥)))
156	154, 155	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ (1...(⌊‘𝑥)))
157		1cnd 11239	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
158	152, 42, 53, 156, 157	musumsum 27142	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = 1)
159	151, 158	eqtr3d 2767	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = 1)
160		fzfid 13970	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
161		fsumconst 15768	. . . . . . . . . . . . . . 15 ⊢ (((1...(⌊‘(𝑥 / 𝑛))) ∈ Fin ∧ (μ‘𝑛) ∈ ℂ) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
162	160, 56, 161	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
163		rprege0 13021	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → ((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)))
164		flge0nn0 13817	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)) → (⌊‘(𝑥 / 𝑛)) ∈ ℕ₀)
165		hashfz1 14337	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘(𝑥 / 𝑛)) ∈ ℕ₀ → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
166	65, 163, 164, 165	4syl 19	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
167	166	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
168	162, 167	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
169	168	sumeq2dv 15681	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
170	148, 159, 169	3eqtr3rd 2774	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) = 1)
171	170	oveq2d 7432	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
172	126, 141, 171	3eqtr3d 2773	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
173	123, 172	eqtrd 2765	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
174	173	oveq1d 7431	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥))
175	120, 32, 33	divcan3d 12025	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛))
176		rpcnne0 13024	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
177	176	adantr 479	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
178		divdir 11927	. . . . . . . 8 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
179	31, 81, 177, 178	syl3anc 1368	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
180	174, 175, 179	3eqtr3d 2773	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
181	180	fveq2d 6896	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
182	121, 181	eqled 11347	. . . 4 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
183	182	adantl 480	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
184	1, 113, 114, 119, 183	o1le 15631	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1))
185	184	mptru 1540	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ∧ wa 394 ∧ w3a 1084 = wceq 1533 ⊤wtru 1534 ∈ wcel 2098 ≠ wne 2930 {crab 3419 Vcvv 3463 ⊆ wss 3939 class class class wbr 5143 ↦ cmpt 5226 ‘cfv 6543 (class class class)co 7416 ∘_f cof 7680 Fincfn 8962 ℂcc 11136 ℝcr 11137 0cc0 11138 1c1 11139 + caddc 11141 · cmul 11143 ≤ cle 11279 − cmin 11474 / cdiv 11901 ℕcn 12242 ℕ₀cn0 12502 ℤcz 12588 ℤ_≥cuz 12852 ℝ⁺crp 13006 ...cfz 13516 ⌊cfl 13787 ♯chash 14321 abscabs 15213 ⇝_𝑟 crli 15461 𝑂(1)co1 15462 Σcsu 15664 ∥ cdvds 16230 μcmu 27045

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7738 ax-inf2 9664 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3769 df-csb 3885 df-dif 3942 df-un 3944 df-in 3946 df-ss 3956 df-pss 3959 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-disj 5109 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7372 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7682 df-om 7869 df-1st 7991 df-2nd 7992 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-oadd 8489 df-er 8723 df-map 8845 df-pm 8846 df-en 8963 df-dom 8964 df-sdom 8965 df-fin 8966 df-sup 9465 df-inf 9466 df-oi 9533 df-dju 9924 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-div 11902 df-nn 12243 df-2 12305 df-3 12306 df-n0 12503 df-xnn0 12575 df-z 12589 df-uz 12853 df-q 12963 df-rp 13007 df-ico 13362 df-fz 13517 df-fzo 13660 df-fl 13789 df-mod 13867 df-seq 13999 df-exp 14059 df-fac 14265 df-bc 14294 df-hash 14322 df-cj 15078 df-re 15079 df-im 15080 df-sqrt 15214 df-abs 15215 df-clim 15464 df-rlim 15465 df-o1 15466 df-lo1 15467 df-sum 15665 df-dvds 16231 df-gcd 16469 df-prm 16642 df-pc 16805 df-mu 27051

This theorem is referenced by: mulogsumlem 27482 mulog2sumlem3 27487 selberglem1 27496

W3C validator