vmalogdivsum2

Description: The sum sum_ n <_ x , Lam ( n ) log ( x / n ) / n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ) . Exercise 9.1.7 of Shapiro, p. 336. (Contributed by Mario Carneiro, 30-May-2016)

		Ref	Expression
	Assertion	vmalogdivsum2	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
2		elfznn	$⊢ k \in (1 \dots ⌊x⌋) \to k \in ℕ$
3	2	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to k \in ℕ$
4	3	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to k \in ℝ^{+}$
5	4	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to \log k \in ℝ$
6	5 3	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to \frac{\log k}{k} \in ℝ$
7	1 6	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) \in ℝ$
8	7	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) \in ℂ$
9		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
10	9	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ$
11		1rp	$⊢ 1 \in ℝ^{+}$
12	11	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
13		1red	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ$
14		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
15	14	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
16	15	simpld	$⊢ (⊤ \land x \in (1, +∞)) \to 1 < x$
17	13 10 16	ltled	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \leq x$
18	10 12 17	rpgecld	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ^{+}$
19	18	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
20	19	resqcld	$⊢ (⊤ \land x \in (1, +∞)) \to {\log x}^{2} \in ℝ$
21	20	rehalfcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{{\log x}^{2}}{2} \in ℝ$
22	21	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{{\log x}^{2}}{2} \in ℂ$
23	19	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
24	10 16	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
25	24	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
26	8 22 23 25	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})}{\log x} = (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\frac{{\log x}^{2}}{2}}{\log x})$
27	7 21	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2}) \in ℝ$
28	27	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2}) \in ℂ$
29	28 23 25	divrecd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})}{\log x} = (\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) (\frac{1}{\log x})$
30	20	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to {\log x}^{2} \in ℂ$
31		2cnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℂ$
32		2ne0	$⊢ 2 \neq 0$
33	32	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \neq 0$
34	30 31 23 33 25	divdiv32d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{{\log x}^{2}}{2}}{\log x} = \frac{\frac{{\log x}^{2}}{\log x}}{2}$
35	23	sqvald	$⊢ (⊤ \land x \in (1, +∞)) \to {\log x}^{2} = \log x \log x$
36	35	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{{\log x}^{2}}{\log x} = \frac{\log x \log x}{\log x}$
37	23 23 25	divcan3d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x \log x}{\log x} = \log x$
38	36 37	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{{\log x}^{2}}{\log x} = \log x$
39	38	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{{\log x}^{2}}{\log x}}{2} = \frac{\log x}{2}$
40	34 39	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{{\log x}^{2}}{2}}{\log x} = \frac{\log x}{2}$
41	40	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\frac{{\log x}^{2}}{2}}{\log x}) = (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\log x}{2})$
42	26 29 41	3eqtr3rd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\log x}{2}) = (\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) (\frac{1}{\log x})$
43	42	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\log x}{2})) = (x \in (1, +∞) ⟼ (\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) (\frac{1}{\log x}))$
44	24	rprecred	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{1}{\log x} \in ℝ$
45	18	ex	$⊢ ⊤ \to (x \in (1, +∞) \to x \in ℝ^{+})$
46	45	ssrdv	$⊢ ⊤ \to (1, +∞) \subseteq ℝ^{+}$
47		eqid	$⊢ (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) = (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2}))$
48	47	logdivsum	$⊢ ((x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) : ℝ^{+} ⟶ ℝ \land (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) \in dom \underset{ℝ}{⇝} \land (((x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) \underset{ℝ}{⇝} 1 \land 1 \in ℝ^{+} \land e \leq 1) \to \|(x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) (1) - 1\| \leq \frac{\log 1}{1}))$
49	48	simp2i	$⊢ (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) \in dom \underset{ℝ}{⇝}$
50		rlimdmo1	$⊢ (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) \in dom \underset{ℝ}{⇝} \to (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) \in 𝑂 (1)$
51	49 50	mp1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) \in 𝑂 (1)$
52	46 51	o1res2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) \in 𝑂 (1)$
53		divlogrlim	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0$
54		rlimo1	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0 \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
55	53 54	mp1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
56	27 44 52 55	o1mul2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - (\frac{{\log x}^{2}}{2})) (\frac{1}{\log x})) \in 𝑂 (1)$
57	43 56	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
58	8 23 25	divcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x} \in ℂ$
59	23	halfcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℂ$
60	58 59	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\log x}{2}) \in ℂ$
61		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
62	61	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
63		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
64	62 63	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
65	64 62	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
66	18	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
67	62	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
68	66 67	rpdivcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
69	68	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
70	65 69	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℝ$
71	1 70	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℝ$
72	71	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
73	24	rpcnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
74	72 73 25	divcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} \in ℂ$
75	73	halfcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℂ$
76	74 75	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}) \in ℂ$
77	58 74 59	nnncan2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\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_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x})$
78	8 72 23 25	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} = (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x})$
79		fzfid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
80	64	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (n) \in ℝ$
81	62	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \in ℕ$
82		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
83	82	adantl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
84	81 83	nnmulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n m \in ℕ$
85	80 84	nndivred	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{Λ (n)}{n m} \in ℝ$
86	79 85	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) \in ℝ$
87	86	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) \in ℂ$
88	70	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
89	1 87 88	fsumsub	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
90	64	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
91	62	nncnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
92	62	nnne0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
93	90 91 92	divcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
94	83	nnrecred	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{1}{m} \in ℝ$
95	79 94	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \in ℝ$
96	95	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \in ℂ$
97	69	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
98	93 96 97	subdid	$⊢ ((⊤ \land x \in (1, +∞)) \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}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
99	90	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (n) \in ℂ$
100	91	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \in ℂ$
101	83	nncnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℂ$
102	92	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \neq 0$
103	83	nnne0d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \neq 0$
104	99 100 101 102 103	divdiv1d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{Λ (n)}{n}}{m} = \frac{Λ (n)}{n m}$
105	99 100 102	divcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{Λ (n)}{n} \in ℂ$
106	105 101 103	divrecd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{Λ (n)}{n}}{m} = (\frac{Λ (n)}{n}) (\frac{1}{m})$
107	104 106	eqtr3d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{Λ (n)}{n m} = (\frac{Λ (n)}{n}) (\frac{1}{m})$
108	107	sumeq2dv	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n}) (\frac{1}{m})$
109	101 103	reccld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{1}{m} \in ℂ$
110	79 93 109	fsummulc2	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n}) (\frac{1}{m})$
111	108 110	eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) = (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m})$
112	111	oveq1d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
113	98 112	eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
114	113	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \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⌋} (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) - (\frac{Λ (n)}{n}) \log (\frac{x}{n}))$
115		vmasum	$⊢ k \in ℕ \to \sum_{n \in \{y \in ℕ \| y ∥ k\}} Λ (n) = \log k$
116	3 115	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to \sum_{n \in \{y \in ℕ \| y ∥ k\}} Λ (n) = \log k$
117	116	oveq1d	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to \frac{\sum_{n \in \{y \in ℕ \| y ∥ k\}} Λ (n)}{k} = \frac{\log k}{k}$
118		fzfid	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to (1 \dots k) \in Fin$
119		dvdsssfz1	$⊢ k \in ℕ \to \{y \in ℕ \| y ∥ k\} \subseteq (1 \dots k)$
120	3 119	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to \{y \in ℕ \| y ∥ k\} \subseteq (1 \dots k)$
121	118 120	ssfid	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to \{y \in ℕ \| y ∥ k\} \in Fin$
122	3	nncnd	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to k \in ℂ$
123		ssrab2	$⊢ \{y \in ℕ \| y ∥ k\} \subseteq ℕ$
124		simprr	$⊢ ((⊤ \land x \in (1, +∞)) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to n \in \{y \in ℕ \| y ∥ k\}$
125	123 124	sselid	$⊢ ((⊤ \land x \in (1, +∞)) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to n \in ℕ$
126	125 63	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to Λ (n) \in ℝ$
127	126	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to Λ (n) \in ℂ$
128	127	anassrs	$⊢ (((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \land n \in \{y \in ℕ \| y ∥ k\}) \to Λ (n) \in ℂ$
129	3	nnne0d	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to k \neq 0$
130	121 122 128 129	fsumdivc	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to \frac{\sum_{n \in \{y \in ℕ \| y ∥ k\}} Λ (n)}{k} = \sum_{n \in \{y \in ℕ \| y ∥ k\}} (\frac{Λ (n)}{k})$
131	117 130	eqtr3d	$⊢ ((⊤ \land x \in (1, +∞)) \land k \in (1 \dots ⌊x⌋)) \to \frac{\log k}{k} = \sum_{n \in \{y \in ℕ \| y ∥ k\}} (\frac{Λ (n)}{k})$
132	131	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) = \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} (\frac{Λ (n)}{k})$
133		oveq2	$⊢ k = n m \to \frac{Λ (n)}{k} = \frac{Λ (n)}{n m}$
134	2	ad2antrl	$⊢ ((⊤ \land x \in (1, +∞)) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to k \in ℕ$
135	134	nncnd	$⊢ ((⊤ \land x \in (1, +∞)) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to k \in ℂ$
136	134	nnne0d	$⊢ ((⊤ \land x \in (1, +∞)) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to k \neq 0$
137	127 135 136	divcld	$⊢ ((⊤ \land x \in (1, +∞)) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to \frac{Λ (n)}{k} \in ℂ$
138	133 10 137	dvdsflsumcom	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} (\frac{Λ (n)}{k}) = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m})$
139	132 138	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m})$
140	139	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (n)}{n m}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
141	89 114 140	3eqtr4rd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))$
142	141	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k}) - \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{1}{m}) - \log (\frac{x}{n}))}{\log x}$
143	77 78 142	3eqtr2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\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{1}{m}) - \log (\frac{x}{n}))}{\log x}$
144	143	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\log x}) - (\frac{\log x}{2}) - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}))) = (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))}{\log x})$
145		1red	$⊢ ⊤ \to 1 \in ℝ$
146	1 65	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℝ$
147	146 24	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x} \in ℝ$
148		ioossre	$⊢ (1, +∞) \subseteq ℝ$
149		ax-1cn	$⊢ 1 \in ℂ$
150		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 1 \in ℂ) \to (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
151	148 149 150	mp2an	$⊢ (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
152	151	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
153	147	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x} \in ℂ$
154	12	rpcnd	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℂ$
155	146	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
156	155 23 23 25	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})$
157	155 23	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℂ$
158	157 23 25	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})$
159	23 25	dividd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{\log x} = 1$
160	159	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$
161	156 158 160	3eqtr3rd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1 = (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x})$
162	161	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1) = (x \in (1, +∞) ⟼ (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x}))$
163	146 19	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℝ$
164		vmadivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
165	164	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
166	46 165	o1res2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
167	163 44 166 55	o1mul2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x})) \in 𝑂 (1)$
168	162 167	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1) \in 𝑂 (1)$
169	153 154 168	o1dif	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ 1) \in 𝑂 (1))$
170	152 169	mpbird	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) \in 𝑂 (1)$
171	147 170	o1lo1d	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) \in \leq 𝑂 (1)$
172	95 69	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) \in ℝ$
173	65 172	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in ℝ$
174	1 173	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in ℝ$
175	174 24	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))}{\log x} \in ℝ$
176		1red	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
177		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
178	62 177	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n)$
179	64 67 178	divge0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{Λ (n)}{n}$
180	68	rpred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
181	91	mulid2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 n = n$
182		fznnfl	$⊢ x \in ℝ \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
183	10 182	syl	$⊢ (⊤ \land x \in (1, +∞)) \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
184	183	simplbda	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \leq x$
185	181 184	eqbrtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 n \leq x$
186	10	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
187	176 186 67	lemuldivd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 n \leq x \leftrightarrow 1 \leq \frac{x}{n})$
188	185 187	mpbid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x}{n}$
189		harmonicubnd	$⊢ (\frac{x}{n} \in ℝ \land 1 \leq \frac{x}{n}) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \leq \log (\frac{x}{n}) + 1$
190	180 188 189	syl2anc	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \leq \log (\frac{x}{n}) + 1$
191	95 69 176	lesubadd2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) \leq 1 \leftrightarrow \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \leq \log (\frac{x}{n}) + 1)$
192	190 191	mpbird	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) \leq 1$
193	172 176 65 179 192	lemul2ad	$⊢ ((⊤ \land x \in (1, +∞)) \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{Λ (n)}{n}) \cdot 1$
194	93	mulid1d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \cdot 1 = \frac{Λ (n)}{n}$
195	193 194	breqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \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{Λ (n)}{n}$
196	1 173 65 195	fsumle	$⊢ (⊤ \land x \in (1, +∞)) \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})$
197	174 146 24 196	lediv1dd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))}{\log x} \leq \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}$
198	197	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{1}{m}) - \log (\frac{x}{n}))}{\log x} \leq \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}$
199	145 171 147 175 198	lo1le	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))}{\log x}) \in \leq 𝑂 (1)$
200		0red	$⊢ ⊤ \to 0 \in ℝ$
201		harmoniclbnd	$⊢ \frac{x}{n} \in ℝ^{+} \to \log (\frac{x}{n}) \leq \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m})$
202	68 201	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \leq \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m})$
203	95 69	subge0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (0 \leq \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}) \leftrightarrow \log (\frac{x}{n}) \leq \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}))$
204	202 203	mpbird	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})$
205	65 172 179 204	mulge0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))$
206	1 173 205	fsumge0	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))$
207	174 24 206	divge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))}{\log x}$
208	175 200 207	o1lo12	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))}{\log x}) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))}{\log x}) \in \leq 𝑂 (1))$
209	199 208	mpbird	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))}{\log x}) \in 𝑂 (1)$
210	144 209	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\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)$
211	60 76 210	o1dif	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ (\frac{\sum_{k = 1}^{⌊x⌋} (\frac{\log k}{k})}{\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))$
212	57 211	mpbid	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
213	212	mptru	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem vmalogdivsum2

Proof