selbergb

Description: Convert eventual boundedness in selberg to boundedness on [ 1 , +oo ) . (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 30-May-2016)

		Ref	Expression
	Assertion	selbergb	$⊢ \exists c \in ℝ^{+} \forall x \in [1, +∞) \|(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \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	4	ex	$⊢ ⊤ \to (x \in [1, +∞) \to x \in ℝ)$
6	5	ssrdv	$⊢ ⊤ \to [1, +∞) \subseteq ℝ$
7	1	a1i	$⊢ ⊤ \to 1 \in ℝ$
8		fzfid	$⊢ (⊤ \land x \in [1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
9		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
10	9	adantl	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
11		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
12	10 11	syl	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
13	10	nnrpd	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
14	13	relogcld	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
15	4	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
16	15 10	nndivred	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
17		chpcl	$⊢ \frac{x}{n} \in ℝ \to ψ (\frac{x}{n}) \in ℝ$
18	16 17	syl	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℝ$
19	14 18	readdcld	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n + ψ (\frac{x}{n}) \in ℝ$
20	12 19	remulcld	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\log n + ψ (\frac{x}{n})) \in ℝ$
21	8 20	fsumrecl	$⊢ (⊤ \land x \in [1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) \in ℝ$
22		1rp	$⊢ 1 \in ℝ^{+}$
23	22	a1i	$⊢ (⊤ \land x \in [1, +∞)) \to 1 \in ℝ^{+}$
24	3	simplbda	$⊢ (⊤ \land x \in [1, +∞)) \to 1 \leq x$
25	4 23 24	rpgecld	$⊢ (⊤ \land x \in [1, +∞)) \to x \in ℝ^{+}$
26	21 25	rerpdivcld	$⊢ (⊤ \land x \in [1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x} \in ℝ$
27		2re	$⊢ 2 \in ℝ$
28	27	a1i	$⊢ (⊤ \land x \in [1, +∞)) \to 2 \in ℝ$
29	25	relogcld	$⊢ (⊤ \land x \in [1, +∞)) \to \log x \in ℝ$
30	28 29	remulcld	$⊢ (⊤ \land x \in [1, +∞)) \to 2 \log x \in ℝ$
31	26 30	resubcld	$⊢ (⊤ \land x \in [1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x \in ℝ$
32	31	recnd	$⊢ (⊤ \land x \in [1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x \in ℂ$
33	25	ex	$⊢ ⊤ \to (x \in [1, +∞) \to x \in ℝ^{+})$
34	33	ssrdv	$⊢ ⊤ \to [1, +∞) \subseteq ℝ^{+}$
35		selberg	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) \in 𝑂 (1)$
36	35	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) \in 𝑂 (1)$
37	34 36	o1res2	$⊢ ⊤ \to (x \in [1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) \in 𝑂 (1)$
38		fzfid	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to (1 \dots ⌊y⌋) \in Fin$
39		elfznn	$⊢ n \in (1 \dots ⌊y⌋) \to n \in ℕ$
40	39	adantl	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to n \in ℕ$
41	40 11	syl	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to Λ (n) \in ℝ$
42	40	nnrpd	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to n \in ℝ^{+}$
43	42	relogcld	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to \log n \in ℝ$
44		simprl	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to y \in ℝ$
45	44	adantr	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to y \in ℝ$
46	45 40	nndivred	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to \frac{y}{n} \in ℝ$
47		chpcl	$⊢ \frac{y}{n} \in ℝ \to ψ (\frac{y}{n}) \in ℝ$
48	46 47	syl	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to ψ (\frac{y}{n}) \in ℝ$
49	43 48	readdcld	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to \log n + ψ (\frac{y}{n}) \in ℝ$
50	41 49	remulcld	$⊢ ((⊤ \land (y \in ℝ \land 1 \leq y)) \land n \in (1 \dots ⌊y⌋)) \to Λ (n) (\log n + ψ (\frac{y}{n})) \in ℝ$
51	38 50	fsumrecl	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n})) \in ℝ$
52	27	a1i	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to 2 \in ℝ$
53	22	a1i	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to 1 \in ℝ^{+}$
54		simprr	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to 1 \leq y$
55	44 53 54	rpgecld	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to y \in ℝ^{+}$
56	55	relogcld	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to \log y \in ℝ$
57	52 56	remulcld	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to 2 \log y \in ℝ$
58	51 57	readdcld	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n})) + 2 \log y \in ℝ$
59	31	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x \in ℝ$
60	59	recnd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x \in ℂ$
61	60	abscld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x\| \in ℝ$
62	26	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x} \in ℝ$
63	30	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \log x \in ℝ$
64	62 63	readdcld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) + 2 \log x \in ℝ$
65		fzfid	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (1 \dots ⌊y⌋) \in Fin$
66	39	adantl	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to n \in ℕ$
67	66 11	syl	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to Λ (n) \in ℝ$
68	66	nnrpd	$⊢ (((⊤ \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	relogcld	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to \log n \in ℝ$
70		simprll	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℝ$
71	70	adantr	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to y \in ℝ$
72	71 66	nndivred	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to \frac{y}{n} \in ℝ$
73	72 47	syl	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to ψ (\frac{y}{n}) \in ℝ$
74	69 73	readdcld	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to \log n + ψ (\frac{y}{n}) \in ℝ$
75	67 74	remulcld	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to Λ (n) (\log n + ψ (\frac{y}{n})) \in ℝ$
76	65 75	fsumrecl	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n})) \in ℝ$
77	27	a1i	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \in ℝ$
78	25	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℝ^{+}$
79	4	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℝ$
80		simprr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x < y$
81	79 70 80	ltled	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \leq y$
82	70 78 81	rpgecld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℝ^{+}$
83	82	relogcld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log y \in ℝ$
84	77 83	remulcld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \log y \in ℝ$
85	76 84	readdcld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n})) + 2 \log y \in ℝ$
86	62	recnd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x} \in ℂ$
87	63	recnd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \log x \in ℂ$
88	86 87	abs2dif2d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x\| \leq \|\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}\| + \|2 \log x\|$
89	21	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) \in ℝ$
90		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
91	10 90	syl	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n)$
92	10	nnred	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
93	10	nnge1d	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq n$
94	92 93	logge0d	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \log n$
95		chpge0	$⊢ \frac{x}{n} \in ℝ \to 0 \leq ψ (\frac{x}{n})$
96	16 95	syl	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq ψ (\frac{x}{n})$
97	14 18 94 96	addge0d	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \log n + ψ (\frac{x}{n})$
98	12 19 91 97	mulge0d	$⊢ ((⊤ \land x \in [1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n) (\log n + ψ (\frac{x}{n}))$
99	8 20 98	fsumge0	$⊢ (⊤ \land x \in [1, +∞)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))$
100	99	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))$
101	89 78 100	divge0d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}$
102	62 101	absidd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}\| = \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}$
103	78	relogcld	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \in ℝ$
104		2rp	$⊢ 2 \in ℝ^{+}$
105		rpge0	$⊢ 2 \in ℝ^{+} \to 0 \leq 2$
106	104 105	mp1i	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq 2$
107	24	adantr	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 1 \leq x$
108	79 107	logge0d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \log x$
109	77 103 106 108	mulge0d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq 2 \log x$
110	63 109	absidd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|2 \log x\| = 2 \log x$
111	102 110	oveq12d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}\| + \|2 \log x\| = (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) + 2 \log x$
112	88 111	breqtrd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x\| \leq (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) + 2 \log x$
113	22	a1i	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 1 \in ℝ^{+}$
114	79	adantr	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to x \in ℝ$
115	114 66	nndivred	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to \frac{x}{n} \in ℝ$
116	115 17	syl	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to ψ (\frac{x}{n}) \in ℝ$
117	69 116	readdcld	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to \log n + ψ (\frac{x}{n}) \in ℝ$
118	67 117	remulcld	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to Λ (n) (\log n + ψ (\frac{x}{n})) \in ℝ$
119	65 118	fsumrecl	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{x}{n})) \in ℝ$
120	66 90	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)$
121	66	nnred	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to n \in ℝ$
122	66	nnge1d	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to 1 \leq n$
123	121 122	logge0d	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to 0 \leq \log n$
124	115 95	syl	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to 0 \leq ψ (\frac{x}{n})$
125	69 116 123 124	addge0d	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to 0 \leq \log n + ψ (\frac{x}{n})$
126	67 117 120 125	mulge0d	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to 0 \leq Λ (n) (\log n + ψ (\frac{x}{n}))$
127		flword2	$⊢ (x \in ℝ \land y \in ℝ \land x \leq y) \to ⌊y⌋ \in ℤ_{\geq ⌊x⌋}$
128	79 70 81 127	syl3anc	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ⌊y⌋ \in ℤ_{\geq ⌊x⌋}$
129		fzss2	$⊢ ⌊y⌋ \in ℤ_{\geq ⌊x⌋} \to (1 \dots ⌊x⌋) \subseteq (1 \dots ⌊y⌋)$
130	128 129	syl	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (1 \dots ⌊x⌋) \subseteq (1 \dots ⌊y⌋)$
131	65 118 126 130	fsumless	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) \leq \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{x}{n}))$
132	81	adantr	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to x \leq y$
133	114 71 68 132	lediv1dd	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to \frac{x}{n} \leq \frac{y}{n}$
134		chpwordi	$⊢ (\frac{x}{n} \in ℝ \land \frac{y}{n} \in ℝ \land \frac{x}{n} \leq \frac{y}{n}) \to ψ (\frac{x}{n}) \leq ψ (\frac{y}{n})$
135	115 72 133 134	syl3anc	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to ψ (\frac{x}{n}) \leq ψ (\frac{y}{n})$
136	116 73 69 135	leadd2dd	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to \log n + ψ (\frac{x}{n}) \leq \log n + ψ (\frac{y}{n})$
137	117 74 67 120 136	lemul2ad	$⊢ (((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊y⌋)) \to Λ (n) (\log n + ψ (\frac{x}{n})) \leq Λ (n) (\log n + ψ (\frac{y}{n}))$
138	65 118 75 137	fsumle	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{x}{n})) \leq \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n}))$
139	89 119 76 131 138	letrd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) \leq \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n}))$
140	89 76 113 79 100 139 107	lediv12ad	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x} \leq \frac{\sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n}))}{1}$
141	76	recnd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n})) \in ℂ$
142	141	div1d	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{\sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n}))}{1} = \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n}))$
143	140 142	breqtrd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x} \leq \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n}))$
144	78 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)$
145	81 144	mpbid	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \leq \log y$
146	103 83 77 106 145	lemul2ad	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \log x \leq 2 \log y$
147	62 63 76 84 143 146	le2addd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) + 2 \log x \leq \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n})) + 2 \log y$
148	61 64 85 112 147	letrd	$⊢ ((⊤ \land x \in [1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x\| \leq \sum_{n = 1}^{⌊y⌋} Λ (n) (\log n + ψ (\frac{y}{n})) + 2 \log y$
149	6 7 32 37 58 148	o1bddrp	$⊢ ⊤ \to \exists c \in ℝ^{+} \forall x \in [1, +∞) \|(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x\| \leq c$
150	149	mptru	$⊢ \exists c \in ℝ^{+} \forall x \in [1, +∞) \|(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x\| \leq c$

Metamath Proof Explorer

Theorem selbergb

Proof