2vmadivsumlem

	Ref	Expression
Hypotheses	2vmadivsum.1	$⊢ φ \to A \in ℝ^{+}$
	2vmadivsum.2	$⊢ φ \to \forall y \in [1, +∞) \|\sum_{i = 1}^{⌊y⌋} (\frac{Λ (i)}{i}) - \log y\| \leq A$
Assertion	2vmadivsumlem	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		2vmadivsum.1	$⊢ φ \to A \in ℝ^{+}$
2		2vmadivsum.2	$⊢ φ \to \forall y \in [1, +∞) \|\sum_{i = 1}^{⌊y⌋} (\frac{Λ (i)}{i}) - \log y\| \leq A$
3		vmalogdivsum2	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
4	3	a1i	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
5		fzfid	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
6		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
7	6	adantl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
8		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
9	7 8	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
10	9 7	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
11		fzfid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
12		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
13	12	adantl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
14		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
15	13 14	syl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \in ℝ$
16	15 13	nndivred	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{Λ (m)}{m} \in ℝ$
17	11 16	fsumrecl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℝ$
18	10 17	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℝ$
19	5 18	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℝ$
20		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
21	20	adantl	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ$
22		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
23	22	adantl	$⊢ (φ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
24	23	simpld	$⊢ (φ \land x \in (1, +∞)) \to 1 < x$
25	21 24	rplogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
26	19 25	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x} \in ℝ$
27		1rp	$⊢ 1 \in ℝ^{+}$
28	27	a1i	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
29		1red	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ$
30	29 21 24	ltled	$⊢ (φ \land x \in (1, +∞)) \to 1 \leq x$
31	21 28 30	rpgecld	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ^{+}$
32	31	relogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ$
33	32	rehalfcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℝ$
34	26 33	resubcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}) \in ℝ$
35	34	recnd	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}) \in ℂ$
36	31	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
37	7	nnrpd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
38	36 37	rpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
39	38	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
40	10 39	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℝ$
41	5 40	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℝ$
42	41 25	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} \in ℝ$
43	42 33	resubcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}) \in ℝ$
44	43	recnd	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}) \in ℂ$
45	19	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℂ$
46	41	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
47	32	recnd	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℂ$
48	25	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to \log x \neq 0$
49	45 46 47 48	divsubdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x})$
50	10	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
51	17	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℂ$
52	39	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
53	50 51 52	subdid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})) = (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
54	53	sumeq2dv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n}))$
55	18	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℂ$
56	40	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
57	5 55 56	fsumsub	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
58	54 57	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
59	58	oveq1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x} = \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}$
60	26	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x} \in ℂ$
61	42	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} \in ℂ$
62	33	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℂ$
63	60 61 62	nnncan2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}) - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x})$
64	49 59 63	3eqtr4d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x} = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}) - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}))$
65	64	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x}) = (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}) - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})))$
66		1red	$⊢ φ \to 1 \in ℝ$
67	5 10	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℝ$
68	67 25	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x} \in ℝ$
69	1	rpred	$⊢ φ \to A \in ℝ$
70	69	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ$
71		ioossre	$⊢ (1, +∞) \subseteq ℝ$
72		1cnd	$⊢ φ \to 1 \in ℂ$
73		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 1 \in ℂ) \to (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
74	71 72 73	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
75	68	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x} \in ℂ$
76		1cnd	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℂ$
77	67	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
78	77 47 47 48	divsubdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x}{\log x} = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - (\frac{\log x}{\log x})$
79	77 47	subcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℂ$
80	79 47 48	divrecd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x}{\log x} = (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x})$
81	47 48	dividd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x}{\log x} = 1$
82	81	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - (\frac{\log x}{\log x}) = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1$
83	78 80 82	3eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x}) = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1$
84	83	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x})) = (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1)$
85	67 32	resubcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℝ$
86	29 25	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{1}{\log x} \in ℝ$
87	31	ex	$⊢ φ \to (x \in (1, +∞) \to x \in ℝ^{+})$
88	87	ssrdv	$⊢ φ \to (1, +∞) \subseteq ℝ^{+}$
89		vmadivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
90	89	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
91	88 90	o1res2	$⊢ φ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
92		divlogrlim	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0$
93		rlimo1	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0 \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
94	92 93	mp1i	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
95	85 86 91 94	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x})) \in 𝑂 (1)$
96	84 95	eqeltrrd	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1) \in 𝑂 (1)$
97	75 76 96	o1dif	$⊢ φ \to ((x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ 1) \in 𝑂 (1))$
98	74 97	mpbird	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) \in 𝑂 (1)$
99	69	recnd	$⊢ φ \to A \in ℂ$
100		o1const	$⊢ ((1, +∞) \subseteq ℝ \land A \in ℂ) \to (x \in (1, +∞) ⟼ A) \in 𝑂 (1)$
101	71 99 100	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ A) \in 𝑂 (1)$
102	68 70 98 101	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A) \in 𝑂 (1)$
103	68 70	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A \in ℝ$
104	17 39	resubcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}) \in ℝ$
105	10 104	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})) \in ℝ$
106	5 105	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})) \in ℝ$
107	106	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})) \in ℂ$
108	107 47 48	divcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x} \in ℂ$
109	107	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| \in ℝ$
110	67 70	remulcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A \in ℝ$
111	105	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})) \in ℂ$
112	111	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| \in ℝ$
113	5 112	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|(\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| \in ℝ$
114	5 111	fsumabs	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} \|(\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\|$
115	70	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℝ$
116	10 115	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) A \in ℝ$
117	104	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}) \in ℂ$
118	50 117	absmuld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| = \|\frac{Λ (n)}{n}\| \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\|$
119		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
120	7 119	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n)$
121	9 37 120	divge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{Λ (n)}{n}$
122	10 121	absidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{Λ (n)}{n}\| = \frac{Λ (n)}{n}$
123	122	oveq1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{Λ (n)}{n}\| \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\| = (\frac{Λ (n)}{n}) \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\|$
124	118 123	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| = (\frac{Λ (n)}{n}) \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\|$
125	117	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\| \in ℝ$
126		fveq2	$⊢ i = m \to Λ (i) = Λ (m)$
127		id	$⊢ i = m \to i = m$
128	126 127	oveq12d	$⊢ i = m \to \frac{Λ (i)}{i} = \frac{Λ (m)}{m}$
129	128	cbvsumv	$⊢ \sum_{i = 1}^{⌊y⌋} (\frac{Λ (i)}{i}) = \sum_{m = 1}^{⌊y⌋} (\frac{Λ (m)}{m})$
130		fveq2	$⊢ y = \frac{x}{n} \to ⌊y⌋ = ⌊\frac{x}{n}⌋$
131	130	oveq2d	$⊢ y = \frac{x}{n} \to (1 \dots ⌊y⌋) = (1 \dots ⌊\frac{x}{n}⌋)$
132	131	sumeq1d	$⊢ y = \frac{x}{n} \to \sum_{m = 1}^{⌊y⌋} (\frac{Λ (m)}{m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
133	129 132	eqtrid	$⊢ y = \frac{x}{n} \to \sum_{i = 1}^{⌊y⌋} (\frac{Λ (i)}{i}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
134		fveq2	$⊢ y = \frac{x}{n} \to \log y = \log (\frac{x}{n})$
135	133 134	oveq12d	$⊢ y = \frac{x}{n} \to \sum_{i = 1}^{⌊y⌋} (\frac{Λ (i)}{i}) - \log y = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})$
136	135	fveq2d	$⊢ y = \frac{x}{n} \to \|\sum_{i = 1}^{⌊y⌋} (\frac{Λ (i)}{i}) - \log y\| = \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\|$
137	136	breq1d	$⊢ y = \frac{x}{n} \to (\|\sum_{i = 1}^{⌊y⌋} (\frac{Λ (i)}{i}) - \log y\| \leq A \leftrightarrow \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\| \leq A)$
138	2	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \forall y \in [1, +∞) \|\sum_{i = 1}^{⌊y⌋} (\frac{Λ (i)}{i}) - \log y\| \leq A$
139	38	rpred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
140	7	nncnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
141	140	mullidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 n = n$
142		fznnfl	$⊢ x \in ℝ \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
143	21 142	syl	$⊢ (φ \land x \in (1, +∞)) \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
144	143	simplbda	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \leq x$
145	141 144	eqbrtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 n \leq x$
146		1red	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
147	21	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
148	146 147 37	lemuldivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 n \leq x \leftrightarrow 1 \leq \frac{x}{n})$
149	145 148	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x}{n}$
150		1re	$⊢ 1 \in ℝ$
151		elicopnf	$⊢ 1 \in ℝ \to (\frac{x}{n} \in [1, +∞) \leftrightarrow (\frac{x}{n} \in ℝ \land 1 \leq \frac{x}{n}))$
152	150 151	ax-mp	$⊢ \frac{x}{n} \in [1, +∞) \leftrightarrow (\frac{x}{n} \in ℝ \land 1 \leq \frac{x}{n})$
153	139 149 152	sylanbrc	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in [1, +∞)$
154	137 138 153	rspcdva	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\| \leq A$
155	125 115 10 121 154	lemul2ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n})\| \leq (\frac{Λ (n)}{n}) A$
156	124 155	eqbrtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| \leq (\frac{Λ (n)}{n}) A$
157	5 112 116 156	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|(\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A$
158	99	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℂ$
159	5 158 50	fsummulc1	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A$
160	157 159	breqtrrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|(\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A$
161	109 113 110 114 160	letrd	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A$
162	109 110 25 161	lediv1dd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\|}{\log x} \leq \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A}{\log x}$
163	107 47 48	absdivd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\|}{\|\log x\|}$
164	25	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \log x$
165	32 164	absidd	$⊢ (φ \land x \in (1, +∞)) \to \|\log x\| = \log x$
166	165	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\|}{\|\log x\|} = \frac{\|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\|}{\log x}$
167	163 166	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))\|}{\log x}$
168	5 10 121	fsumge0	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})$
169	67 25 168	divge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}$
170	1	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ^{+}$
171	170	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq A$
172	68 70 169 171	mulge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A$
173	103 172	absidd	$⊢ (φ \land x \in (1, +∞)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A\| = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A$
174	77 158 47 48	div23d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A}{\log x} = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A$
175	173 174	eqtr4d	$⊢ (φ \land x \in (1, +∞)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A\| = \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A}{\log x}$
176	162 167 175	3brtr4d	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x}\| \leq \|(\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A\|$
177	176	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x}\| \leq \|(\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) A\|$
178	66 102 103 108 177	o1le	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log (\frac{x}{n}))}{\log x}) \in 𝑂 (1)$
179	65 178	eqeltrrd	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}) - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}))) \in 𝑂 (1)$
180	35 44 179	o1dif	$⊢ φ \to ((x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1))$
181	4 180	mpbird	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem 2vmadivsumlem

Proof