selberg34r

		Ref	Expression
	Hypothesis	pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		2re	$⊢ 2 \in ℝ$
3	2	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℝ$
4		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
5	4	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ$
6		1rp	$⊢ 1 \in ℝ^{+}$
7	6	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
8		1red	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ$
9		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
10	9	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
11	10	simpld	$⊢ (⊤ \land x \in (1, +∞)) \to 1 < x$
12	8 5 11	ltled	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \leq x$
13	5 7 12	rpgecld	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ^{+}$
14	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
15	14	ffvelcdmi	$⊢ x \in ℝ^{+} \to R (x) \in ℝ$
16	13 15	syl	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \in ℝ$
17	13	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
18	16 17	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x \in ℝ$
19	3 18	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x \in ℝ$
20	19	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x \in ℂ$
21	5 11	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
22	3 21	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
23	22	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℂ$
24		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
25	13	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
26		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
27	26	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
28	27	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
29	25 28	rpdivcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
30	14	ffvelcdmi	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) \in ℝ$
31	29 30	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℝ$
32		fzfid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots n) \in Fin$
33		dvdsssfz1	$⊢ n \in ℕ \to \{y \in ℕ \| y ∥ n\} \subseteq (1 \dots n)$
34	27 33	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \{y \in ℕ \| y ∥ n\} \subseteq (1 \dots n)$
35	32 34	ssfid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \{y \in ℕ \| y ∥ n\} \in Fin$
36		ssrab2	$⊢ \{y \in ℕ \| y ∥ n\} \subseteq ℕ$
37		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\}$
38	36 37	sselid	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to m \in ℕ$
39		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
40	38 39	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) \in ℝ$
41		dvdsdivcl	$⊢ (n \in ℕ \land m \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{m} \in \{y \in ℕ \| y ∥ n\}$
42	27 41	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\}$
43	36 42	sselid	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{m} \in ℕ$
44		vmacl	$⊢ \frac{n}{m} \in ℕ \to Λ (\frac{n}{m}) \in ℝ$
45	43 44	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (\frac{n}{m}) \in ℝ$
46	40 45	remulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) Λ (\frac{n}{m}) \in ℝ$
47	35 46	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) \in ℝ$
48		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
49	27 48	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
50	28	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
51	49 50	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n \in ℝ$
52	47 51	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 ℝ$
53	31 52	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 ℝ$
54	24 53	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 ℝ$
55	54	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 ℂ$
56	23 55	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) \in ℂ$
57	20 56	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) \in ℂ$
58	5	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℂ$
59		2cnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℂ$
60	13	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \neq 0$
61		2ne0	$⊢ 2 \neq 0$
62	61	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \neq 0$
63	57 58 59 60 62	divdiv32d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x}}{2} = \frac{\frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{2}}{x}$
64	57 58 60	divcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x} \in ℂ$
65	64 59 62	divrecd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x}}{2} = (\frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x}) (\frac{1}{2})$
66	20 56 59 62	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{2} = (\frac{2 R (x) \log x}{2}) - (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{2})$
67	18	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x \in ℂ$
68	67 59 62	divcan3d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 R (x) \log x}{2} = R (x) \log x$
69	21	rpcnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
70	21	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
71	59 69 55 70	div32d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) = 2 (\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})$
72	71	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{2} = \frac{2 (\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})}{2}$
73	54 21	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 ℝ$
74	73	recnd	$⊢ (⊤ \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 ℂ$
75	74 59 62	divcan3d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 (\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})}{2} = \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}$
76	72 75	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{2} = \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}$
77	68 76	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2 R (x) \log x}{2}) - (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{2}) = 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})$
78	66 77	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{2} = 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})$
79	78	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{2}}{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}$
80	63 65 79	3eqtr3d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x}) (\frac{1}{2}) = \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}$
81	80	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x}) (\frac{1}{2})) = (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})$
82	22 54	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) \in ℝ$
83	19 82	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) \in ℝ$
84	83 13	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x} \in ℝ$
85	8	rehalfcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{1}{2} \in ℝ$
86	31	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℂ$
87	47	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) \in ℂ$
88	49	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
89	50	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
90	88 89	mulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n \in ℂ$
91	86 87 90	subdid	$⊢ ((⊤ \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}) - R (\frac{x}{n}) Λ (n) \log n$
92	86 88 89	mul12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) Λ (n) \log n = Λ (n) R (\frac{x}{n}) \log n$
93	88 86 89	mulassd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) R (\frac{x}{n}) \log n = Λ (n) R (\frac{x}{n}) \log n$
94	92 93	eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) Λ (n) \log n = Λ (n) R (\frac{x}{n}) \log n$
95	94	oveq2d	$⊢ ((⊤ \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}) - R (\frac{x}{n}) Λ (n) \log n = R (\frac{x}{n}) \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) R (\frac{x}{n}) \log n$
96	91 95	eqtrd	$⊢ ((⊤ \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) R (\frac{x}{n}) \log n$
97	96	sumeq2dv	$⊢ (⊤ \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) = \sum_{n = 1}^{⌊x⌋} (R (\frac{x}{n}) \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) R (\frac{x}{n}) \log n)$
98	86 87	mulcld	$⊢ ((⊤ \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}) \in ℂ$
99	88 86	mulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) R (\frac{x}{n}) \in ℂ$
100	99 89	mulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) R (\frac{x}{n}) \log n \in ℂ$
101	24 98 100	fsumsub	$⊢ (⊤ \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) R (\frac{x}{n}) \log n) = \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
102	46	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) Λ (\frac{n}{m}) \in ℂ$
103	35 86 102	fsummulc2	$⊢ ((⊤ \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}) = \sum_{m \in \{y \in ℕ \| y ∥ n\}} R (\frac{x}{n}) Λ (m) Λ (\frac{n}{m})$
104	103	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) = \sum_{n = 1}^{⌊x⌋} \sum_{m \in \{y \in ℕ \| y ∥ n\}} R (\frac{x}{n}) Λ (m) Λ (\frac{n}{m})$
105		oveq2	$⊢ n = m k \to \frac{x}{n} = \frac{x}{m k}$
106	105	fveq2d	$⊢ n = m k \to R (\frac{x}{n}) = R (\frac{x}{m k})$
107		fvoveq1	$⊢ n = m k \to Λ (\frac{n}{m}) = Λ (\frac{m k}{m})$
108	107	oveq2d	$⊢ n = m k \to Λ (m) Λ (\frac{n}{m}) = Λ (m) Λ (\frac{m k}{m})$
109	106 108	oveq12d	$⊢ n = m k \to R (\frac{x}{n}) Λ (m) Λ (\frac{n}{m}) = R (\frac{x}{m k}) Λ (m) Λ (\frac{m k}{m})$
110	31	adantrr	$⊢ ((⊤ \land x \in (1, +∞)) \land (n \in (1 \dots ⌊x⌋) \land m \in \{y \in ℕ \| y ∥ n\})) \to R (\frac{x}{n}) \in ℝ$
111	40	anasss	$⊢ ((⊤ \land x \in (1, +∞)) \land (n \in (1 \dots ⌊x⌋) \land m \in \{y \in ℕ \| y ∥ n\})) \to Λ (m) \in ℝ$
112	45	anasss	$⊢ ((⊤ \land x \in (1, +∞)) \land (n \in (1 \dots ⌊x⌋) \land m \in \{y \in ℕ \| y ∥ n\})) \to Λ (\frac{n}{m}) \in ℝ$
113	111 112	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land (n \in (1 \dots ⌊x⌋) \land m \in \{y \in ℕ \| y ∥ n\})) \to Λ (m) Λ (\frac{n}{m}) \in ℝ$
114	110 113	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land (n \in (1 \dots ⌊x⌋) \land m \in \{y \in ℕ \| y ∥ n\})) \to R (\frac{x}{n}) Λ (m) Λ (\frac{n}{m}) \in ℝ$
115	114	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land (n \in (1 \dots ⌊x⌋) \land m \in \{y \in ℕ \| y ∥ n\})) \to R (\frac{x}{n}) Λ (m) Λ (\frac{n}{m}) \in ℂ$
116	109 5 115	dvdsflsumcom	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \sum_{m \in \{y \in ℕ \| y ∥ n\}} R (\frac{x}{n}) Λ (m) Λ (\frac{n}{m}) = \sum_{m = 1}^{⌊x⌋} \sum_{k = 1}^{⌊\frac{x}{m}⌋} R (\frac{x}{m k}) Λ (m) Λ (\frac{m k}{m})$
117	58	ad2antrr	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to x \in ℂ$
118		elfznn	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℕ$
119	118	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℕ$
120	119	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℝ^{+}$
121	120	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to m \in ℝ^{+}$
122	121	rpcnd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to m \in ℂ$
123		elfznn	$⊢ k \in (1 \dots ⌊\frac{x}{m}⌋) \to k \in ℕ$
124	123	adantl	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to k \in ℕ$
125	124	nncnd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to k \in ℂ$
126	121	rpne0d	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to m \neq 0$
127	124	nnne0d	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to k \neq 0$
128	117 122 125 126 127	divdiv1d	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to \frac{\frac{x}{m}}{k} = \frac{x}{m k}$
129	128	eqcomd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to \frac{x}{m k} = \frac{\frac{x}{m}}{k}$
130	129	fveq2d	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to R (\frac{x}{m k}) = R (\frac{\frac{x}{m}}{k})$
131	125 122 126	divcan3d	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to \frac{m k}{m} = k$
132	131	fveq2d	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (\frac{m k}{m}) = Λ (k)$
133	132	oveq2d	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (m) Λ (\frac{m k}{m}) = Λ (m) Λ (k)$
134	130 133	oveq12d	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to R (\frac{x}{m k}) Λ (m) Λ (\frac{m k}{m}) = R (\frac{\frac{x}{m}}{k}) Λ (m) Λ (k)$
135	13	ad2antrr	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to x \in ℝ^{+}$
136	135 121	rpdivcld	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to \frac{x}{m} \in ℝ^{+}$
137	124	nnrpd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to k \in ℝ^{+}$
138	136 137	rpdivcld	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to \frac{\frac{x}{m}}{k} \in ℝ^{+}$
139	14	ffvelcdmi	$⊢ \frac{\frac{x}{m}}{k} \in ℝ^{+} \to R (\frac{\frac{x}{m}}{k}) \in ℝ$
140	138 139	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to R (\frac{\frac{x}{m}}{k}) \in ℝ$
141	140	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to R (\frac{\frac{x}{m}}{k}) \in ℂ$
142	119 39	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \in ℝ$
143	142	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \in ℂ$
144	143	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (m) \in ℂ$
145		vmacl	$⊢ k \in ℕ \to Λ (k) \in ℝ$
146	124 145	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (k) \in ℝ$
147	146	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (k) \in ℂ$
148	144 147	mulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (m) Λ (k) \in ℂ$
149	141 148	mulcomd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to R (\frac{\frac{x}{m}}{k}) Λ (m) Λ (k) = Λ (m) Λ (k) R (\frac{\frac{x}{m}}{k})$
150	144 147 141	mulassd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (m) Λ (k) R (\frac{\frac{x}{m}}{k}) = Λ (m) Λ (k) R (\frac{\frac{x}{m}}{k})$
151	134 149 150	3eqtrd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to R (\frac{x}{m k}) Λ (m) Λ (\frac{m k}{m}) = Λ (m) Λ (k) R (\frac{\frac{x}{m}}{k})$
152	151	sumeq2dv	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \sum_{k = 1}^{⌊\frac{x}{m}⌋} R (\frac{x}{m k}) Λ (m) Λ (\frac{m k}{m}) = \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (m) Λ (k) R (\frac{\frac{x}{m}}{k})$
153		fzfid	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{m}⌋) \in Fin$
154	146 140	remulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℝ$
155	154	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℂ$
156	153 143 155	fsummulc2	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) = \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (m) Λ (k) R (\frac{\frac{x}{m}}{k})$
157	152 156	eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \sum_{k = 1}^{⌊\frac{x}{m}⌋} R (\frac{x}{m k}) Λ (m) Λ (\frac{m k}{m}) = Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})$
158	157	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} \sum_{k = 1}^{⌊\frac{x}{m}⌋} R (\frac{x}{m k}) Λ (m) Λ (\frac{m k}{m}) = \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})$
159	104 116 158	3eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) = \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})$
160	159	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n = \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) - \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
161	97 101 160	3eqtrd	$⊢ (⊤ \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) = \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) - \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
162	161	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) = (\frac{2}{\log x}) (\sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) - \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n)$
163	153 154	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℝ$
164	142 163	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℝ$
165	24 164	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℝ$
166	165	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℂ$
167	49 31	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) R (\frac{x}{n}) \in ℝ$
168	167 50	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) R (\frac{x}{n}) \log n \in ℝ$
169	24 168	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n \in ℝ$
170	169	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n \in ℂ$
171	23 166 170	subdid	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) - \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n) = (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
172	162 171	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) = (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
173	172	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) = 2 R (x) \log x - ((\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n)$
174	23 166	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℂ$
175	22 169	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n \in ℝ$
176	175	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n \in ℂ$
177	20 174 176	subsub3d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x - ((\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n) = 2 R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})$
178	173 177	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) = 2 R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})$
179	67	2timesd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x = R (x) \log x + R (x) \log x$
180	179	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n = R (x) \log x + R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
181	67 176 67	add32d	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n + R (x) \log x = R (x) \log x + R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
182	180 181	eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n = R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n + R (x) \log x$
183	182	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) = (R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n) + R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})$
184	18 175	readdcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n \in ℝ$
185	184	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n \in ℂ$
186	185 67 174	addsubassd	$⊢ (⊤ \land x \in (1, +∞)) \to (R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n) + R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) = R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n + (R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}))$
187	178 183 186	3eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n) = R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n + (R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}))$
188	187	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x} = \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n + (R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}))}{x}$
189	67 174	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℂ$
190	185 189 58 60	divdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n + (R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}))}{x} = (\frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) + (\frac{R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})}{x})$
191	188 190	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x} = (\frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) + (\frac{R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})}{x})$
192	191	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x}) = (x \in (1, +∞) ⟼ (\frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) + (\frac{R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})}{x}))$
193	184 13	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x} \in ℝ$
194	22 165	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℝ$
195	18 194	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k}) \in ℝ$
196	195 13	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})}{x} \in ℝ$
197	1	selberg3r	$⊢ (x \in (1, +∞) ⟼ \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) \in 𝑂 (1)$
198	197	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) \in 𝑂 (1)$
199	1	selberg4r	$⊢ (x \in (1, +∞) ⟼ \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})}{x}) \in 𝑂 (1)$
200	199	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})}{x}) \in 𝑂 (1)$
201	193 196 198 200	o1add2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) + (\frac{R (x) \log x - (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) \sum_{k = 1}^{⌊\frac{x}{m}⌋} Λ (k) R (\frac{\frac{x}{m}}{k})}{x})) \in 𝑂 (1)$
202	192 201	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x}) \in 𝑂 (1)$
203		ioossre	$⊢ (1, +∞) \subseteq ℝ$
204		1cnd	$⊢ ⊤ \to 1 \in ℂ$
205	204	halfcld	$⊢ ⊤ \to \frac{1}{2} \in ℂ$
206		o1const	$⊢ ((1, +∞) \subseteq ℝ \land \frac{1}{2} \in ℂ) \to (x \in (1, +∞) ⟼ \frac{1}{2}) \in 𝑂 (1)$
207	203 205 206	sylancr	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{1}{2}) \in 𝑂 (1)$
208	84 85 202 207	o1mul2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{2 R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} R (\frac{x}{n}) (\sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) - Λ (n) \log n)}{x}) (\frac{1}{2})) \in 𝑂 (1)$
209	81 208	eqeltrrd	$⊢ ⊤ \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)$
210	209	mptru	$⊢ (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)$

Metamath Proof Explorer

Theorem selberg34r

Proof