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 27559

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 11265	. . 3 ⊢ (⊤ → 1 ∈ ℝ)
2		reex 11249	. . . . . . 7 ⊢ ℝ ∈ V
3		rpssre 13035	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℝ
4	2, 3	ssexi 5327	. . . . . 6 ⊢ ℝ⁺ ∈ V
5	4	a1i 11	. . . . 5 ⊢ (⊤ → ℝ⁺ ∈ V)
6		fzfid 13993	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (1...(⌊‘𝑥)) ∈ Fin)
7		rpre 13036	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
8		elfznn 13584	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
9		nndivre 12305	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ)
10	7, 8, 9	syl2an 594	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
11	10	recnd 11292	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
12		reflcl 13816	. . . . . . . . . . . 12 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
13	10, 12	syl 17	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
14	13	recnd 11292	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
15	11, 14	subcld 11621	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
16	8	adantl 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
17		mucl 27169	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
19	18	zcnd 12719	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
20	15, 19	mulcld 11284	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
21	6, 20	fsumcl 15737	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
22		rpcn 13038	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
23		rpne0 13044	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
24	21, 22, 23	divcld 12041	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
25	24	adantl 480	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
26		ovexd 7459	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (1 / 𝑥) ∈ V)
27		eqidd 2727	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)))
28		eqidd 2727	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)))
29	5, 25, 26, 27, 28	offval2 7710	. . . 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 15460	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)))
35		rprege0 13043	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
36		absid 15301	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘𝑥) = 𝑥)
38	37	adantr 479	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
39	38	oveq2d 7440	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
40	34, 39	eqtrd 2766	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
41	31	abscld 15441	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
42		fzfid 13993	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ∈ Fin)
43	20	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
44	43	abscld 15441	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
45	42, 44	fsumrecl 15738	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
46	7	adantr 479	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ)
47	42, 43	fsumabs 15805	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))))
48		reflcl 13816	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
49	46, 48	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℝ)
50		1red 11265	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
51	15	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
52		fz1ssnn 13586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...(⌊‘𝑥)) ⊆ ℕ
53	52	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ⊆ ℕ)
54	53	sselda 3979	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
55	54, 17	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
56	55	zcnd 12719	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
57	51, 56	absmuld 15459	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) = ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))))
58	51	abscld 15441	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ∈ ℝ)
59	56	abscld 15441	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
60	51	absge0d 15449	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))))
61	56	absge0d 15449	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(μ‘𝑛)))
62		simpl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ⁺)
63	8	nnrpd 13068	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
64		rpdivcl 13053	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
65	62, 63, 64	syl2an 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
66	3, 65	sselid 3977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
67	66, 12	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
68		flle 13819	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
69	66, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
70	67, 66, 69	abssubge0d 15436	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))
71		fracle1 13823	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
72	66, 71	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
73	70, 72	eqbrtrd 5175	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ≤ 1)
74		mule1 27176	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
75	54, 74	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
76	58, 50, 59, 50, 60, 61, 73, 75	lemul12ad 12208	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ (1 · 1))
77		1t1e1 12426	. . . . . . . . . . . . . . . 16 ⊢ (1 · 1) = 1
78	76, 77	breqtrdi 5194	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ 1)
79	57, 78	eqbrtrd 5175	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 1)
80	42, 44, 50, 79	fsumle 15803	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))1)
81		1cnd 11259	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ ℂ)
82		fsumconst 15794	. . . . . . . . . . . . . . 15 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((♯‘(1...(⌊‘𝑥))) · 1))
83	42, 81, 82	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((♯‘(1...(⌊‘𝑥))) · 1))
84		flge1nn 13841	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
85	7, 84	sylan 578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
86	85	nnnn0d 12584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
87		hashfz1 14363	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
88	86, 87	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
89	88	oveq1d 7439	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((♯‘(1...(⌊‘𝑥))) · 1) = ((⌊‘𝑥) · 1))
90	49	recnd 11292	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℂ)
91	90	mulridd 11281	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((⌊‘𝑥) · 1) = (⌊‘𝑥))
92	83, 89, 91	3eqtrd 2770	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = (⌊‘𝑥))
93	80, 92	breqtrd 5179	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (⌊‘𝑥))
94		flle 13819	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
95	46, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ≤ 𝑥)
96	45, 49, 46, 93, 95	letrd 11421	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
97	41, 45, 46, 47, 96	letrd 11421	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
98	32	mulridd 11281	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · 1) = 𝑥)
99	97, 98	breqtrrd 5181	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1))
100		1red 11265	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ ℝ)
101	41, 100, 62	ledivmuld 13123	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1 ↔ (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1)))
102	99, 101	mpbird 256	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1)
103	40, 102	eqbrtrd 5175	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
104	103	adantl 480	. . . . . 6 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
105	30, 25, 1, 1, 104	elo1d 15538	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1))
106		ax-1cn 11216	. . . . . . 7 ⊢ 1 ∈ ℂ
107		divrcnv 15856	. . . . . . 7 ⊢ (1 ∈ ℂ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0)
108	106, 107	ax-mp 5	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0
109		rlimo1 15619	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0 → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1))
110	108, 109	mp1i 13	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1))
111		o1add 15616	. . . . 5 ⊢ (((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))) ∈ 𝑂(1))
112	105, 110, 111	syl2anc 582	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))) ∈ 𝑂(1))
113	29, 112	eqeltrrd 2827	. . 3 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
114		ovexd 7459	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V)
115	18	zred 12718	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
116	115, 16	nndivred 12318	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
117	116	recnd 11292	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
118	6, 117	fsumcl 15737	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
119	118	adantl 480	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
120	118	adantr 479	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
121	120	abscld 15441	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ)
122	117	adantlr 713	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
123	42, 32, 122	fsummulc2 15788	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
124	14, 19	mulcld 11284	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
125	124	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
126	42, 43, 125	fsumadd 15744	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
127	11	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
128	14	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
129	127, 128	npcand 11625	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) = (𝑥 / 𝑛))
130	129	oveq1d 7439	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((𝑥 / 𝑛) · (μ‘𝑛)))
131	51, 128, 56	adddird 11289	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
132	32	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
133	54	nnrpd 13068	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
134		rpcnne0 13046	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
135	133, 134	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
136		div23 11942	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = ((𝑥 / 𝑛) · (μ‘𝑛)))
137		divass 11941	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = (𝑥 · ((μ‘𝑛) / 𝑛)))
138	136, 137	eqtr3d 2768	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
139	132, 56, 135, 138	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
140	130, 131, 139	3eqtr3d 2774	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (𝑥 · ((μ‘𝑛) / 𝑛)))
141	140	sumeq2dv 15707	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
142		eqidd 2727	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → (μ‘𝑛) = (μ‘𝑛))
143		ssrab2 4076	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ
144		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})
145	143, 144	sselid 3977	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ)
146	145, 17	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ)
147	146	zcnd 12719	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℂ)
148	142, 46, 147	dvdsflsumcom 27216	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛))
149	147	3impb 1112	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (μ‘𝑛) ∈ ℂ)
150	149	mulridd 11281	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((μ‘𝑛) · 1) = (μ‘𝑛))
151	150	2sumeq2dv 15709	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛))
152		eqidd 2727	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → 1 = 1)
153		nnuz 12917	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
154	85, 153	eleqtrdi 2836	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ (ℤ_≥‘1))
155		eluzfz1 13562	. . . . . . . . . . . . . . 15 ⊢ ((⌊‘𝑥) ∈ (ℤ_≥‘1) → 1 ∈ (1...(⌊‘𝑥)))
156	154, 155	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ (1...(⌊‘𝑥)))
157		1cnd 11259	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
158	152, 42, 53, 156, 157	musumsum 27220	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = 1)
159	151, 158	eqtr3d 2768	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = 1)
160		fzfid 13993	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
161		fsumconst 15794	. . . . . . . . . . . . . . 15 ⊢ (((1...(⌊‘(𝑥 / 𝑛))) ∈ Fin ∧ (μ‘𝑛) ∈ ℂ) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
162	160, 56, 161	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
163		rprege0 13043	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → ((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)))
164		flge0nn0 13840	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)) → (⌊‘(𝑥 / 𝑛)) ∈ ℕ₀)
165		hashfz1 14363	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘(𝑥 / 𝑛)) ∈ ℕ₀ → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
166	65, 163, 164, 165	4syl 19	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
167	166	oveq1d 7439	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
168	162, 167	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
169	168	sumeq2dv 15707	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
170	148, 159, 169	3eqtr3rd 2775	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) = 1)
171	170	oveq2d 7440	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
172	126, 141, 171	3eqtr3d 2774	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
173	123, 172	eqtrd 2766	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
174	173	oveq1d 7439	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥))
175	120, 32, 33	divcan3d 12046	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛))
176		rpcnne0 13046	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
177	176	adantr 479	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
178		divdir 11948	. . . . . . . 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 2774	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
181	180	fveq2d 6905	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
182	121, 181	eqled 11367	. . . 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 15657	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1))
185	184	mptru 1541	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ∧ wa 394 ∧ w3a 1084 = wceq 1534 ⊤wtru 1535 ∈ wcel 2099 ≠ wne 2930 {crab 3419 Vcvv 3462 ⊆ wss 3947 class class class wbr 5153 ↦ cmpt 5236 ‘cfv 6554 (class class class)co 7424 ∘_f cof 7688 Fincfn 8974 ℂcc 11156 ℝcr 11157 0cc0 11158 1c1 11159 + caddc 11161 · cmul 11163 ≤ cle 11299 − cmin 11494 / cdiv 11921 ℕcn 12264 ℕ₀cn0 12524 ℤcz 12610 ℤ_≥cuz 12874 ℝ⁺crp 13028 ...cfz 13538 ⌊cfl 13810 ♯chash 14347 abscabs 15239 ⇝_𝑟 crli 15487 𝑂(1)co1 15488 Σcsu 15690 ∥ cdvds 16256 μcmu 27123

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-inf2 9684 ax-cnex 11214 ax-resscn 11215 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-addrcl 11219 ax-mulcl 11220 ax-mulrcl 11221 ax-mulcom 11222 ax-addass 11223 ax-mulass 11224 ax-distr 11225 ax-i2m1 11226 ax-1ne0 11227 ax-1rid 11228 ax-rnegex 11229 ax-rrecex 11230 ax-cnre 11231 ax-pre-lttri 11232 ax-pre-lttrn 11233 ax-pre-ltadd 11234 ax-pre-mulgt0 11235 ax-pre-sup 11236

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-int 4955 df-iun 5003 df-disj 5119 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-se 5638 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-isom 6563 df-riota 7380 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7690 df-om 7877 df-1st 8003 df-2nd 8004 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-1o 8496 df-2o 8497 df-oadd 8500 df-er 8734 df-map 8857 df-pm 8858 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-sup 9485 df-inf 9486 df-oi 9553 df-dju 9944 df-card 9982 df-pnf 11300 df-mnf 11301 df-xr 11302 df-ltxr 11303 df-le 11304 df-sub 11496 df-neg 11497 df-div 11922 df-nn 12265 df-2 12327 df-3 12328 df-n0 12525 df-xnn0 12597 df-z 12611 df-uz 12875 df-q 12985 df-rp 13029 df-ico 13384 df-fz 13539 df-fzo 13682 df-fl 13812 df-mod 13890 df-seq 14022 df-exp 14082 df-fac 14291 df-bc 14320 df-hash 14348 df-cj 15104 df-re 15105 df-im 15106 df-sqrt 15240 df-abs 15241 df-clim 15490 df-rlim 15491 df-o1 15492 df-lo1 15493 df-sum 15691 df-dvds 16257 df-gcd 16495 df-prm 16673 df-pc 16839 df-mu 27129

This theorem is referenced by: mulogsumlem 27560 mulog2sumlem3 27565 selberglem1 27574

W3C validator