mulogsumlem

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

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) \in Fin$
2		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
3	2	adantl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
4		mucl	$⊢ n \in ℕ \to μ (n) \in ℤ$
5	3 4	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
6	5	zred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
7	6 3	nndivred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℝ$
8	7	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℂ$
9	1 8	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in ℂ$
10	9	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in ℂ$
11		emre	$⊢ γ \in ℝ$
12	11	recni	$⊢ γ \in ℂ$
13	12	a1i	$⊢ (⊤ \land x \in ℝ^{+}) \to γ \in ℂ$
14		mudivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1)$
15	14	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1)$
16		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
17		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land γ \in ℂ) \to (x \in ℝ^{+} ⟼ γ) \in 𝑂 (1)$
18	16 12 17	mp2an	$⊢ (x \in ℝ^{+} ⟼ γ) \in 𝑂 (1)$
19	18	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ γ) \in 𝑂 (1)$
20	10 13 15 19	o1mul2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ) \in 𝑂 (1)$
21		fzfid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
22		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
23	22	adantl	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
24	23	nnrecred	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{1}{m} \in ℝ$
25	21 24	fsumrecl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \in ℝ$
26	2	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
27		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
28	26 27	sylan2	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
29	28	relogcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
30	25 29	resubcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) \in ℝ$
31	7 30	remulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in ℝ$
32	1 31	fsumrecl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in ℝ$
33	32	recnd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in ℂ$
34	33	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in ℂ$
35		mulcl	$⊢ (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in ℂ \land γ \in ℂ) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ \in ℂ$
36	9 12 35	sylancl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ \in ℂ$
37	36	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ \in ℂ$
38		nnrecre	$⊢ m \in ℕ \to \frac{1}{m} \in ℝ$
39	38	recnd	$⊢ m \in ℕ \to \frac{1}{m} \in ℂ$
40	23 39	syl	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{1}{m} \in ℂ$
41	21 40	fsumcl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \in ℂ$
42	29	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
43	41 42	subcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) \in ℂ$
44	8 43	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in ℂ$
45		mulcl	$⊢ (\frac{μ (n)}{n} \in ℂ \land γ \in ℂ) \to (\frac{μ (n)}{n}) γ \in ℂ$
46	8 12 45	sylancl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) γ \in ℂ$
47	1 44 46	fsumsub	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - (\frac{μ (n)}{n}) γ) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ$
48	12	a1i	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to γ \in ℂ$
49	41 42 48	subsub4d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) - γ = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)$
50	49	oveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) - γ) = (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))$
51	8 43 48	subdid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) - γ) = (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - (\frac{μ (n)}{n}) γ$
52	50 51	eqtr3d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)) = (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - (\frac{μ (n)}{n}) γ$
53	52	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)) = \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - (\frac{μ (n)}{n}) γ)$
54	12	a1i	$⊢ x \in ℝ^{+} \to γ \in ℂ$
55	1 54 8	fsummulc1	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ$
56	55	oveq2d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ$
57	47 53 56	3eqtr4d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ$
58	57	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ)$
59	16	a1i	$⊢ ⊤ \to ℝ^{+} \subseteq ℝ$
60	42 48	addcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) + γ \in ℂ$
61	41 60	subcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ) \in ℂ$
62	8 61	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)) \in ℂ$
63	1 62	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)) \in ℂ$
64	63	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)) \in ℂ$
65		1red	$⊢ ⊤ \to 1 \in ℝ$
66	63	abscld	$⊢ x \in ℝ^{+} \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \in ℝ$
67	62	abscld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \in ℝ$
68	1 67	fsumrecl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \|(\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \in ℝ$
69		1red	$⊢ x \in ℝ^{+} \to 1 \in ℝ$
70	1 62	fsumabs	$⊢ x \in ℝ^{+} \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \leq \sum_{n = 1}^{⌊x⌋} \|(\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\|$
71		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
72		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
73	71 72	syl	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℕ_{0}$
74	73	nn0red	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℝ$
75		rerpdivcl	$⊢ (⌊x⌋ \in ℝ \land x \in ℝ^{+}) \to \frac{⌊x⌋}{x} \in ℝ$
76	74 75	mpancom	$⊢ x \in ℝ^{+} \to \frac{⌊x⌋}{x} \in ℝ$
77		rpreccl	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℝ^{+}$
78	77	adantr	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{x} \in ℝ^{+}$
79	78	rpred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{x} \in ℝ$
80	8	abscld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|\frac{μ (n)}{n}\| \in ℝ$
81	3	nnrecred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℝ$
82	61	abscld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)\| \in ℝ$
83		id	$⊢ x \in ℝ^{+} \to x \in ℝ^{+}$
84		rpdivcl	$⊢ (n \in ℝ^{+} \land x \in ℝ^{+}) \to \frac{n}{x} \in ℝ^{+}$
85	26 83 84	syl2anr	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{n}{x} \in ℝ^{+}$
86	85	rpred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{n}{x} \in ℝ$
87	8	absge0d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|\frac{μ (n)}{n}\|$
88	61	absge0d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)\|$
89	6	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℂ$
90	3	nncnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
91	3	nnne0d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
92	89 90 91	absdivd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|\frac{μ (n)}{n}\| = \frac{\|μ (n)\|}{\|n\|}$
93	3	nnrpd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
94		rprege0	$⊢ n \in ℝ^{+} \to (n \in ℝ \land 0 \leq n)$
95	93 94	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (n \in ℝ \land 0 \leq n)$
96		absid	$⊢ (n \in ℝ \land 0 \leq n) \to \|n\| = n$
97	95 96	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|n\| = n$
98	97	oveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{\|μ (n)\|}{\|n\|} = \frac{\|μ (n)\|}{n}$
99	92 98	eqtrd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|\frac{μ (n)}{n}\| = \frac{\|μ (n)\|}{n}$
100	89	abscld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \in ℝ$
101		1red	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
102		mule1	$⊢ n \in ℕ \to \|μ (n)\| \leq 1$
103	3 102	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \leq 1$
104	100 101 93 103	lediv1dd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{\|μ (n)\|}{n} \leq \frac{1}{n}$
105	99 104	eqbrtrd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|\frac{μ (n)}{n}\| \leq \frac{1}{n}$
106		harmonicbnd4	$⊢ \frac{x}{n} \in ℝ^{+} \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)\| \leq \frac{1}{\frac{x}{n}}$
107	28 106	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)\| \leq \frac{1}{\frac{x}{n}}$
108		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
109	108	adantr	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (x \in ℂ \land x \neq 0)$
110		rpcnne0	$⊢ n \in ℝ^{+} \to (n \in ℂ \land n \neq 0)$
111	93 110	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (n \in ℂ \land n \neq 0)$
112		recdiv	$⊢ ((x \in ℂ \land x \neq 0) \land (n \in ℂ \land n \neq 0)) \to \frac{1}{\frac{x}{n}} = \frac{n}{x}$
113	109 111 112	syl2anc	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{\frac{x}{n}} = \frac{n}{x}$
114	107 113	breqtrd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)\| \leq \frac{n}{x}$
115	80 81 82 86 87 88 105 114	lemul12ad	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|\frac{μ (n)}{n}\| \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)\| \leq (\frac{1}{n}) (\frac{n}{x})$
116	8 61	absmuld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| = \|\frac{μ (n)}{n}\| \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ)\|$
117		1cnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
118		dmdcan	$⊢ ((n \in ℂ \land n \neq 0) \land (x \in ℂ \land x \neq 0) \land 1 \in ℂ) \to (\frac{n}{x}) (\frac{1}{n}) = \frac{1}{x}$
119	111 109 117 118	syl3anc	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{n}{x}) (\frac{1}{n}) = \frac{1}{x}$
120	85	rpcnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{n}{x} \in ℂ$
121	81	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℂ$
122	120 121	mulcomd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{n}{x}) (\frac{1}{n}) = (\frac{1}{n}) (\frac{n}{x})$
123	119 122	eqtr3d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{x} = (\frac{1}{n}) (\frac{n}{x})$
124	115 116 123	3brtr4d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \leq \frac{1}{x}$
125	1 67 79 124	fsumle	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \|(\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{1}{x})$
126		hashfz1	$⊢ ⌊x⌋ \in ℕ_{0} \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
127	73 126	syl	$⊢ x \in ℝ^{+} \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
128	127	oveq1d	$⊢ x \in ℝ^{+} \to \|(1 \dots ⌊x⌋)\| (\frac{1}{x}) = ⌊x⌋ (\frac{1}{x})$
129	77	rpcnd	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℂ$
130		fsumconst	$⊢ ((1 \dots ⌊x⌋) \in Fin \land \frac{1}{x} \in ℂ) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{x}) = \|(1 \dots ⌊x⌋)\| (\frac{1}{x})$
131	1 129 130	syl2anc	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{x}) = \|(1 \dots ⌊x⌋)\| (\frac{1}{x})$
132	73	nn0cnd	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℂ$
133		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
134		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
135	132 133 134	divrecd	$⊢ x \in ℝ^{+} \to \frac{⌊x⌋}{x} = ⌊x⌋ (\frac{1}{x})$
136	128 131 135	3eqtr4d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{x}) = \frac{⌊x⌋}{x}$
137	125 136	breqtrd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \|(\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \leq \frac{⌊x⌋}{x}$
138		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
139		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
140	138 139	syl	$⊢ x \in ℝ^{+} \to ⌊x⌋ \leq x$
141	133	mulridd	$⊢ x \in ℝ^{+} \to x \cdot 1 = x$
142	140 141	breqtrrd	$⊢ x \in ℝ^{+} \to ⌊x⌋ \leq x \cdot 1$
143		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
144	138 143	syl	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℝ$
145		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
146		ledivmul	$⊢ (⌊x⌋ \in ℝ \land 1 \in ℝ \land (x \in ℝ \land 0 < x)) \to (\frac{⌊x⌋}{x} \leq 1 \leftrightarrow ⌊x⌋ \leq x \cdot 1)$
147	144 69 145 146	syl3anc	$⊢ x \in ℝ^{+} \to (\frac{⌊x⌋}{x} \leq 1 \leftrightarrow ⌊x⌋ \leq x \cdot 1)$
148	142 147	mpbird	$⊢ x \in ℝ^{+} \to \frac{⌊x⌋}{x} \leq 1$
149	68 76 69 137 148	letrd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \|(\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \leq 1$
150	66 68 69 70 149	letrd	$⊢ x \in ℝ^{+} \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \leq 1$
151	150	ad2antrl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))\| \leq 1$
152	59 64 65 65 151	elo1d	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\log (\frac{x}{n}) + γ))) \in 𝑂 (1)$
153	58 152	eqeltrrid	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ) \in 𝑂 (1)$
154	34 37 153	o1dif	$⊢ ⊤ \to ((x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))) \in 𝑂 (1) \leftrightarrow (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) γ) \in 𝑂 (1))$
155	20 154	mpbird	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))) \in 𝑂 (1)$
156	155	mptru	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem mulogsumlem

Proof