selberg2b

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

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

Metamath Proof Explorer

Theorem selberg2b

Proof