selberg4lem1

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

	Ref	Expression
Hypotheses	selberg4lem1.1	$⊢ φ \to A \in ℝ^{+}$
	selberg4lem1.2	$⊢ φ \to \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq A$
Assertion	selberg4lem1	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		selberg4lem1.1	$⊢ φ \to A \in ℝ^{+}$
2		selberg4lem1.2	$⊢ φ \to \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq A$
3		2cnd	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℂ$
4		fzfid	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
5		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
6	5	adantl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
7		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
8	6 7	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
9	8 6	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
10		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
11	10	adantl	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ$
12		1rp	$⊢ 1 \in ℝ^{+}$
13	12	a1i	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
14		1red	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ$
15		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
16	15	adantl	$⊢ (φ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
17	16	simpld	$⊢ (φ \land x \in (1, +∞)) \to 1 < x$
18	14 11 17	ltled	$⊢ (φ \land x \in (1, +∞)) \to 1 \leq x$
19	11 13 18	rpgecld	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ^{+}$
20	19	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
21	6	nnrpd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
22	20 21	rpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
23	22	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
24	9 23	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℝ$
25	4 24	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℝ$
26	11 17	rplogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
27	25 26	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} \in ℝ$
28	27	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} \in ℂ$
29	19	relogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ$
30	29	rehalfcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℝ$
31	30	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℂ$
32	3 28 31	subdid	$⊢ (φ \land x \in (1, +∞)) \to 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) = 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - 2 (\frac{\log x}{2})$
33	29	recnd	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℂ$
34		2ne0	$⊢ 2 \neq 0$
35	34	a1i	$⊢ (φ \land x \in (1, +∞)) \to 2 \neq 0$
36	33 3 35	divcan2d	$⊢ (φ \land x \in (1, +∞)) \to 2 (\frac{\log x}{2}) = \log x$
37	36	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - 2 (\frac{\log x}{2}) = 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x$
38	32 37	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) = 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x$
39	38	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}))) = (x \in (1, +∞) ⟼ 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x)$
40		2re	$⊢ 2 \in ℝ$
41	40	a1i	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℝ$
42	27 30	resubcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}) \in ℝ$
43		ioossre	$⊢ (1, +∞) \subseteq ℝ$
44		2cn	$⊢ 2 \in ℂ$
45		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 2 \in ℂ) \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
46	43 44 45	mp2an	$⊢ (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
47	46	a1i	$⊢ φ \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
48		vmalogdivsum2	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
49	48	a1i	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
50	41 42 47 49	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - (\frac{\log x}{2}))) \in 𝑂 (1)$
51	39 50	eqeltrrd	$⊢ φ \to (x \in (1, +∞) ⟼ 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x) \in 𝑂 (1)$
52		fzfid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
53		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
54	53	adantl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
55		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
56	54 55	syl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \in ℝ$
57	54	nnrpd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℝ^{+}$
58	57	relogcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log m \in ℝ$
59	11	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
60	59 6	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
61	60	adantr	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{x}{n} \in ℝ$
62	61 54	nndivred	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{x}{n}}{m} \in ℝ$
63		chpcl	$⊢ \frac{\frac{x}{n}}{m} \in ℝ \to ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
64	62 63	syl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
65	58 64	readdcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log m + ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
66	56 65	remulcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℝ$
67	52 66	fsumrecl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℝ$
68	8 67	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℝ$
69	4 68	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℝ$
70	19 26	rpmulcld	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℝ^{+}$
71	69 70	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x} \in ℝ$
72	71 29	resubcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x \in ℝ$
73	72	recnd	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x \in ℂ$
74	25	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
75	26	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to \log x \neq 0$
76	74 33 75	divcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} \in ℂ$
77	3 76	mulcld	$⊢ (φ \land x \in (1, +∞)) \to 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) \in ℂ$
78	77 33	subcld	$⊢ (φ \land x \in (1, +∞)) \to 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x \in ℂ$
79	71	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x} \in ℂ$
80	79 77 33	nnncan2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x - (2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x) = (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x})$
81	69	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℂ$
82	11	recnd	$⊢ (φ \land x \in (1, +∞)) \to x \in ℂ$
83	19	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to x \neq 0$
84	81 82 33 83 75	divdiv1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}}{\log x} = \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}$
85	3 74 33 75	divassd	$⊢ (φ \land x \in (1, +∞)) \to \frac{2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} = 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x})$
86	84 85	oveq12d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}}{\log x}) - (\frac{2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) = (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x})$
87	69 19	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} \in ℝ$
88	87	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} \in ℂ$
89	3 74	mulcld	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
90	88 89 33 75	divsubdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} = (\frac{\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}}{\log x}) - (\frac{2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x})$
91	83	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \neq 0$
92	68 59 91	redivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} \in ℝ$
93	92	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} \in ℂ$
94	40	a1i	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℝ$
95	94 24	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℝ$
96	95	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
97	4 93 96	fsumsub	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - \sum_{n = 1}^{⌊x⌋} 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
98	8	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
99	67 59 91	redivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} \in ℝ$
100	99	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} \in ℂ$
101		2cnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
102	23	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
103	6	nncnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
104	6	nnne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
105	102 103 104	divcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{n})}{n} \in ℂ$
106	101 105	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{n}) \in ℂ$
107	98 100 106	subdid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) = Λ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - Λ (n) 2 (\frac{\log (\frac{x}{n})}{n})$
108	67	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℂ$
109	82	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
110	98 108 109 91	divassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} = Λ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x})$
111	98 103 102 104	div32d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = Λ (n) (\frac{\log (\frac{x}{n})}{n})$
112	111	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = 2 Λ (n) (\frac{\log (\frac{x}{n})}{n})$
113	101 98 105	mul12d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 Λ (n) (\frac{\log (\frac{x}{n})}{n}) = Λ (n) 2 (\frac{\log (\frac{x}{n})}{n})$
114	112 113	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = Λ (n) 2 (\frac{\log (\frac{x}{n})}{n})$
115	110 114	oveq12d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = Λ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - Λ (n) 2 (\frac{\log (\frac{x}{n})}{n})$
116	107 115	eqtr4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) = (\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
117	116	sumeq2dv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) = \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n}))$
118	68	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℂ$
119	4 82 118 83	fsumdivc	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x})$
120	24	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
121	4 3 120	fsummulc2	$⊢ (φ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
122	119 121	oveq12d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - \sum_{n = 1}^{⌊x⌋} 2 (\frac{Λ (n)}{n}) \log (\frac{x}{n})$
123	97 117 122	3eqtr4rd	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))$
124	123	oveq1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{(\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x} = \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x}$
125	90 124	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}}{\log x}) - (\frac{2 \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) = \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x}$
126	80 86 125	3eqtr2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x - (2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x) = \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x}$
127	126	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x - (2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x)) = (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x})$
128		1red	$⊢ φ \to 1 \in ℝ$
129	1	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ^{+}$
130	129	rpred	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ$
131	4 9	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℝ$
132	131 26	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x} \in ℝ$
133	1	rpcnd	$⊢ φ \to A \in ℂ$
134		o1const	$⊢ ((1, +∞) \subseteq ℝ \land A \in ℂ) \to (x \in (1, +∞) ⟼ A) \in 𝑂 (1)$
135	43 133 134	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ A) \in 𝑂 (1)$
136		1cnd	$⊢ φ \to 1 \in ℂ$
137		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 1 \in ℂ) \to (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
138	43 136 137	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
139	132	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x} \in ℂ$
140		1cnd	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℂ$
141	131	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
142	141 33 33 75	divsubdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x}{\log x} = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - (\frac{\log x}{\log x})$
143	141 33	subcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℂ$
144	143 33 75	divrecd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x}{\log x} = (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x})$
145	33 75	dividd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x}{\log x} = 1$
146	145	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - (\frac{\log x}{\log x}) = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1$
147	142 144 146	3eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x}) = (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1$
148	147	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x})) = (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1)$
149	131 29	resubcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℝ$
150	14 26	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{1}{\log x} \in ℝ$
151	19	ex	$⊢ φ \to (x \in (1, +∞) \to x \in ℝ^{+})$
152	151	ssrdv	$⊢ φ \to (1, +∞) \subseteq ℝ^{+}$
153		vmadivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
154	153	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
155	152 154	o1res2	$⊢ φ \to (x \in (1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
156		divlogrlim	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0$
157		rlimo1	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0 \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
158	156 157	mp1i	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
159	149 150 155 158	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ (\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) (\frac{1}{\log x})) \in 𝑂 (1)$
160	148 159	eqeltrrd	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) - 1) \in 𝑂 (1)$
161	139 140 160	o1dif	$⊢ φ \to ((x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ 1) \in 𝑂 (1))$
162	138 161	mpbird	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) \in 𝑂 (1)$
163	130 132 135 162	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x})) \in 𝑂 (1)$
164	130 132	remulcld	$⊢ (φ \land x \in (1, +∞)) \to A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}) \in ℝ$
165	23 6	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{n})}{n} \in ℝ$
166	94 165	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{n}) \in ℝ$
167	99 166	resubcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}) \in ℝ$
168	8 167	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) \in ℝ$
169	4 168	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) \in ℝ$
170	169 26	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x} \in ℝ$
171	170	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x} \in ℂ$
172	169	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) \in ℂ$
173	172	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| \in ℝ$
174	130 131	remulcld	$⊢ (φ \land x \in (1, +∞)) \to A \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℝ$
175	100 106	subcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}) \in ℂ$
176	98 175	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) \in ℂ$
177	176	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| \in ℝ$
178	4 177	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| \in ℝ$
179	168	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) \in ℂ$
180	4 179	fsumabs	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} \|Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\|$
181	130	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℝ$
182	181 9	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A (\frac{Λ (n)}{n}) \in ℝ$
183	175	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| \in ℝ$
184	181 6	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{A}{n} \in ℝ$
185		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
186	6 185	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n)$
187	108 109 103 91 104	divdiv2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}} = \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) n}{x}$
188	108 103 109 91	div23d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) n}{x} = (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) n$
189	187 188	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}} = (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) n$
190	101 105 103	mulassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{n}) n = 2 (\frac{\log (\frac{x}{n})}{n}) n$
191	102 103 104	divcan1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\log (\frac{x}{n})}{n}) n = \log (\frac{x}{n})$
192	191	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{n}) n = 2 \log (\frac{x}{n})$
193	190 192	eqtr2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \log (\frac{x}{n}) = 2 (\frac{\log (\frac{x}{n})}{n}) n$
194	189 193	oveq12d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}) - 2 \log (\frac{x}{n}) = (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) n - 2 (\frac{\log (\frac{x}{n})}{n}) n$
195	100 106 103	subdird	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) n = (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) n - 2 (\frac{\log (\frac{x}{n})}{n}) n$
196	194 195	eqtr4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}) - 2 \log (\frac{x}{n}) = ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) n$
197	196	fveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}) - 2 \log (\frac{x}{n})\| = \|((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) n\|$
198	175 103	absmuld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})) n\| = \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| \|n\|$
199	6	nnred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
200	21	rpge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq n$
201	199 200	absidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|n\| = n$
202	201	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| \|n\| = \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| n$
203	197 198 202	3eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}) - 2 \log (\frac{x}{n})\| = \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| n$
204		fveq2	$⊢ i = m \to Λ (i) = Λ (m)$
205		fveq2	$⊢ i = m \to \log i = \log m$
206		oveq2	$⊢ i = m \to \frac{y}{i} = \frac{y}{m}$
207	206	fveq2d	$⊢ i = m \to ψ (\frac{y}{i}) = ψ (\frac{y}{m})$
208	205 207	oveq12d	$⊢ i = m \to \log i + ψ (\frac{y}{i}) = \log m + ψ (\frac{y}{m})$
209	204 208	oveq12d	$⊢ i = m \to Λ (i) (\log i + ψ (\frac{y}{i})) = Λ (m) (\log m + ψ (\frac{y}{m}))$
210	209	cbvsumv	$⊢ \sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i})) = \sum_{m = 1}^{⌊y⌋} Λ (m) (\log m + ψ (\frac{y}{m}))$
211		fveq2	$⊢ y = \frac{x}{n} \to ⌊y⌋ = ⌊\frac{x}{n}⌋$
212	211	oveq2d	$⊢ y = \frac{x}{n} \to (1 \dots ⌊y⌋) = (1 \dots ⌊\frac{x}{n}⌋)$
213		fvoveq1	$⊢ y = \frac{x}{n} \to ψ (\frac{y}{m}) = ψ (\frac{\frac{x}{n}}{m})$
214	213	oveq2d	$⊢ y = \frac{x}{n} \to \log m + ψ (\frac{y}{m}) = \log m + ψ (\frac{\frac{x}{n}}{m})$
215	214	oveq2d	$⊢ y = \frac{x}{n} \to Λ (m) (\log m + ψ (\frac{y}{m})) = Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))$
216	215	adantr	$⊢ (y = \frac{x}{n} \land m \in (1 \dots ⌊y⌋)) \to Λ (m) (\log m + ψ (\frac{y}{m})) = Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))$
217	212 216	sumeq12dv	$⊢ y = \frac{x}{n} \to \sum_{m = 1}^{⌊y⌋} Λ (m) (\log m + ψ (\frac{y}{m})) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))$
218	210 217	syl5eq	$⊢ y = \frac{x}{n} \to \sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i})) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))$
219		id	$⊢ y = \frac{x}{n} \to y = \frac{x}{n}$
220	218 219	oveq12d	$⊢ y = \frac{x}{n} \to \frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y} = \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}$
221		fveq2	$⊢ y = \frac{x}{n} \to \log y = \log (\frac{x}{n})$
222	221	oveq2d	$⊢ y = \frac{x}{n} \to 2 \log y = 2 \log (\frac{x}{n})$
223	220 222	oveq12d	$⊢ y = \frac{x}{n} \to (\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y = (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}) - 2 \log (\frac{x}{n})$
224	223	fveq2d	$⊢ y = \frac{x}{n} \to \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| = \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}) - 2 \log (\frac{x}{n})\|$
225	224	breq1d	$⊢ y = \frac{x}{n} \to (\|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq A \leftrightarrow \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}) - 2 \log (\frac{x}{n})\| \leq A)$
226	2	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq A$
227	103	mulid2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 n = n$
228		fznnfl	$⊢ x \in ℝ \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
229	11 228	syl	$⊢ (φ \land x \in (1, +∞)) \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
230	229	simplbda	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \leq x$
231	227 230	eqbrtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 n \leq x$
232		1red	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
233	232 59 21	lemuldivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 n \leq x \leftrightarrow 1 \leq \frac{x}{n})$
234	231 233	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x}{n}$
235		1re	$⊢ 1 \in ℝ$
236		elicopnf	$⊢ 1 \in ℝ \to (\frac{x}{n} \in [1, +∞) \leftrightarrow (\frac{x}{n} \in ℝ \land 1 \leq \frac{x}{n}))$
237	235 236	ax-mp	$⊢ \frac{x}{n} \in [1, +∞) \leftrightarrow (\frac{x}{n} \in ℝ \land 1 \leq \frac{x}{n})$
238	60 234 237	sylanbrc	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in [1, +∞)$
239	225 226 238	rspcdva	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\frac{x}{n}}) - 2 \log (\frac{x}{n})\| \leq A$
240	203 239	eqbrtrrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| n \leq A$
241	183 181 21	lemuldivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| n \leq A \leftrightarrow \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| \leq \frac{A}{n})$
242	240 241	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| \leq \frac{A}{n}$
243	183 184 8 186 242	lemul2ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| \leq Λ (n) (\frac{A}{n})$
244	98 175	absmuld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| = \|Λ (n)\| \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\|$
245	8 186	absidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n)\| = Λ (n)$
246	245	oveq1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n)\| \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\| = Λ (n) \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\|$
247	244 246	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| = Λ (n) \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n})\|$
248	133	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℂ$
249	248 98 103 104	div12d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A (\frac{Λ (n)}{n}) = Λ (n) (\frac{A}{n})$
250	243 247 249	3brtr4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| \leq A (\frac{Λ (n)}{n})$
251	4 177 182 250	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| \leq \sum_{n = 1}^{⌊x⌋} A (\frac{Λ (n)}{n})$
252	133	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℂ$
253	9	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
254	4 252 253	fsummulc2	$⊢ (φ \land x \in (1, +∞)) \to A \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} A (\frac{Λ (n)}{n})$
255	251 254	breqtrrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| \leq A \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})$
256	173 178 174 180 255	letrd	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\| \leq A \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})$
257	173 174 26 256	lediv1dd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\|}{\log x} \leq \frac{A \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}$
258	252 141 33 75	divassd	$⊢ (φ \land x \in (1, +∞)) \to \frac{A \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x} = A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x})$
259	257 258	breqtrd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\|}{\log x} \leq A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x})$
260	172 33 75	absdivd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\|}{\|\log x\|}$
261	26	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \log x$
262	29 261	absidd	$⊢ (φ \land x \in (1, +∞)) \to \|\log x\| = \log x$
263	262	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\|}{\|\log x\|} = \frac{\|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\|}{\log x}$
264	260 263	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))\|}{\log x}$
265	129	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq A$
266	8 21 186	divge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{Λ (n)}{n}$
267	4 9 266	fsumge0	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})$
268	131 26 267	divge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x}$
269	130 132 265 268	mulge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x})$
270	164 269	absidd	$⊢ (φ \land x \in (1, +∞)) \to \|A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x})\| = A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x})$
271	259 264 270	3brtr4d	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x}\| \leq \|A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x})\|$
272	271	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x}\| \leq \|A (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n})}{\log x})\|$
273	128 163 164 171 272	o1le	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}) - 2 (\frac{\log (\frac{x}{n})}{n}))}{\log x}) \in 𝑂 (1)$
274	127 273	eqeltrd	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x - (2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x)) \in 𝑂 (1)$
275	73 78 274	o1dif	$⊢ φ \to ((x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log (\frac{x}{n})}{\log x}) - \log x) \in 𝑂 (1))$
276	51 275	mpbird	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberg4lem1

Proof