vmadivsumb

Description: Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016)

		Ref	Expression
	Assertion	vmadivsumb	$⊢ \exists c \in ℝ^{+} \forall x \in [1, +∞) \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x\| \leq c$

Proof

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		elicopnf	$⊢ 1 \in ℝ \to (x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x))$
3	1 2	mp1i	$⊢ ⊤ \to (x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x))$
4	3	simprbda	$⊢ (⊤ \land x \in [1, +∞)) \to x \in ℝ$
5		1rp	$⊢ 1 \in ℝ^{+}$
6	5	a1i	$⊢ (⊤ \land x \in [1, +∞)) \to 1 \in ℝ^{+}$
7	3	simplbda	$⊢ (⊤ \land x \in [1, +∞)) \to 1 \leq x$
8	4 6 7	rpgecld	$⊢ (⊤ \land x \in [1, +∞)) \to x \in ℝ^{+}$
9	8	ex	$⊢ ⊤ \to (x \in [1, +∞) \to x \in ℝ^{+})$
10	9	ssrdv	$⊢ ⊤ \to [1, +∞) \subseteq ℝ^{+}$
11		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
12	10 11	sstrdi	$⊢ ⊤ \to [1, +∞) \subseteq ℝ$
13	1	a1i	$⊢ ⊤ \to 1 \in ℝ$
14		fzfid	$⊢ (⊤ \land x \in [1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
15		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
16	15	adantl	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
17		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
18	16 17	syl	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
19	18 16	nndivred	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
20	14 19	fsumrecl	$⊢ (⊤ \land x \in [1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℝ$
21	8	relogcld	$⊢ (⊤ \land x \in [1, +∞)) \to \log x \in ℝ$
22	20 21	resubcld	$⊢ (⊤ \land x \in [1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℝ$
23	22	recnd	$⊢ (⊤ \land x \in [1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℂ$
24		vmadivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
25	24	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
26	10 25	o1res2	$⊢ ⊤ \to (x \in [1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
27		fzfid	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to (1 \dots ⌊y⌋) \in Fin$
28		elfznn	$⊢ n \in (1 \dots ⌊y⌋) \to n \in ℕ$
29	28	adantl	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to n \in ℕ$
30	29 17	syl	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to Λ (n) \in ℝ$
31	30 29	nndivred	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to \frac{Λ (n)}{n} \in ℝ$
32	27 31	fsumrecl	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to \sum_{n = 1}^{⌊y⌋} (\frac{Λ (n)}{n}) \in ℝ$
33		simprl	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to y \in ℝ$
34	5	a1i	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to 1 \in ℝ^{+}$
35		simprr	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to 1 \leq y$
36	33 34 35	rpgecld	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to y \in ℝ^{+}$
37	36	relogcld	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to \log y \in ℝ$
38	32 37	readdcld	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to \sum_{n = 1}^{⌊y⌋} (\frac{Λ (n)}{n}) + \log y \in ℝ$
39	22	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℝ$
40	39	recnd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℂ$
41	40	abscld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x\| \in ℝ$
42	20	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℝ$
43	8	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℝ^{+}$
44	43	relogcld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \in ℝ$
45	42 44	readdcld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) + \log x \in ℝ$
46	38	ad2ant2r	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊y⌋} (\frac{Λ (n)}{n}) + \log y \in ℝ$
47	42	recnd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
48	44	recnd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \in ℂ$
49	47 48	abs2dif2d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x\| \leq \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})\| + \|\log x\|$
50	16	nnrpd	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
51		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
52	16 51	syl	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n)$
53	18 50 52	divge0d	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{Λ (n)}{n}$
54	14 19 53	fsumge0	$⊢ (⊤ \land x \in [1, +∞)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})$
55	54	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})$
56	42 55	absidd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})\| = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})$
57	21	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \in ℝ$
58	4	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℝ$
59	7	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 1 \leq x$
60	58 59	logge0d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \log x$
61	57 60	absidd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\log x\| = \log x$
62	56 61	oveq12d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})\| + \|\log x\| = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) + \log x$
63	49 62	breqtrd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) + \log x$
64	32	ad2ant2r	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊y⌋} (\frac{Λ (n)}{n}) \in ℝ$
65	36	ad2ant2r	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℝ^{+}$
66	65	relogcld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log y \in ℝ$
67		fzfid	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (1 \dots ⌊y⌋) \in Fin$
68	28	adantl	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to n \in ℕ$
69	68 17	syl	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to Λ (n) \in ℝ$
70	69 68	nndivred	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to \frac{Λ (n)}{n} \in ℝ$
71	68	nnrpd	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to n \in ℝ^{+}$
72	68 51	syl	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to 0 \leq Λ (n)$
73	69 71 72	divge0d	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to 0 \leq \frac{Λ (n)}{n}$
74		simprll	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℝ$
75		simprr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x < y$
76	58 74 75	ltled	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \leq y$
77		flword2	$⊢ (x \in ℝ \land y \in ℝ \land x \leq y) \to ⌊y⌋ \in ℤ_{\geq ⌊x⌋}$
78	58 74 76 77	syl3anc	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ⌊y⌋ \in ℤ_{\geq ⌊x⌋}$
79		fzss2	$⊢ ⌊y⌋ \in ℤ_{\geq ⌊x⌋} \to (1 \dots ⌊x⌋) \subseteq (1 \dots ⌊y⌋)$
80	78 79	syl	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (1 \dots ⌊x⌋) \subseteq (1 \dots ⌊y⌋)$
81	67 70 73 80	fsumless	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \leq \sum_{n = 1}^{⌊y⌋} (\frac{Λ (n)}{n})$
82	74 43 76	rpgecld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℝ^{+}$
83	43 82	logled	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (x \leq y \leftrightarrow \log x \leq \log y)$
84	76 83	mpbid	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \leq \log y$
85	42 44 64 66 81 84	le2addd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) + \log x \leq \sum_{n = 1}^{⌊y⌋} (\frac{Λ (n)}{n}) + \log y$
86	41 45 46 63 85	letrd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x\| \leq \sum_{n = 1}^{⌊y⌋} (\frac{Λ (n)}{n}) + \log y$
87	12 13 23 26 38 86	o1bddrp	$⊢ ⊤ \to \exists c \in ℝ^{+} \forall x \in [1, +∞) \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x\| \leq c$
88	87	mptru	$⊢ \exists c \in ℝ^{+} \forall x \in [1, +∞) \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x\| \leq c$

Metamath Proof Explorer

Theorem vmadivsumb

Proof