pntrlog2bndlem1

	Ref	Expression
Hypotheses	pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
	pntrlog2bnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
Assertion	pntrlog2bndlem1	$⊢ (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x}) \in \leq 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
2		pntrlog2bnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
3		1red	$⊢ ⊤ \to 1 \in ℝ$
4	2	selberg34r	$⊢ (x \in (1, +∞) ⟼ \frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}) \in 𝑂 (1)$
5		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
6	5	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ$
7		1rp	$⊢ 1 \in ℝ^{+}$
8	7	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
9		1red	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ$
10		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
11	10	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
12	11	simpld	$⊢ (⊤ \land x \in (1, +∞)) \to 1 < x$
13	9 6 12	ltled	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \leq x$
14	6 8 13	rpgecld	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ^{+}$
15	2	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
16	15	ffvelcdmi	$⊢ x \in ℝ^{+} \to R (x) \in ℝ$
17	14 16	syl	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \in ℝ$
18	14	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
19	17 18	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x \in ℝ$
20		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
21	14	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
22		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
23	22	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
24	23	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
25	21 24	rpdivcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
26	15	ffvelcdmi	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) \in ℝ$
27	25 26	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℝ$
28		fzfid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots n) \in Fin$
29		dvdsssfz1	$⊢ n \in ℕ \to \{y \in ℕ \| y ∥ n\} \subseteq (1 \dots n)$
30	23 29	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \{y \in ℕ \| y ∥ n\} \subseteq (1 \dots n)$
31	28 30	ssfid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \{y \in ℕ \| y ∥ n\} \in Fin$
32		ssrab2	$⊢ \{y \in ℕ \| y ∥ n\} \subseteq ℕ$
33		simpr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to m \in \{y \in ℕ \| y ∥ n\}$
34	32 33	sselid	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to m \in ℕ$
35		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
36	34 35	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) \in ℝ$
37		dvdsdivcl	$⊢ (n \in ℕ \land m \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{m} \in \{y \in ℕ \| y ∥ n\}$
38	23 37	sylan	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{m} \in \{y \in ℕ \| y ∥ n\}$
39	32 38	sselid	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{m} \in ℕ$
40		vmacl	$⊢ \frac{n}{m} \in ℕ \to Λ (\frac{n}{m}) \in ℝ$
41	39 40	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (\frac{n}{m}) \in ℝ$
42	36 41	remulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) Λ (\frac{n}{m}) \in ℝ$
43	31 42	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) \in ℝ$
44		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
45	23 44	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
46	24	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
47	45 46	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n \in ℝ$
48	43 47	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n \in ℝ$
49	27 48	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) \in ℝ$
50	20 49	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) \in ℝ$
51	6 12	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
52	50 51	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x} \in ℝ$
53	19 52	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x}) \in ℝ$
54	53 14	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x} \in ℝ$
55	54	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x} \in ℂ$
56	55	lo1o12	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ \frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ \|\frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}\|) \in \leq 𝑂 (1))$
57	4 56	mpbii	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \|\frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}\|) \in \leq 𝑂 (1)$
58	55	abscld	$⊢ (⊤ \land x \in (1, +∞)) \to \|\frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}\| \in ℝ$
59	17	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \in ℂ$
60	59	abscld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \in ℝ$
61	60 18	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℝ$
62	27	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℂ$
63	62	abscld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \in ℝ$
64	23	nnred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
65	1	pntsf	$⊢ S : ℝ ⟶ ℝ$
66	65	ffvelcdmi	$⊢ n \in ℝ \to S (n) \in ℝ$
67	64 66	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) \in ℝ$
68		1red	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
69	64 68	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℝ$
70	65	ffvelcdmi	$⊢ n - 1 \in ℝ \to S (n - 1) \in ℝ$
71	69 70	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n - 1) \in ℝ$
72	67 71	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) \in ℝ$
73	63 72	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n) - S (n - 1)) \in ℝ$
74	20 73	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1)) \in ℝ$
75	74 51	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x} \in ℝ$
76	61 75	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x}) \in ℝ$
77	76 14	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x} \in ℝ$
78	18	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
79	59 78	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x \in ℂ$
80	50	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) \in ℂ$
81	51	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
82	80 78 81	divcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x} \in ℂ$
83	79 82	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x}) \in ℂ$
84	83	abscld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\| \in ℝ$
85	80	abscld	$⊢ (⊤ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\| \in ℝ$
86	85 51	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\log x} \in ℝ$
87	61 86	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\log x}) \in ℝ$
88	49	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) \in ℂ$
89	88	abscld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\| \in ℝ$
90	20 89	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\| \in ℝ$
91	20 88	fsumabs	$⊢ (⊤ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\| \leq \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|$
92	48	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n \in ℂ$
93	62 92	absmuld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\| = \|R (\frac{x}{n})\| \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n\|$
94	92	abscld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n\| \in ℝ$
95	62	absge0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|R (\frac{x}{n})\|$
96	43	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) \in ℂ$
97	47	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n \in ℂ$
98	96 97	abs2dif2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n\| \leq \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})\| + \|Λ (n) \log n\|$
99	71	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n - 1) \in ℂ$
100	96 97	addcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) + Λ (n) \log n \in ℂ$
101	99 100	pncan2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n - 1) + (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) + Λ (n) \log n) - S (n - 1) = \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) + Λ (n) \log n$
102		elfzuz	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℤ_{\geq 1}$
103	102	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℤ_{\geq 1}$
104		elfznn	$⊢ k \in (1 \dots n) \to k \in ℕ$
105	104	adantl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to k \in ℕ$
106		vmacl	$⊢ k \in ℕ \to Λ (k) \in ℝ$
107	105 106	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to Λ (k) \in ℝ$
108	105	nnrpd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to k \in ℝ^{+}$
109	108	relogcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to \log k \in ℝ$
110	107 109	remulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to Λ (k) \log k \in ℝ$
111		fzfid	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to (1 \dots k) \in Fin$
112		dvdsssfz1	$⊢ k \in ℕ \to \{y \in ℕ \| y ∥ k\} \subseteq (1 \dots k)$
113	105 112	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to \{y \in ℕ \| y ∥ k\} \subseteq (1 \dots k)$
114	111 113	ssfid	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to \{y \in ℕ \| y ∥ k\} \in Fin$
115		ssrab2	$⊢ \{y \in ℕ \| y ∥ k\} \subseteq ℕ$
116		simpr	$⊢ ((((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \land m \in \{y \in ℕ \| y ∥ k\}) \to m \in \{y \in ℕ \| y ∥ k\}$
117	115 116	sselid	$⊢ ((((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \land m \in \{y \in ℕ \| y ∥ k\}) \to m \in ℕ$
118	117 35	syl	$⊢ ((((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \land m \in \{y \in ℕ \| y ∥ k\}) \to Λ (m) \in ℝ$
119		dvdsdivcl	$⊢ (k \in ℕ \land m \in \{y \in ℕ \| y ∥ k\}) \to \frac{k}{m} \in \{y \in ℕ \| y ∥ k\}$
120	105 119	sylan	$⊢ ((((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \land m \in \{y \in ℕ \| y ∥ k\}) \to \frac{k}{m} \in \{y \in ℕ \| y ∥ k\}$
121	115 120	sselid	$⊢ ((((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \land m \in \{y \in ℕ \| y ∥ k\}) \to \frac{k}{m} \in ℕ$
122		vmacl	$⊢ \frac{k}{m} \in ℕ \to Λ (\frac{k}{m}) \in ℝ$
123	121 122	syl	$⊢ ((((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \land m \in \{y \in ℕ \| y ∥ k\}) \to Λ (\frac{k}{m}) \in ℝ$
124	118 123	remulcld	$⊢ ((((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \land m \in \{y \in ℕ \| y ∥ k\}) \to Λ (m) Λ (\frac{k}{m}) \in ℝ$
125	114 124	fsumrecl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}) \in ℝ$
126	110 125	readdcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}) \in ℝ$
127	126	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land k \in (1 \dots n)) \to Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}) \in ℂ$
128		fveq2	$⊢ k = n \to Λ (k) = Λ (n)$
129		fveq2	$⊢ k = n \to \log k = \log n$
130	128 129	oveq12d	$⊢ k = n \to Λ (k) \log k = Λ (n) \log n$
131		breq2	$⊢ k = n \to (y ∥ k \leftrightarrow y ∥ n)$
132	131	rabbidv	$⊢ k = n \to \{y \in ℕ \| y ∥ k\} = \{y \in ℕ \| y ∥ n\}$
133		fvoveq1	$⊢ k = n \to Λ (\frac{k}{m}) = Λ (\frac{n}{m})$
134	133	oveq2d	$⊢ k = n \to Λ (m) Λ (\frac{k}{m}) = Λ (m) Λ (\frac{n}{m})$
135	134	adantr	$⊢ (k = n \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) Λ (\frac{k}{m}) = Λ (m) Λ (\frac{n}{m})$
136	132 135	sumeq12rdv	$⊢ k = n \to \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}) = \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
137	130 136	oveq12d	$⊢ k = n \to Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}) = Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
138	103 127 137	fsumm1	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{k = 1}^{n} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m})) = \sum_{k = 1}^{n - 1} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m})) + Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
139	1	pntsval2	$⊢ n \in ℝ \to S (n) = \sum_{k = 1}^{⌊n⌋} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}))$
140	64 139	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) = \sum_{k = 1}^{⌊n⌋} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}))$
141	23	nnzd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℤ$
142		flid	$⊢ n \in ℤ \to ⌊n⌋ = n$
143	141 142	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ⌊n⌋ = n$
144	143	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊n⌋) = (1 \dots n)$
145	144	sumeq1d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{k = 1}^{⌊n⌋} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m})) = \sum_{k = 1}^{n} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}))$
146	140 145	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) = \sum_{k = 1}^{n} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}))$
147	1	pntsval2	$⊢ n - 1 \in ℝ \to S (n - 1) = \sum_{k = 1}^{⌊n - 1⌋} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}))$
148	69 147	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n - 1) = \sum_{k = 1}^{⌊n - 1⌋} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}))$
149		1zzd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℤ$
150	141 149	zsubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℤ$
151		flid	$⊢ n - 1 \in ℤ \to ⌊n - 1⌋ = n - 1$
152	150 151	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ⌊n - 1⌋ = n - 1$
153	152	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊n - 1⌋) = (1 \dots n - 1)$
154	153	sumeq1d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{k = 1}^{⌊n - 1⌋} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m})) = \sum_{k = 1}^{n - 1} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}))$
155	148 154	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n - 1) = \sum_{k = 1}^{n - 1} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m}))$
156	96 97	addcomd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) + Λ (n) \log n = Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
157	155 156	oveq12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n - 1) + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) + Λ (n) \log n = \sum_{k = 1}^{n - 1} (Λ (k) \log k + \sum_{m \in \{y \in ℕ \| y ∥ k\}} Λ (m) Λ (\frac{k}{m})) + Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
158	138 146 157	3eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) = S (n - 1) + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) + Λ (n) \log n$
159	158	oveq1d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) = S (n - 1) + (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) + Λ (n) \log n) - S (n - 1)$
160		vmage0	$⊢ m \in ℕ \to 0 \leq Λ (m)$
161	34 160	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to 0 \leq Λ (m)$
162		vmage0	$⊢ \frac{n}{m} \in ℕ \to 0 \leq Λ (\frac{n}{m})$
163	39 162	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to 0 \leq Λ (\frac{n}{m})$
164	36 41 161 163	mulge0d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to 0 \leq Λ (m) Λ (\frac{n}{m})$
165	31 42 164	fsumge0	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
166	43 165	absidd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})\| = \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
167		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
168	23 167	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n)$
169	23	nnge1d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq n$
170	64 169	logge0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \log n$
171	45 46 168 170	mulge0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n) \log n$
172	47 171	absidd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|Λ (n) \log n\| = Λ (n) \log n$
173	166 172	oveq12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})\| + \|Λ (n) \log n\| = \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) + Λ (n) \log n$
174	101 159 173	3eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) = \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})\| + \|Λ (n) \log n\|$
175	98 174	breqtrrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n\| \leq S (n) - S (n - 1)$
176	94 72 63 95 175	lemul2ad	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \|\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n\| \leq \|R (\frac{x}{n})\| (S (n) - S (n - 1))$
177	93 176	eqbrtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\| \leq \|R (\frac{x}{n})\| (S (n) - S (n - 1))$
178	20 89 73 177	fsumle	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\| \leq \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))$
179	85 90 74 91 178	letrd	$⊢ (⊤ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\| \leq \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))$
180	85 74 51 179	lediv1dd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\log x} \leq \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x}$
181	86 75 61 180	lesub2dd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x}) \leq \|R (x)\| \log x - (\frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\log x})$
182	59 78	absmuld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x) \log x\| = \|R (x)\| \|\log x\|$
183	6 13	logge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq \log x$
184	18 183	absidd	$⊢ (⊤ \land x \in (1, +∞)) \to \|\log x\| = \log x$
185	184	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \|\log x\| = \|R (x)\| \log x$
186	182 185	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x) \log x\| = \|R (x)\| \log x$
187	80 78 81	absdivd	$⊢ (⊤ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\|\log x\|}$
188	184	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\|\log x\|} = \frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\log x}$
189	187 188	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\log x}$
190	186 189	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x) \log x\| - \|\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x}\| = \|R (x)\| \log x - (\frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\log x})$
191	79 82	abs2difd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x) \log x\| - \|\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x}\| \leq \|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\|$
192	190 191	eqbrtrrd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{\|\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)\|}{\log x}) \leq \|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\|$
193	76 87 84 181 192	letrd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x}) \leq \|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\|$
194	76 84 14 193	lediv1dd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x} \leq \frac{\|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\|}{x}$
195	53	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x}) \in ℂ$
196	6	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℂ$
197	14	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \neq 0$
198	195 196 197	absdivd	$⊢ (⊤ \land x \in (1, +∞)) \to \|\frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}\| = \frac{\|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\|}{\|x\|}$
199	14	rpge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq x$
200	6 199	absidd	$⊢ (⊤ \land x \in (1, +∞)) \to \|x\| = x$
201	200	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\|}{\|x\|} = \frac{\|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\|}{x}$
202	198 201	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \|\frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}\| = \frac{\|R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})\|}{x}$
203	194 202	breqtrrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x} \leq \|\frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}\|$
204	203	adantrr	$⊢ (⊤ \land (x \in (1, +∞) \land 1 \leq x)) \to \frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x} \leq \|\frac{R (x) \log x - (\frac{\sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{\log x})}{x}\|$
205	3 57 58 77 204	lo1le	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x}) \in \leq 𝑂 (1)$
206	205	mptru	$⊢ (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x}) \in \leq 𝑂 (1)$

Metamath Proof Explorer

Theorem pntrlog2bndlem1

Proof