selberg3lem1

Description: Introduce a log weighting on the summands of sum_ m x. n <_ x , Lam ( m ) Lam ( n ) , the core of selberg2 (written here as sum_ n <_ x , Lam ( n ) psi ( x / n ) ). Equation 10.4.21 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

	Ref	Expression
Hypotheses	selberg3lem1.1	$⊢ φ \to A \in ℝ^{+}$
	selberg3lem1.2	$⊢ φ \to \forall y \in [1, +∞) \|\frac{\sum_{k = 1}^{⌊y⌋} Λ (k) \log k - ψ (y) \log y}{y}\| \leq A$
Assertion	selberg3lem1	$⊢ φ \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)$

Proof

Step	Hyp	Ref	Expression
1		selberg3lem1.1	$⊢ φ \to A \in ℝ^{+}$
2		selberg3lem1.2	$⊢ φ \to \forall y \in [1, +∞) \|\frac{\sum_{k = 1}^{⌊y⌋} Λ (k) \log k - ψ (y) \log y}{y}\| \leq A$
3		1red	$⊢ φ \to 1 \in ℝ$
4		ioossre	$⊢ (1, +∞) \subseteq ℝ$
5	1	rpcnd	$⊢ φ \to A \in ℂ$
6		o1const	$⊢ ((1, +∞) \subseteq ℝ \land A \in ℂ) \to (x \in (1, +∞) ⟼ A) \in 𝑂 (1)$
7	4 5 6	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ A) \in 𝑂 (1)$
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	12 10	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
14	8 13	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℝ$
15		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
16		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
17	16	simpld	$⊢ x \in (1, +∞) \to 1 < x$
18	15 17	rplogcld	$⊢ x \in (1, +∞) \to \log x \in ℝ^{+}$
19		rpdivcl	$⊢ (A \in ℝ^{+} \land \log x \in ℝ^{+}) \to \frac{A}{\log x} \in ℝ^{+}$
20	1 18 19	syl2an	$⊢ (φ \land x \in (1, +∞)) \to \frac{A}{\log x} \in ℝ^{+}$
21	20	rpred	$⊢ (φ \land x \in (1, +∞)) \to \frac{A}{\log x} \in ℝ$
22	14 21	remulcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) \in ℝ$
23	22	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) \in ℂ$
24	5	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℂ$
25	14	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
26	18	adantl	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
27	26	rpcnd	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℂ$
28	20	rpcnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{A}{\log x} \in ℂ$
29	25 27 28	subdird	$⊢ (φ \land x \in (1, +∞)) \to (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{A}{\log x}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) - \log x (\frac{A}{\log x})$
30	26	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to \log x \neq 0$
31	24 27 30	divcan2d	$⊢ (φ \land x \in (1, +∞)) \to \log x (\frac{A}{\log x}) = A$
32	31	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) - \log x (\frac{A}{\log x}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) - A$
33	29 32	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{A}{\log x}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) - A$
34	33	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{A}{\log x})) = (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) - A)$
35	26	rpred	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ$
36	14 35	resubcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℝ$
37	15	adantl	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ$
38		0red	$⊢ (φ \land x \in (1, +∞)) \to 0 \in ℝ$
39		1red	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ$
40		0lt1	$⊢ 0 < 1$
41	40	a1i	$⊢ (φ \land x \in (1, +∞)) \to 0 < 1$
42	17	adantl	$⊢ (φ \land x \in (1, +∞)) \to 1 < x$
43	38 39 37 41 42	lttrd	$⊢ (φ \land x \in (1, +∞)) \to 0 < x$
44	37 43	elrpd	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ^{+}$
45	44	ex	$⊢ φ \to (x \in (1, +∞) \to x \in ℝ^{+})$
46	45	ssrdv	$⊢ φ \to (1, +∞) \subseteq ℝ^{+}$
47		vmadivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
48	47	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
49	46 48	o1res2	$⊢ φ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
50	4	a1i	$⊢ φ \to (1, +∞) \subseteq ℝ$
51		ere	$⊢ e \in ℝ$
52	51	a1i	$⊢ φ \to e \in ℝ$
53	1	rpred	$⊢ φ \to A \in ℝ$
54	20	adantrr	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to \frac{A}{\log x} \in ℝ^{+}$
55	54	rprege0d	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to (\frac{A}{\log x} \in ℝ \land 0 \leq \frac{A}{\log x})$
56		absid	$⊢ (\frac{A}{\log x} \in ℝ \land 0 \leq \frac{A}{\log x}) \to \|\frac{A}{\log x}\| = \frac{A}{\log x}$
57	55 56	syl	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to \|\frac{A}{\log x}\| = \frac{A}{\log x}$
58		loge	$⊢ \log e = 1$
59		simprr	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to e \leq x$
60		epr	$⊢ e \in ℝ^{+}$
61	44	adantrr	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to x \in ℝ^{+}$
62		logleb	$⊢ (e \in ℝ^{+} \land x \in ℝ^{+}) \to (e \leq x \leftrightarrow \log e \leq \log x)$
63	60 61 62	sylancr	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to (e \leq x \leftrightarrow \log e \leq \log x)$
64	59 63	mpbid	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to \log e \leq \log x$
65	58 64	eqbrtrrid	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to 1 \leq \log x$
66		1rp	$⊢ 1 \in ℝ^{+}$
67		rpregt0	$⊢ 1 \in ℝ^{+} \to (1 \in ℝ \land 0 < 1)$
68	66 67	mp1i	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to (1 \in ℝ \land 0 < 1)$
69	26	adantrr	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to \log x \in ℝ^{+}$
70	69	rpregt0d	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to (\log x \in ℝ \land 0 < \log x)$
71	1	adantr	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to A \in ℝ^{+}$
72	71	rpregt0d	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to (A \in ℝ \land 0 < A)$
73		lediv2	$⊢ ((1 \in ℝ \land 0 < 1) \land (\log x \in ℝ \land 0 < \log x) \land (A \in ℝ \land 0 < A)) \to (1 \leq \log x \leftrightarrow \frac{A}{\log x} \leq \frac{A}{1})$
74	68 70 72 73	syl3anc	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to (1 \leq \log x \leftrightarrow \frac{A}{\log x} \leq \frac{A}{1})$
75	65 74	mpbid	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to \frac{A}{\log x} \leq \frac{A}{1}$
76	5	adantr	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to A \in ℂ$
77	76	div1d	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to \frac{A}{1} = A$
78	75 77	breqtrd	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to \frac{A}{\log x} \leq A$
79	57 78	eqbrtrd	$⊢ (φ \land (x \in (1, +∞) \land e \leq x)) \to \|\frac{A}{\log x}\| \leq A$
80	50 28 52 53 79	elo1d	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{A}{\log x}) \in 𝑂 (1)$
81	36 21 49 80	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{A}{\log x})) \in 𝑂 (1)$
82	34 81	eqeltrrd	$⊢ φ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) - A) \in 𝑂 (1)$
83	23 24 82	o1dif	$⊢ φ \to ((x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x})) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ A) \in 𝑂 (1))$
84	7 83	mpbird	$⊢ φ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x})) \in 𝑂 (1)$
85		2re	$⊢ 2 \in ℝ$
86		rerpdivcl	$⊢ (2 \in ℝ \land \log x \in ℝ^{+}) \to \frac{2}{\log x} \in ℝ$
87	85 26 86	sylancr	$⊢ (φ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
88		nndivre	$⊢ (x \in ℝ \land n \in ℕ) \to \frac{x}{n} \in ℝ$
89	37 9 88	syl2an	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
90		chpcl	$⊢ \frac{x}{n} \in ℝ \to ψ (\frac{x}{n}) \in ℝ$
91	89 90	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℝ$
92	12 91	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \in ℝ$
93	10	nnrpd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
94	93	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
95	92 94	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
96	8 95	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
97	87 96	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
98	8 92	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℝ$
99	97 98	resubcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℝ$
100	99 44	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \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 ℝ$
101	100	recnd	$⊢ (φ \land x \in (1, +∞)) \to \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 ℂ$
102	101	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|\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 ℝ$
103	23	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x})\| \in ℝ$
104		2cnd	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℂ$
105	96	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
106	104 105	mulcld	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
107	98	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℂ$
108	107 27	mulcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x \in ℂ$
109	106 108	subcld	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x \in ℂ$
110	109	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\| \in ℝ$
111	43	gt0ne0d	$⊢ (φ \land x \in (1, +∞)) \to x \neq 0$
112	110 37 111	redivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x} \in ℝ$
113	53	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ$
114	14 113	remulcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A \in ℝ$
115	12	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
116		fzfid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
117		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
118	117	adantl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
119		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
120	118 119	syl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \in ℝ$
121	118	nnrpd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℝ^{+}$
122	121	relogcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log m \in ℝ$
123	120 122	remulcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \log m \in ℝ$
124	116 123	fsumrecl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℝ$
125	9	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
126		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
127	44 125 126	syl2an	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
128	127	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
129	91 128	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \log (\frac{x}{n}) \in ℝ$
130	124 129	resubcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}) \in ℝ$
131	130	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}) \in ℂ$
132	115 131	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})) \in ℂ$
133	8 132	fsumcl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})) \in ℂ$
134	133	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| \in ℝ$
135	132	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| \in ℝ$
136	8 135	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| \in ℝ$
137	113 37	remulcld	$⊢ (φ \land x \in (1, +∞)) \to A x \in ℝ$
138	14 137	remulcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x \in ℝ$
139	8 132	fsumabs	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} \|Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\|$
140	53	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℝ$
141	37	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
142	140 141	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A x \in ℝ$
143	13 142	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) A x \in ℝ$
144	131	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\| \in ℝ$
145	142 10	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{A x}{n} \in ℝ$
146		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
147	10 146	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n)$
148	89	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℂ$
149	127	rpne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \neq 0$
150	131 148 149	absdivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})}{\frac{x}{n}}\| = \frac{\|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|}{\|\frac{x}{n}\|}$
151	127	rpge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{x}{n}$
152	89 151	absidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{x}{n}\| = \frac{x}{n}$
153	152	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|}{\|\frac{x}{n}\|} = \frac{\|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|}{\frac{x}{n}}$
154	150 153	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})}{\frac{x}{n}}\| = \frac{\|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|}{\frac{x}{n}}$
155		fveq2	$⊢ k = m \to Λ (k) = Λ (m)$
156		fveq2	$⊢ k = m \to \log k = \log m$
157	155 156	oveq12d	$⊢ k = m \to Λ (k) \log k = Λ (m) \log m$
158	157	cbvsumv	$⊢ \sum_{k = 1}^{⌊y⌋} Λ (k) \log k = \sum_{m = 1}^{⌊y⌋} Λ (m) \log m$
159		fveq2	$⊢ y = \frac{x}{n} \to ⌊y⌋ = ⌊\frac{x}{n}⌋$
160	159	oveq2d	$⊢ y = \frac{x}{n} \to (1 \dots ⌊y⌋) = (1 \dots ⌊\frac{x}{n}⌋)$
161	160	sumeq1d	$⊢ y = \frac{x}{n} \to \sum_{m = 1}^{⌊y⌋} Λ (m) \log m = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m$
162	158 161	eqtrid	$⊢ y = \frac{x}{n} \to \sum_{k = 1}^{⌊y⌋} Λ (k) \log k = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m$
163		fveq2	$⊢ y = \frac{x}{n} \to ψ (y) = ψ (\frac{x}{n})$
164		fveq2	$⊢ y = \frac{x}{n} \to \log y = \log (\frac{x}{n})$
165	163 164	oveq12d	$⊢ y = \frac{x}{n} \to ψ (y) \log y = ψ (\frac{x}{n}) \log (\frac{x}{n})$
166	162 165	oveq12d	$⊢ y = \frac{x}{n} \to \sum_{k = 1}^{⌊y⌋} Λ (k) \log k - ψ (y) \log y = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})$
167		id	$⊢ y = \frac{x}{n} \to y = \frac{x}{n}$
168	166 167	oveq12d	$⊢ y = \frac{x}{n} \to \frac{\sum_{k = 1}^{⌊y⌋} Λ (k) \log k - ψ (y) \log y}{y} = \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})}{\frac{x}{n}}$
169	168	fveq2d	$⊢ y = \frac{x}{n} \to \|\frac{\sum_{k = 1}^{⌊y⌋} Λ (k) \log k - ψ (y) \log y}{y}\| = \|\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})}{\frac{x}{n}}\|$
170	169	breq1d	$⊢ y = \frac{x}{n} \to (\|\frac{\sum_{k = 1}^{⌊y⌋} Λ (k) \log k - ψ (y) \log y}{y}\| \leq A \leftrightarrow \|\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})}{\frac{x}{n}}\| \leq A)$
171	2	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \forall y \in [1, +∞) \|\frac{\sum_{k = 1}^{⌊y⌋} Λ (k) \log k - ψ (y) \log y}{y}\| \leq A$
172	10	nncnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
173	172	mulid2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 n = n$
174		fznnfl	$⊢ x \in ℝ \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
175	37 174	syl	$⊢ (φ \land x \in (1, +∞)) \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
176	175	simplbda	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \leq x$
177	173 176	eqbrtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 n \leq x$
178		1red	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
179	178 141 93	lemuldivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 n \leq x \leftrightarrow 1 \leq \frac{x}{n})$
180	177 179	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x}{n}$
181		1re	$⊢ 1 \in ℝ$
182		elicopnf	$⊢ 1 \in ℝ \to (\frac{x}{n} \in [1, +∞) \leftrightarrow (\frac{x}{n} \in ℝ \land 1 \leq \frac{x}{n}))$
183	181 182	ax-mp	$⊢ \frac{x}{n} \in [1, +∞) \leftrightarrow (\frac{x}{n} \in ℝ \land 1 \leq \frac{x}{n})$
184	89 180 183	sylanbrc	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in [1, +∞)$
185	170 171 184	rspcdva	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})}{\frac{x}{n}}\| \leq A$
186	154 185	eqbrtrrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|}{\frac{x}{n}} \leq A$
187	144 140 127	ledivmul2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|}{\frac{x}{n}} \leq A \leftrightarrow \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\| \leq A (\frac{x}{n}))$
188	186 187	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\| \leq A (\frac{x}{n})$
189	24	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℂ$
190	141	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
191	10	nnne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
192	189 190 172 191	divassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{A x}{n} = A (\frac{x}{n})$
193	188 192	breqtrrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\| \leq \frac{A x}{n}$
194	144 145 12 147 193	lemul2ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\| \leq Λ (n) (\frac{A x}{n})$
195	115 131	absmuld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| = \|Λ (n)\| \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|$
196	12 147	absidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n)\| = Λ (n)$
197	196	oveq1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n)\| \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\| = Λ (n) \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|$
198	195 197	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| = Λ (n) \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})\|$
199	142	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A x \in ℂ$
200	115 172 199 191	div32d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) A x = Λ (n) (\frac{A x}{n})$
201	194 198 200	3brtr4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| \leq (\frac{Λ (n)}{n}) A x$
202	8 135 143 201	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x$
203	37	recnd	$⊢ (φ \land x \in (1, +∞)) \to x \in ℂ$
204	24 203	mulcld	$⊢ (φ \land x \in (1, +∞)) \to A x \in ℂ$
205	115 172 191	divcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
206	8 204 205	fsummulc1	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x$
207	202 206	breqtrrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x$
208	134 136 138 139 207	letrd	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x$
209	124	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℂ$
210	91	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℂ$
211	94	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
212	210 211	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \log n \in ℂ$
213	209 212	addcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n \in ℂ$
214	115 213	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) \in ℂ$
215	115 210	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \in ℂ$
216	27	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log x \in ℂ$
217	215 216	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log x \in ℂ$
218	8 214 217	fsumsub	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) - Λ (n) ψ (\frac{x}{n}) \log x) = \sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x$
219	210 216	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \log x \in ℂ$
220	115 213 219	subdid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n - ψ (\frac{x}{n}) \log x) = Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) - Λ (n) ψ (\frac{x}{n}) \log x$
221	44	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
222	221 93	relogdivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) = \log x - \log n$
223	222	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \log (\frac{x}{n}) = ψ (\frac{x}{n}) (\log x - \log n)$
224	210 216 211	subdid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) (\log x - \log n) = ψ (\frac{x}{n}) \log x - ψ (\frac{x}{n}) \log n$
225	223 224	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \log (\frac{x}{n}) = ψ (\frac{x}{n}) \log x - ψ (\frac{x}{n}) \log n$
226	225	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - (ψ (\frac{x}{n}) \log x - ψ (\frac{x}{n}) \log n)$
227	209 219 212	subsub3d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - (ψ (\frac{x}{n}) \log x - ψ (\frac{x}{n}) \log n) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n - ψ (\frac{x}{n}) \log x$
228	226 227	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n - ψ (\frac{x}{n}) \log x$
229	228	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})) = Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n - ψ (\frac{x}{n}) \log x)$
230	115 210 216	mulassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log x = Λ (n) ψ (\frac{x}{n}) \log x$
231	230	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) - Λ (n) ψ (\frac{x}{n}) \log x = Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) - Λ (n) ψ (\frac{x}{n}) \log x$
232	220 229 231	3eqtr4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})) = Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) - Λ (n) ψ (\frac{x}{n}) \log x$
233	232	sumeq2dv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) - Λ (n) ψ (\frac{x}{n}) \log x)$
234		fveq2	$⊢ n = m \to Λ (n) = Λ (m)$
235		oveq2	$⊢ n = m \to \frac{x}{n} = \frac{x}{m}$
236	235	fveq2d	$⊢ n = m \to ψ (\frac{x}{n}) = ψ (\frac{x}{m})$
237	234 236	oveq12d	$⊢ n = m \to Λ (n) ψ (\frac{x}{n}) = Λ (m) ψ (\frac{x}{m})$
238		fveq2	$⊢ n = m \to \log n = \log m$
239	237 238	oveq12d	$⊢ n = m \to Λ (n) ψ (\frac{x}{n}) \log n = Λ (m) ψ (\frac{x}{m}) \log m$
240	239	cbvsumv	$⊢ \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m$
241		elfznn	$⊢ n \in (1 \dots ⌊\frac{x}{m}⌋) \to n \in ℕ$
242	241	adantl	$⊢ (((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land n \in (1 \dots ⌊\frac{x}{m}⌋)) \to n \in ℕ$
243	242 11	syl	$⊢ (((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land n \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (n) \in ℝ$
244	243	recnd	$⊢ (((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land n \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (n) \in ℂ$
245	244	anasss	$⊢ ((φ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to Λ (n) \in ℂ$
246		elfznn	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℕ$
247	246	adantl	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℕ$
248	247 119	syl	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \in ℝ$
249	248	recnd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \in ℂ$
250	247	nnrpd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℝ^{+}$
251	250	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \log m \in ℝ$
252	251	recnd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \log m \in ℂ$
253	249 252	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \log m \in ℂ$
254	253	adantrr	$⊢ ((φ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to Λ (m) \log m \in ℂ$
255	245 254	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to Λ (n) Λ (m) \log m \in ℂ$
256	37 255	fsumfldivdiag	$⊢ (φ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (n) Λ (m) \log m$
257	37	adantr	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to x \in ℝ$
258	257 247	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \frac{x}{m} \in ℝ$
259		chpcl	$⊢ \frac{x}{m} \in ℝ \to ψ (\frac{x}{m}) \in ℝ$
260	258 259	syl	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) \in ℝ$
261	260	recnd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) \in ℂ$
262	249 261 252	mul32d	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) ψ (\frac{x}{m}) \log m = Λ (m) \log m ψ (\frac{x}{m})$
263	248 251	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \log m \in ℝ$
264	263	recnd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \log m \in ℂ$
265	264 261	mulcomd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \log m ψ (\frac{x}{m}) = ψ (\frac{x}{m}) Λ (m) \log m$
266		chpval	$⊢ \frac{x}{m} \in ℝ \to ψ (\frac{x}{m}) = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n)$
267	258 266	syl	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n)$
268	267	oveq1d	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) Λ (m) \log m = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
269		fzfid	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{m}⌋) \in Fin$
270	269 264 244	fsummulc1	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
271	268 270	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) Λ (m) \log m = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
272	262 265 271	3eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) ψ (\frac{x}{m}) \log m = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
273	272	sumeq2dv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m = \sum_{m = 1}^{⌊x⌋} \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
274	123	recnd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \log m \in ℂ$
275	116 115 274	fsummulc2	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (n) Λ (m) \log m$
276	275	sumeq2dv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (n) Λ (m) \log m$
277	256 273 276	3eqtr4d	$⊢ (φ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m = \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m$
278	240 277	eqtrid	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m$
279	115 210 211	mulassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n = Λ (n) ψ (\frac{x}{n}) \log n$
280	279	sumeq2dv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
281	278 280	oveq12d	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
282	105	2timesd	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
283	115 209	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℂ$
284	115 212	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
285	8 283 284	fsumadd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + Λ (n) ψ (\frac{x}{n}) \log n) = \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
286	281 282 285	3eqtr4d	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = \sum_{n = 1}^{⌊x⌋} (Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + Λ (n) ψ (\frac{x}{n}) \log n)$
287	115 209 212	adddid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) = Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + Λ (n) ψ (\frac{x}{n}) \log n$
288	287	sumeq2dv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) = \sum_{n = 1}^{⌊x⌋} (Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + Λ (n) ψ (\frac{x}{n}) \log n)$
289	286 288	eqtr4d	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = \sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n)$
290	92	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \in ℂ$
291	8 27 290	fsummulc1	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x = \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x$
292	289 291	oveq12d	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x = \sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (\frac{x}{n}) \log n) - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x$
293	218 233 292	3eqtr4rd	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x = \sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))$
294	293	fveq2d	$⊢ (φ \land x \in (1, +∞)) \to \|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\| = \|\sum_{n = 1}^{⌊x⌋} Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - ψ (\frac{x}{n}) \log (\frac{x}{n}))\|$
295	25 24 203	mulassd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x$
296	208 294 295	3brtr4d	$⊢ (φ \land x \in (1, +∞)) \to \|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x$
297	110 114 44	ledivmul2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x} \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A \leftrightarrow \|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A x)$
298	296 297	mpbird	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x} \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A$
299	112 114 26 298	lediv1dd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x}}{\log x} \leq \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A}{\log x}$
300	110	recnd	$⊢ (φ \land x \in (1, +∞)) \to \|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\| \in ℂ$
301	300 203 27 111 30	divdiv1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x}}{\log x} = \frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x \log x}$
302	109 27 203 30 111	divdiv32d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{\log x}}{x} = \frac{\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{x}}{\log x}$
303	106 108 27 30	divsubdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{\log x} = (\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{\log x})$
304	104 105 27 30	div23d	$⊢ (φ \land x \in (1, +∞)) \to \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{\log x} = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
305	107 27 30	divcan4d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{\log x} = \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})$
306	304 305	oveq12d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{\log x}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})$
307	303 306	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{\log x} = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})$
308	307	oveq1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{\log x}}{x} = \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}$
309	109 203 27 111 30	divdiv1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{x}}{\log x} = \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{x \log x}$
310	302 308 309	3eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x} = \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{x \log x}$
311	310	fveq2d	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}\| = \|\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{x \log x}\|$
312	44 26	rpmulcld	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℝ^{+}$
313	312	rpcnd	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℂ$
314	312	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to x \log x \neq 0$
315	109 313 314	absdivd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x}{x \log x}\| = \frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{\|x \log x\|}$
316	312	rpred	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℝ$
317	312	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq x \log x$
318	316 317	absidd	$⊢ (φ \land x \in (1, +∞)) \to \|x \log x\| = x \log x$
319	318	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{\|x \log x\|} = \frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x \log x}$
320	311 315 319	3eqtrd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}\| = \frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x \log x}$
321	301 320	eqtr4d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{\|2 \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log x\|}{x}}{\log x} = \|\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}\|$
322	25 24 27 30	divassd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) A}{\log x} = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x})$
323	299 321 322	3brtr3d	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x})$
324	22	leabsd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x}) \leq \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x})\|$
325	102 22 103 323 324	letrd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}\| \leq \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x})\|$
326	325	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \|\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}\| \leq \|\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) (\frac{A}{\log x})\|$
327	3 84 22 101 326	o1le	$⊢ φ \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)$

Metamath Proof Explorer

Theorem selberg3lem1

Proof