mudivsum

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

		Ref	Expression
	Assertion	mudivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		1red	$⊢ ⊤ \to 1 \in ℝ$
2		reex	$⊢ ℝ \in V$
3		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
4	2 3	ssexi	$⊢ ℝ^{+} \in V$
5	4	a1i	$⊢ ⊤ \to ℝ^{+} \in V$
6		fzfid	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) \in Fin$
7		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
8		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
9		nndivre	$⊢ (x \in ℝ \land n \in ℕ) \to \frac{x}{n} \in ℝ$
10	7 8 9	syl2an	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
11	10	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℂ$
12		reflcl	$⊢ \frac{x}{n} \in ℝ \to ⌊\frac{x}{n}⌋ \in ℝ$
13	10 12	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{n}⌋ \in ℝ$
14	13	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{n}⌋ \in ℂ$
15	11 14	subcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{x}{n}) - ⌊\frac{x}{n}⌋ \in ℂ$
16	8	adantl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
17		mucl	$⊢ n \in ℕ \to μ (n) \in ℤ$
18	16 17	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
19	18	zcnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℂ$
20	15 19	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) \in ℂ$
21	6 20	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) \in ℂ$
22		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
23		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
24	21 22 23	divcld	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x} \in ℂ$
25	24	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x} \in ℂ$
26		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{1}{x} \in V$
27		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) = (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x})$
28		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) = (x \in ℝ^{+} ⟼ \frac{1}{x})$
29	5 25 26 27 28	offval2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) +_{f} (x \in ℝ^{+} ⟼ \frac{1}{x}) = (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x}))$
30	3	a1i	$⊢ ⊤ \to ℝ^{+} \subseteq ℝ$
31	21	adantr	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) \in ℂ$
32	22	adantr	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \in ℂ$
33	23	adantr	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \neq 0$
34	31 32 33	absdivd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\|}{\|x\|}$
35		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
36		absid	$⊢ (x \in ℝ \land 0 \leq x) \to \|x\| = x$
37	35 36	syl	$⊢ x \in ℝ^{+} \to \|x\| = x$
38	37	adantr	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|x\| = x$
39	38	oveq2d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \frac{\|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\|}{\|x\|} = \frac{\|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\|}{x}$
40	34 39	eqtrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\|}{x}$
41	31	abscld	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \in ℝ$
42		fzfid	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to (1 \dots ⌊x⌋) \in Fin$
43	20	adantlr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) \in ℂ$
44	43	abscld	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \in ℝ$
45	42 44	fsumrecl	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} \|((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \in ℝ$
46	7	adantr	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \in ℝ$
47	42 43	fsumabs	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \leq \sum_{n = 1}^{⌊x⌋} \|((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\|$
48		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
49	46 48	syl	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \in ℝ$
50		1red	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
51	15	adantlr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (\frac{x}{n}) - ⌊\frac{x}{n}⌋ \in ℂ$
52		fz1ssnn	$⊢ (1 \dots ⌊x⌋) \subseteq ℕ$
53	52	a1i	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to (1 \dots ⌊x⌋) \subseteq ℕ$
54	53	sselda	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
55	54 17	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
56	55	zcnd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℂ$
57	51 56	absmuld	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| = \|(\frac{x}{n}) - ⌊\frac{x}{n}⌋\| \|μ (n)\|$
58	51	abscld	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{x}{n}) - ⌊\frac{x}{n}⌋\| \in ℝ$
59	56	abscld	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \in ℝ$
60	51	absge0d	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|(\frac{x}{n}) - ⌊\frac{x}{n}⌋\|$
61	56	absge0d	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|μ (n)\|$
62		simpl	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \in ℝ^{+}$
63	8	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
64		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
65	62 63 64	syl2an	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
66	3 65	sselid	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
67	66 12	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{n}⌋ \in ℝ$
68		flle	$⊢ \frac{x}{n} \in ℝ \to ⌊\frac{x}{n}⌋ \leq \frac{x}{n}$
69	66 68	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{n}⌋ \leq \frac{x}{n}$
70	67 66 69	abssubge0d	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{x}{n}) - ⌊\frac{x}{n}⌋\| = (\frac{x}{n}) - ⌊\frac{x}{n}⌋$
71		fracle1	$⊢ \frac{x}{n} \in ℝ \to (\frac{x}{n}) - ⌊\frac{x}{n}⌋ \leq 1$
72	66 71	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (\frac{x}{n}) - ⌊\frac{x}{n}⌋ \leq 1$
73	70 72	eqbrtrd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{x}{n}) - ⌊\frac{x}{n}⌋\| \leq 1$
74		mule1	$⊢ n \in ℕ \to \|μ (n)\| \leq 1$
75	54 74	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \leq 1$
76	58 50 59 50 60 61 73 75	lemul12ad	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{x}{n}) - ⌊\frac{x}{n}⌋\| \|μ (n)\| \leq 1 \cdot 1$
77		1t1e1	$⊢ 1 \cdot 1 = 1$
78	76 77	breqtrdi	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{x}{n}) - ⌊\frac{x}{n}⌋\| \|μ (n)\| \leq 1$
79	57 78	eqbrtrd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \leq 1$
80	42 44 50 79	fsumle	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} \|((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \leq \sum_{n = 1}^{⌊x⌋} 1$
81		1cnd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to 1 \in ℂ$
82		fsumconst	$⊢ ((1 \dots ⌊x⌋) \in Fin \land 1 \in ℂ) \to \sum_{n = 1}^{⌊x⌋} 1 = \|(1 \dots ⌊x⌋)\| \cdot 1$
83	42 81 82	syl2anc	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} 1 = \|(1 \dots ⌊x⌋)\| \cdot 1$
84		flge1nn	$⊢ (x \in ℝ \land 1 \leq x) \to ⌊x⌋ \in ℕ$
85	7 84	sylan	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \in ℕ$
86	85	nnnn0d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \in ℕ_{0}$
87		hashfz1	$⊢ ⌊x⌋ \in ℕ_{0} \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
88	86 87	syl	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
89	88	oveq1d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|(1 \dots ⌊x⌋)\| \cdot 1 = ⌊x⌋ \cdot 1$
90	49	recnd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \in ℂ$
91	90	mulid1d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \cdot 1 = ⌊x⌋$
92	83 89 91	3eqtrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} 1 = ⌊x⌋$
93	80 92	breqtrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} \|((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \leq ⌊x⌋$
94		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
95	46 94	syl	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \leq x$
96	45 49 46 93 95	letrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} \|((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \leq x$
97	41 45 46 47 96	letrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \leq x$
98	32	mulid1d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \cdot 1 = x$
99	97 98	breqtrrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \leq x \cdot 1$
100		1red	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to 1 \in ℝ$
101	41 100 62	ledivmuld	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to (\frac{\|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\|}{x} \leq 1 \leftrightarrow \|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\| \leq x \cdot 1)$
102	99 101	mpbird	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \frac{\|\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)\|}{x} \leq 1$
103	40 102	eqbrtrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}\| \leq 1$
104	103	adantl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}\| \leq 1$
105	30 25 1 1 104	elo1d	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) \in 𝑂 (1)$
106		ax-1cn	$⊢ 1 \in ℂ$
107		divrcnv	$⊢ 1 \in ℂ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0$
108	106 107	ax-mp	$⊢ (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0$
109		rlimo1	$⊢ (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0 \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)$
110	108 109	mp1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)$
111		o1add	$⊢ ((x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) \in 𝑂 (1) \land (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)) \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) +_{f} (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)$
112	105 110 111	syl2anc	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) +_{f} (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)$
113	29 112	eqeltrrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x})) \in 𝑂 (1)$
114		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x}) \in V$
115	18	zred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
116	115 16	nndivred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℝ$
117	116	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℂ$
118	6 117	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in ℂ$
119	118	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in ℂ$
120	118	adantr	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in ℂ$
121	120	abscld	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})\| \in ℝ$
122	117	adantlr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℂ$
123	42 32 122	fsummulc2	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} x (\frac{μ (n)}{n})$
124	14 19	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{n}⌋ μ (n) \in ℂ$
125	124	adantlr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{n}⌋ μ (n) \in ℂ$
126	42 43 125	fsumadd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + ⌊\frac{x}{n}⌋ μ (n)) = \sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + \sum_{n = 1}^{⌊x⌋} ⌊\frac{x}{n}⌋ μ (n)$
127	11	adantlr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℂ$
128	14	adantlr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{n}⌋ \in ℂ$
129	127 128	npcand	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (\frac{x}{n}) - ⌊\frac{x}{n}⌋ + ⌊\frac{x}{n}⌋ = \frac{x}{n}$
130	129	oveq1d	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{x}{n}) - ⌊\frac{x}{n}⌋ + ⌊\frac{x}{n}⌋) μ (n) = (\frac{x}{n}) μ (n)$
131	51 128 56	adddird	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{x}{n}) - ⌊\frac{x}{n}⌋ + ⌊\frac{x}{n}⌋) μ (n) = ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + ⌊\frac{x}{n}⌋ μ (n)$
132	32	adantr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
133	54	nnrpd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
134		rpcnne0	$⊢ n \in ℝ^{+} \to (n \in ℂ \land n \neq 0)$
135	133 134	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (n \in ℂ \land n \neq 0)$
136		div23	$⊢ (x \in ℂ \land μ (n) \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{x μ (n)}{n} = (\frac{x}{n}) μ (n)$
137		divass	$⊢ (x \in ℂ \land μ (n) \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{x μ (n)}{n} = x (\frac{μ (n)}{n})$
138	136 137	eqtr3d	$⊢ (x \in ℂ \land μ (n) \in ℂ \land (n \in ℂ \land n \neq 0)) \to (\frac{x}{n}) μ (n) = x (\frac{μ (n)}{n})$
139	132 56 135 138	syl3anc	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (\frac{x}{n}) μ (n) = x (\frac{μ (n)}{n})$
140	130 131 139	3eqtr3d	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + ⌊\frac{x}{n}⌋ μ (n) = x (\frac{μ (n)}{n})$
141	140	sumeq2dv	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + ⌊\frac{x}{n}⌋ μ (n)) = \sum_{n = 1}^{⌊x⌋} x (\frac{μ (n)}{n})$
142		eqidd	$⊢ k = n m \to μ (n) = μ (n)$
143		ssrab2	$⊢ \{y \in ℕ \| y ∥ k\} \subseteq ℕ$
144		simprr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to n \in \{y \in ℕ \| y ∥ k\}$
145	143 144	sselid	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to n \in ℕ$
146	145 17	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) \in ℤ$
147	146	zcnd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) \in ℂ$
148	142 46 147	dvdsflsumcom	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n)$
149	147	3impb	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\}) \to μ (n) \in ℂ$
150	149	mulid1d	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\}) \to μ (n) \cdot 1 = μ (n)$
151	150	2sumeq2dv	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) \cdot 1 = \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n)$
152		eqidd	$⊢ k = 1 \to 1 = 1$
153		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
154	85 153	eleqtrdi	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \in ℤ_{\geq 1}$
155		eluzfz1	$⊢ ⌊x⌋ \in ℤ_{\geq 1} \to 1 \in (1 \dots ⌊x⌋)$
156	154 155	syl	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to 1 \in (1 \dots ⌊x⌋)$
157		1cnd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land k \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
158	152 42 53 156 157	musumsum	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) \cdot 1 = 1$
159	151 158	eqtr3d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) = 1$
160		fzfid	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
161		fsumconst	$⊢ ((1 \dots ⌊\frac{x}{n}⌋) \in Fin \land μ (n) \in ℂ) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) = \|(1 \dots ⌊\frac{x}{n}⌋)\| μ (n)$
162	160 56 161	syl2anc	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) = \|(1 \dots ⌊\frac{x}{n}⌋)\| μ (n)$
163		rprege0	$⊢ \frac{x}{n} \in ℝ^{+} \to (\frac{x}{n} \in ℝ \land 0 \leq \frac{x}{n})$
164		flge0nn0	$⊢ (\frac{x}{n} \in ℝ \land 0 \leq \frac{x}{n}) \to ⌊\frac{x}{n}⌋ \in ℕ_{0}$
165		hashfz1	$⊢ ⌊\frac{x}{n}⌋ \in ℕ_{0} \to \|(1 \dots ⌊\frac{x}{n}⌋)\| = ⌊\frac{x}{n}⌋$
166	65 163 164 165	4syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|(1 \dots ⌊\frac{x}{n}⌋)\| = ⌊\frac{x}{n}⌋$
167	166	oveq1d	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \|(1 \dots ⌊\frac{x}{n}⌋)\| μ (n) = ⌊\frac{x}{n}⌋ μ (n)$
168	162 167	eqtrd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) = ⌊\frac{x}{n}⌋ μ (n)$
169	168	sumeq2dv	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) = \sum_{n = 1}^{⌊x⌋} ⌊\frac{x}{n}⌋ μ (n)$
170	148 159 169	3eqtr3rd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} ⌊\frac{x}{n}⌋ μ (n) = 1$
171	170	oveq2d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + \sum_{n = 1}^{⌊x⌋} ⌊\frac{x}{n}⌋ μ (n) = \sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + 1$
172	126 141 171	3eqtr3d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} x (\frac{μ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + 1$
173	123 172	eqtrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + 1$
174	173	oveq1d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \frac{x \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})}{x} = \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + 1}{x}$
175	120 32 33	divcan3d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \frac{x \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})$
176		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
177	176	adantr	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to (x \in ℂ \land x \neq 0)$
178		divdir	$⊢ (\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) \in ℂ \land 1 \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + 1}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x})$
179	31 81 177 178	syl3anc	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n) + 1}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x})$
180	174 175 179	3eqtr3d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) = (\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x})$
181	180	fveq2d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})\| = \|(\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x})\|$
182	121 181	eqled	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})\| \leq \|(\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x})\|$
183	182	adantl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})\| \leq \|(\frac{\sum_{n = 1}^{⌊x⌋} ((\frac{x}{n}) - ⌊\frac{x}{n}⌋) μ (n)}{x}) + (\frac{1}{x})\|$
184	1 113 114 119 183	o1le	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1)$
185	184	mptru	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem mudivsum

Proof