selberg3lem2

Description: Lemma for selberg3 . Equation 10.4.21 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		elicopnf	$⊢ 1 \in ℝ \to (y \in [1, +∞) \leftrightarrow (y \in ℝ \land 1 \leq y))$
3	1 2	ax-mp	$⊢ y \in [1, +∞) \leftrightarrow (y \in ℝ \land 1 \leq y)$
4	3	simplbi	$⊢ y \in [1, +∞) \to y \in ℝ$
5	4	ssriv	$⊢ [1, +∞) \subseteq ℝ$
6	5	a1i	$⊢ ⊤ \to [1, +∞) \subseteq ℝ$
7	1	a1i	$⊢ ⊤ \to 1 \in ℝ$
8		fzfid	$⊢ (⊤ \land y \in [1, +∞)) \to (1 \dots ⌊y⌋) \in Fin$
9		elfznn	$⊢ m \in (1 \dots ⌊y⌋) \to m \in ℕ$
10	9	adantl	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to m \in ℕ$
11		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
12	10 11	syl	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to Λ (m) \in ℝ$
13	10	nnrpd	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to m \in ℝ^{+}$
14	13	relogcld	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to \log m \in ℝ$
15	12 14	remulcld	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to Λ (m) \log m \in ℝ$
16	8 15	fsumrecl	$⊢ (⊤ \land y \in [1, +∞)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m \in ℝ$
17	4	adantl	$⊢ (⊤ \land y \in [1, +∞)) \to y \in ℝ$
18		chpcl	$⊢ y \in ℝ \to ψ (y) \in ℝ$
19	17 18	syl	$⊢ (⊤ \land y \in [1, +∞)) \to ψ (y) \in ℝ$
20		1rp	$⊢ 1 \in ℝ^{+}$
21	20	a1i	$⊢ (⊤ \land y \in [1, +∞)) \to 1 \in ℝ^{+}$
22	3	simprbi	$⊢ y \in [1, +∞) \to 1 \leq y$
23	22	adantl	$⊢ (⊤ \land y \in [1, +∞)) \to 1 \leq y$
24	17 21 23	rpgecld	$⊢ (⊤ \land y \in [1, +∞)) \to y \in ℝ^{+}$
25	24	relogcld	$⊢ (⊤ \land y \in [1, +∞)) \to \log y \in ℝ$
26	19 25	remulcld	$⊢ (⊤ \land y \in [1, +∞)) \to ψ (y) \log y \in ℝ$
27	16 26	resubcld	$⊢ (⊤ \land y \in [1, +∞)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y \in ℝ$
28	27 24	rerpdivcld	$⊢ (⊤ \land y \in [1, +∞)) \to \frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y} \in ℝ$
29	28	recnd	$⊢ (⊤ \land y \in [1, +∞)) \to \frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y} \in ℂ$
30	24	ex	$⊢ ⊤ \to (y \in [1, +∞) \to y \in ℝ^{+})$
31	30	ssrdv	$⊢ ⊤ \to [1, +∞) \subseteq ℝ^{+}$
32		selberg2lem	$⊢ (y \in ℝ^{+} ⟼ \frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}) \in 𝑂 (1)$
33	32	a1i	$⊢ ⊤ \to (y \in ℝ^{+} ⟼ \frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}) \in 𝑂 (1)$
34	31 33	o1res2	$⊢ ⊤ \to (y \in [1, +∞) ⟼ \frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}) \in 𝑂 (1)$
35		fzfid	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to (1 \dots ⌊x⌋) \in Fin$
36		elfznn	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℕ$
37	36	adantl	$⊢ ((⊤ \land (x \in ℝ \land 1 \leq x)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℕ$
38	37 11	syl	$⊢ ((⊤ \land (x \in ℝ \land 1 \leq x)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \in ℝ$
39	37	nnrpd	$⊢ ((⊤ \land (x \in ℝ \land 1 \leq x)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℝ^{+}$
40	39	relogcld	$⊢ ((⊤ \land (x \in ℝ \land 1 \leq x)) \land m \in (1 \dots ⌊x⌋)) \to \log m \in ℝ$
41	38 40	remulcld	$⊢ ((⊤ \land (x \in ℝ \land 1 \leq x)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \log m \in ℝ$
42	35 41	fsumrecl	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) \log m \in ℝ$
43		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
44	43	ad2antrl	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to ψ (x) \in ℝ$
45		simprl	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to x \in ℝ$
46	20	a1i	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to 1 \in ℝ^{+}$
47		simprr	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to 1 \leq x$
48	45 46 47	rpgecld	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to x \in ℝ^{+}$
49	48	relogcld	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to \log x \in ℝ$
50	44 49	remulcld	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to ψ (x) \log x \in ℝ$
51	42 50	readdcld	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) \log m + ψ (x) \log x \in ℝ$
52	27	adantr	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y \in ℝ$
53	52	recnd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y \in ℂ$
54	24	adantr	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to y \in ℝ^{+}$
55	54	rpcnd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to y \in ℂ$
56	54	rpne0d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to y \neq 0$
57	53 55 56	absdivd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| = \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{\|y\|}$
58	17	adantr	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to y \in ℝ$
59	54	rpge0d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to 0 \leq y$
60	58 59	absidd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|y\| = y$
61	60	oveq2d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{\|y\|} = \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{y}$
62	57 61	eqtrd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| = \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{y}$
63	53	abscld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\| \in ℝ$
64	63 54	rerpdivcld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{y} \in ℝ$
65	42	ad2ant2r	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) \log m \in ℝ$
66		simprll	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to x \in ℝ$
67	66 43	syl	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ψ (x) \in ℝ$
68		simprr	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to y < x$
69	58 66 68	ltled	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to y \leq x$
70	66 54 69	rpgecld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to x \in ℝ^{+}$
71	70	relogcld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \log x \in ℝ$
72	67 71	remulcld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ψ (x) \log x \in ℝ$
73	65 72	readdcld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) \log m + ψ (x) \log x \in ℝ$
74	20	a1i	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to 1 \in ℝ^{+}$
75	53	absge0d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to 0 \leq \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|$
76	23	adantr	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to 1 \leq y$
77	74 54 63 75 76	lediv2ad	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{y} \leq \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{1}$
78	63	recnd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\| \in ℂ$
79	78	div1d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{1} = \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|$
80	77 79	breqtrd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{y} \leq \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|$
81	16	adantr	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m \in ℝ$
82	58 18	syl	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ψ (y) \in ℝ$
83	54	relogcld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \log y \in ℝ$
84	82 83	remulcld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ψ (y) \log y \in ℝ$
85	81 84	readdcld	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m + ψ (y) \log y \in ℝ$
86	81	recnd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m \in ℂ$
87	26	adantr	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ψ (y) \log y \in ℝ$
88	87	recnd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ψ (y) \log y \in ℂ$
89	86 88	abs2dif2d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\| \leq \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m\| + \|ψ (y) \log y\|$
90		vmage0	$⊢ m \in ℕ \to 0 \leq Λ (m)$
91	10 90	syl	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to 0 \leq Λ (m)$
92	10	nnred	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to m \in ℝ$
93	10	nnge1d	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to 1 \leq m$
94	92 93	logge0d	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to 0 \leq \log m$
95	12 14 91 94	mulge0d	$⊢ ((⊤ \land y \in [1, +∞)) \land m \in (1 \dots ⌊y⌋)) \to 0 \leq Λ (m) \log m$
96	8 15 95	fsumge0	$⊢ (⊤ \land y \in [1, +∞)) \to 0 \leq \sum_{m = 1}^{⌊y⌋} Λ (m) \log m$
97	96	adantr	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to 0 \leq \sum_{m = 1}^{⌊y⌋} Λ (m) \log m$
98	81 97	absidd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m\| = \sum_{m = 1}^{⌊y⌋} Λ (m) \log m$
99		chpge0	$⊢ y \in ℝ \to 0 \leq ψ (y)$
100	58 99	syl	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to 0 \leq ψ (y)$
101	58 76	logge0d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to 0 \leq \log y$
102	82 83 100 101	mulge0d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to 0 \leq ψ (y) \log y$
103	87 102	absidd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|ψ (y) \log y\| = ψ (y) \log y$
104	98 103	oveq12d	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m\| + \|ψ (y) \log y\| = \sum_{m = 1}^{⌊y⌋} Λ (m) \log m + ψ (y) \log y$
105	89 104	breqtrd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\| \leq \sum_{m = 1}^{⌊y⌋} Λ (m) \log m + ψ (y) \log y$
106		fzfid	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to (1 \dots ⌊x⌋) \in Fin$
107	36	adantl	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℕ$
108	107 11	syl	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \in ℝ$
109	107	nnrpd	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℝ^{+}$
110	109	relogcld	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to \log m \in ℝ$
111	108 110	remulcld	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \log m \in ℝ$
112	107 90	syl	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (m)$
113	107	nnred	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℝ$
114	107	nnge1d	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to 1 \leq m$
115	113 114	logge0d	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to 0 \leq \log m$
116	108 110 112 115	mulge0d	$⊢ (((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \land m \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (m) \log m$
117		flword2	$⊢ (y \in ℝ \land x \in ℝ \land y \leq x) \to ⌊x⌋ \in ℤ_{\geq ⌊y⌋}$
118	58 66 69 117	syl3anc	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ⌊x⌋ \in ℤ_{\geq ⌊y⌋}$
119		fzss2	$⊢ ⌊x⌋ \in ℤ_{\geq ⌊y⌋} \to (1 \dots ⌊y⌋) \subseteq (1 \dots ⌊x⌋)$
120	118 119	syl	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to (1 \dots ⌊y⌋) \subseteq (1 \dots ⌊x⌋)$
121	106 111 116 120	fsumless	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m \leq \sum_{m = 1}^{⌊x⌋} Λ (m) \log m$
122		chpwordi	$⊢ (y \in ℝ \land x \in ℝ \land y \leq x) \to ψ (y) \leq ψ (x)$
123	58 66 69 122	syl3anc	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ψ (y) \leq ψ (x)$
124	54 70	logled	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to (y \leq x \leftrightarrow \log y \leq \log x)$
125	69 124	mpbid	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \log y \leq \log x$
126	82 67 83 71 100 101 123 125	lemul12ad	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to ψ (y) \log y \leq ψ (x) \log x$
127	81 84 65 72 121 126	le2addd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m + ψ (y) \log y \leq \sum_{m = 1}^{⌊x⌋} Λ (m) \log m + ψ (x) \log x$
128	63 85 73 105 127	letrd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\| \leq \sum_{m = 1}^{⌊x⌋} Λ (m) \log m + ψ (x) \log x$
129	64 63 73 80 128	letrd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \frac{\|\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y\|}{y} \leq \sum_{m = 1}^{⌊x⌋} Λ (m) \log m + ψ (x) \log x$
130	62 129	eqbrtrd	$⊢ ((⊤ \land y \in [1, +∞)) \land ((x \in ℝ \land 1 \leq x) \land y < x)) \to \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| \leq \sum_{m = 1}^{⌊x⌋} Λ (m) \log m + ψ (x) \log x$
131	6 7 29 34 51 130	o1bddrp	$⊢ ⊤ \to \exists c \in ℝ^{+} \forall y \in [1, +∞) \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| \leq c$
132	131	mptru	$⊢ \exists c \in ℝ^{+} \forall y \in [1, +∞) \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| \leq c$
133		simpl	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| \leq c) \to c \in ℝ^{+}$
134		simpr	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| \leq c) \to \forall y \in [1, +∞) \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| \leq c$
135	133 134	selberg3lem1	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| \leq c) \to (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) \in 𝑂 (1)$
136	135	rexlimiva	$⊢ \exists c \in ℝ^{+} \forall y \in [1, +∞) \|\frac{\sum_{m = 1}^{⌊y⌋} Λ (m) \log m - ψ (y) \log y}{y}\| \leq c \to (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) \in 𝑂 (1)$
137	132 136	ax-mp	$⊢ (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberg3lem2

Proof