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 26106

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 10642	. . 3 ⊢ (⊤ → 1 ∈ ℝ)
2		reex 10628	. . . . . . 7 ⊢ ℝ ∈ V
3		rpssre 12397	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℝ
4	2, 3	ssexi 5226	. . . . . 6 ⊢ ℝ⁺ ∈ V
5	4	a1i 11	. . . . 5 ⊢ (⊤ → ℝ⁺ ∈ V)
6		fzfid 13342	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (1...(⌊‘𝑥)) ∈ Fin)
7		rpre 12398	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
8		elfznn 12937	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
9		nndivre 11679	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ)
10	7, 8, 9	syl2an 597	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
11	10	recnd 10669	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
12		reflcl 13167	. . . . . . . . . . . 12 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
13	10, 12	syl 17	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
14	13	recnd 10669	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
15	11, 14	subcld 10997	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
16	8	adantl 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
17		mucl 25718	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
19	18	zcnd 12089	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
20	15, 19	mulcld 10661	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
21	6, 20	fsumcl 15090	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
22		rpcn 12400	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
23		rpne0 12406	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
24	21, 22, 23	divcld 11416	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
25	24	adantl 484	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
26		ovexd 7191	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (1 / 𝑥) ∈ V)
27		eqidd 2822	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)))
28		eqidd 2822	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)))
29	5, 25, 26, 27, 28	offval2 7426	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
30	3	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ⁺ ⊆ ℝ)
31	21	adantr 483	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
32	22	adantr 483	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℂ)
33	23	adantr 483	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ≠ 0)
34	31, 32, 33	absdivd 14815	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)))
35		rprege0 12405	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
36		absid 14656	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘𝑥) = 𝑥)
38	37	adantr 483	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
39	38	oveq2d 7172	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
40	34, 39	eqtrd 2856	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
41	31	abscld 14796	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
42		fzfid 13342	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ∈ Fin)
43	20	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
44	43	abscld 14796	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
45	42, 44	fsumrecl 15091	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
46	7	adantr 483	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ)
47	42, 43	fsumabs 15156	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))))
48		reflcl 13167	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
49	46, 48	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℝ)
50		1red 10642	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
51	15	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
52		fz1ssnn 12939	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...(⌊‘𝑥)) ⊆ ℕ
53	52	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ⊆ ℕ)
54	53	sselda 3967	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
55	54, 17	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
56	55	zcnd 12089	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
57	51, 56	absmuld 14814	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) = ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))))
58	51	abscld 14796	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ∈ ℝ)
59	56	abscld 14796	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
60	51	absge0d 14804	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))))
61	56	absge0d 14804	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(μ‘𝑛)))
62		simpl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ⁺)
63	8	nnrpd 12430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
64		rpdivcl 12415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
65	62, 63, 64	syl2an 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
66	3, 65	sseldi 3965	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
67	66, 12	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
68		flle 13170	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
69	66, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
70	67, 66, 69	abssubge0d 14791	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))
71		fracle1 13174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
72	66, 71	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
73	70, 72	eqbrtrd 5088	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ≤ 1)
74		mule1 25725	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
75	54, 74	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
76	58, 50, 59, 50, 60, 61, 73, 75	lemul12ad 11582	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ (1 · 1))
77		1t1e1 11800	. . . . . . . . . . . . . . . 16 ⊢ (1 · 1) = 1
78	76, 77	breqtrdi 5107	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ 1)
79	57, 78	eqbrtrd 5088	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 1)
80	42, 44, 50, 79	fsumle 15154	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))1)
81		1cnd 10636	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ ℂ)
82		fsumconst 15145	. . . . . . . . . . . . . . 15 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((♯‘(1...(⌊‘𝑥))) · 1))
83	42, 81, 82	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((♯‘(1...(⌊‘𝑥))) · 1))
84		flge1nn 13192	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
85	7, 84	sylan 582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
86	85	nnnn0d 11956	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
87		hashfz1 13707	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
88	86, 87	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
89	88	oveq1d 7171	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((♯‘(1...(⌊‘𝑥))) · 1) = ((⌊‘𝑥) · 1))
90	49	recnd 10669	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℂ)
91	90	mulid1d 10658	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((⌊‘𝑥) · 1) = (⌊‘𝑥))
92	83, 89, 91	3eqtrd 2860	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = (⌊‘𝑥))
93	80, 92	breqtrd 5092	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (⌊‘𝑥))
94		flle 13170	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
95	46, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ≤ 𝑥)
96	45, 49, 46, 93, 95	letrd 10797	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
97	41, 45, 46, 47, 96	letrd 10797	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
98	32	mulid1d 10658	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · 1) = 𝑥)
99	97, 98	breqtrrd 5094	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1))
100		1red 10642	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ ℝ)
101	41, 100, 62	ledivmuld 12485	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1 ↔ (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1)))
102	99, 101	mpbird 259	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1)
103	40, 102	eqbrtrd 5088	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
104	103	adantl 484	. . . . . 6 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
105	30, 25, 1, 1, 104	elo1d 14893	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1))
106		ax-1cn 10595	. . . . . . 7 ⊢ 1 ∈ ℂ
107		divrcnv 15207	. . . . . . 7 ⊢ (1 ∈ ℂ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0)
108	106, 107	ax-mp 5	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0
109		rlimo1 14973	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ⇝_𝑟 0 → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1))
110	108, 109	mp1i 13	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1))
111		o1add 14970	. . . . 5 ⊢ (((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))) ∈ 𝑂(1))
112	105, 110, 111	syl2anc 586	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))) ∈ 𝑂(1))
113	29, 112	eqeltrrd 2914	. . 3 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
114		ovexd 7191	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V)
115	18	zred 12088	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
116	115, 16	nndivred 11692	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
117	116	recnd 10669	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
118	6, 117	fsumcl 15090	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
119	118	adantl 484	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
120	118	adantr 483	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
121	120	abscld 14796	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ)
122	117	adantlr 713	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
123	42, 32, 122	fsummulc2 15139	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
124	14, 19	mulcld 10661	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
125	124	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
126	42, 43, 125	fsumadd 15096	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
127	11	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
128	14	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
129	127, 128	npcand 11001	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) = (𝑥 / 𝑛))
130	129	oveq1d 7171	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((𝑥 / 𝑛) · (μ‘𝑛)))
131	51, 128, 56	adddird 10666	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
132	32	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
133	54	nnrpd 12430	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
134		rpcnne0 12408	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
135	133, 134	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
136		div23 11317	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = ((𝑥 / 𝑛) · (μ‘𝑛)))
137		divass 11316	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = (𝑥 · ((μ‘𝑛) / 𝑛)))
138	136, 137	eqtr3d 2858	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
139	132, 56, 135, 138	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
140	130, 131, 139	3eqtr3d 2864	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (𝑥 · ((μ‘𝑛) / 𝑛)))
141	140	sumeq2dv 15060	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
142		eqidd 2822	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → (μ‘𝑛) = (μ‘𝑛))
143		ssrab2 4056	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ
144		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})
145	143, 144	sseldi 3965	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ)
146	145, 17	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ)
147	146	zcnd 12089	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℂ)
148	142, 46, 147	dvdsflsumcom 25765	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛))
149	147	3impb 1111	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (μ‘𝑛) ∈ ℂ)
150	149	mulid1d 10658	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((μ‘𝑛) · 1) = (μ‘𝑛))
151	150	2sumeq2dv 15062	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛))
152		eqidd 2822	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → 1 = 1)
153		nnuz 12282	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
154	85, 153	eleqtrdi 2923	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ (ℤ_≥‘1))
155		eluzfz1 12915	. . . . . . . . . . . . . . 15 ⊢ ((⌊‘𝑥) ∈ (ℤ_≥‘1) → 1 ∈ (1...(⌊‘𝑥)))
156	154, 155	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → 1 ∈ (1...(⌊‘𝑥)))
157		1cnd 10636	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
158	152, 42, 53, 156, 157	musumsum 25769	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = 1)
159	151, 158	eqtr3d 2858	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = 1)
160		fzfid 13342	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
161		fsumconst 15145	. . . . . . . . . . . . . . 15 ⊢ (((1...(⌊‘(𝑥 / 𝑛))) ∈ Fin ∧ (μ‘𝑛) ∈ ℂ) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
162	160, 56, 161	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
163		rprege0 12405	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → ((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)))
164		flge0nn0 13191	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)) → (⌊‘(𝑥 / 𝑛)) ∈ ℕ₀)
165		hashfz1 13707	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘(𝑥 / 𝑛)) ∈ ℕ₀ → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
166	65, 163, 164, 165	4syl 19	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
167	166	oveq1d 7171	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
168	162, 167	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
169	168	sumeq2dv 15060	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
170	148, 159, 169	3eqtr3rd 2865	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) = 1)
171	170	oveq2d 7172	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
172	126, 141, 171	3eqtr3d 2864	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
173	123, 172	eqtrd 2856	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
174	173	oveq1d 7171	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥))
175	120, 32, 33	divcan3d 11421	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛))
176		rpcnne0 12408	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
177	176	adantr 483	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
178		divdir 11323	. . . . . . . 8 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
179	31, 81, 177, 178	syl3anc 1367	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
180	174, 175, 179	3eqtr3d 2864	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
181	180	fveq2d 6674	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
182	121, 181	eqled 10743	. . . 4 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
183	182	adantl 484	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
184	1, 113, 114, 119, 183	o1le 15009	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1))
185	184	mptru 1544	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ∧ wa 398 ∧ w3a 1083 = wceq 1537 ⊤wtru 1538 ∈ wcel 2114 ≠ wne 3016 {crab 3142 Vcvv 3494 ⊆ wss 3936 class class class wbr 5066 ↦ cmpt 5146 ‘cfv 6355 (class class class)co 7156 ∘_f cof 7407 Fincfn 8509 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 ≤ cle 10676 − cmin 10870 / cdiv 11297 ℕcn 11638 ℕ₀cn0 11898 ℤcz 11982 ℤ_≥cuz 12244 ℝ⁺crp 12390 ...cfz 12893 ⌊cfl 13161 ♯chash 13691 abscabs 14593 ⇝_𝑟 crli 14842 𝑂(1)co1 14843 Σcsu 15042 ∥ cdvds 15607 μcmu 25672

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-disj 5032 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-sup 8906 df-inf 8907 df-oi 8974 df-dju 9330 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-n0 11899 df-xnn0 11969 df-z 11983 df-uz 12245 df-q 12350 df-rp 12391 df-ico 12745 df-fz 12894 df-fzo 13035 df-fl 13163 df-mod 13239 df-seq 13371 df-exp 13431 df-fac 13635 df-bc 13664 df-hash 13692 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-clim 14845 df-rlim 14846 df-o1 14847 df-lo1 14848 df-sum 15043 df-dvds 15608 df-gcd 15844 df-prm 16016 df-pc 16174 df-mu 25678

This theorem is referenced by: mulogsumlem 26107 mulog2sumlem3 26112 selberglem1 26121

W3C validator