vmalogdivsum

Description: The sum sum_ n <_ x , Lam ( n ) log 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	vmalogdivsum	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
2	1	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ$
3		1rp	$⊢ 1 \in ℝ^{+}$
4	3	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
5		1red	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ$
6		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
7	6	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
8	7	simpld	$⊢ (⊤ \land x \in (1, +∞)) \to 1 < x$
9	5 2 8	ltled	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \leq x$
10	2 4 9	rpgecld	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ^{+}$
11	10	ex	$⊢ ⊤ \to (x \in (1, +∞) \to x \in ℝ^{+})$
12	11	ssrdv	$⊢ ⊤ \to (1, +∞) \subseteq ℝ^{+}$
13		vmadivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
14	13	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
15	12 14	o1res2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
16		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
17		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
18	17	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
19		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
20	18 19	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
21	20 18	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
22	21	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
23	16 22	fsumcl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
24	10	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
25	24	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
26	23 25	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℂ$
27	18	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
28	27	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
29	21 28	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log n \in ℝ$
30	16 29	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n \in ℝ$
31	2 8	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
32	30 31	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x} \in ℝ$
33	24	rehalfcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℝ$
34	32 33	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2}) \in ℝ$
35	34	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2}) \in ℂ$
36	33	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℂ$
37	23 36	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\log x}{2}) \in ℂ$
38	32	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x} \in ℂ$
39	37 38 36	nnncan2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\log x}{2})) - (\frac{\log x}{2}) - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\log x}{2}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x})$
40	23 36 36	subsub4d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\log x}{2}) - (\frac{\log x}{2}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - ((\frac{\log x}{2}) + (\frac{\log x}{2}))$
41	25	2halvesd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\log x}{2}) + (\frac{\log x}{2}) = \log x$
42	41	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - ((\frac{\log x}{2}) + (\frac{\log x}{2})) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x$
43	40 42	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\log x}{2}) - (\frac{\log x}{2}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x$
44	43	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\log x}{2})) - (\frac{\log x}{2}) - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2}))$
45	23 36 38	sub32d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\log x}{2}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})$
46	10	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
47	46	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log x \in ℝ$
48	21 47	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log x \in ℝ$
49	48	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log x \in ℂ$
50	29	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log n \in ℂ$
51	16 49 50	fsumsub	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n)}{n}) \log x - (\frac{Λ (n)}{n}) \log n) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
52	46 27	relogdivd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) = \log x - \log n$
53	52	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = (\frac{Λ (n)}{n}) (\log x - \log n)$
54	25	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log x \in ℂ$
55	28	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
56	22 54 55	subdid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) (\log x - \log n) = (\frac{Λ (n)}{n}) \log x - (\frac{Λ (n)}{n}) \log n$
57	53 56	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = (\frac{Λ (n)}{n}) \log x - (\frac{Λ (n)}{n}) \log n$
58	57	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n)}{n}) \log x - (\frac{Λ (n)}{n}) \log n)$
59	20	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
60	18	nncnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
61	18	nnne0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
62	59 60 61	divcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
63	16 25 62	fsummulc1	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x$
64	63	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
65	51 58 64	3eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
66	65	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} = \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}$
67	23 25	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x \in ℂ$
68	30	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n \in ℂ$
69	31	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
70	67 68 25 69	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x - \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x} = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x})$
71	23 25 69	divcan4d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log x}{\log x} = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})$
72	71	oveq1d	$⊢ (⊤ \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 n}{\log x}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x})$
73	66 70 72	3eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x})$
74	73	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})$
75	45 74	eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - (\frac{\log x}{2}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})$
76	39 44 75	3eqtr3d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})$
77	76	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2}))) = (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}))$
78		vmalogdivsum2	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
79	77 78	eqeltrdi	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2}))) \in 𝑂 (1)$
80	26 35 79	o1dif	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1))$
81	15 80	mpbid	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
82	81	mptru	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem vmalogdivsum

Proof