pntrlog2bndlem4

Description: Lemma for pntrlog2bnd . Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016)

	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)$
	pntrlog2bnd.t	$⊢ T = (a \in ℝ ⟼ if (a \in ℝ^{+}, a \log a, 0))$
Assertion	pntrlog2bndlem4	$⊢ (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{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		pntrlog2bnd.t	$⊢ T = (a \in ℝ ⟼ if (a \in ℝ^{+}, a \log a, 0))$
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	13	rprege0d	$⊢ (⊤ \land x \in (1, +∞)) \to (x \in ℝ \land 0 \leq x)$
15		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
16	14 15	syl	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ \in ℕ_{0}$
17		nn0p1nn	$⊢ ⌊x⌋ \in ℕ_{0} \to ⌊x⌋ + 1 \in ℕ$
18	16 17	syl	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \in ℕ$
19	18	nnrpd	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \in ℝ^{+}$
20	13 19	rpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} \in ℝ^{+}$
21	2	pntrval	$⊢ \frac{x}{⌊x⌋ + 1} \in ℝ^{+} \to R (\frac{x}{⌊x⌋ + 1}) = ψ (\frac{x}{⌊x⌋ + 1}) - (\frac{x}{⌊x⌋ + 1})$
22	20 21	syl	$⊢ (⊤ \land x \in (1, +∞)) \to R (\frac{x}{⌊x⌋ + 1}) = ψ (\frac{x}{⌊x⌋ + 1}) - (\frac{x}{⌊x⌋ + 1})$
23	5 18	nndivred	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} \in ℝ$
24		2re	$⊢ 2 \in ℝ$
25	24	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℝ$
26		flltp1	$⊢ x \in ℝ \to x < ⌊x⌋ + 1$
27	5 26	syl	$⊢ (⊤ \land x \in (1, +∞)) \to x < ⌊x⌋ + 1$
28	18	nncnd	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \in ℂ$
29	28	mulridd	$⊢ (⊤ \land x \in (1, +∞)) \to (⌊x⌋ + 1) \cdot 1 = ⌊x⌋ + 1$
30	27 29	breqtrrd	$⊢ (⊤ \land x \in (1, +∞)) \to x < (⌊x⌋ + 1) \cdot 1$
31	5 8 19	ltdivmuld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1} < 1 \leftrightarrow x < (⌊x⌋ + 1) \cdot 1)$
32	30 31	mpbird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} < 1$
33		1lt2	$⊢ 1 < 2$
34	33	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 1 < 2$
35	23 8 25 32 34	lttrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} < 2$
36		chpeq0	$⊢ \frac{x}{⌊x⌋ + 1} \in ℝ \to (ψ (\frac{x}{⌊x⌋ + 1}) = 0 \leftrightarrow \frac{x}{⌊x⌋ + 1} < 2)$
37	23 36	syl	$⊢ (⊤ \land x \in (1, +∞)) \to (ψ (\frac{x}{⌊x⌋ + 1}) = 0 \leftrightarrow \frac{x}{⌊x⌋ + 1} < 2)$
38	35 37	mpbird	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (\frac{x}{⌊x⌋ + 1}) = 0$
39	38	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (\frac{x}{⌊x⌋ + 1}) - (\frac{x}{⌊x⌋ + 1}) = 0 - (\frac{x}{⌊x⌋ + 1})$
40	22 39	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to R (\frac{x}{⌊x⌋ + 1}) = 0 - (\frac{x}{⌊x⌋ + 1})$
41	40	fveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{⌊x⌋ + 1})\| = \|0 - (\frac{x}{⌊x⌋ + 1})\|$
42		0red	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \in ℝ$
43	20	rpge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq \frac{x}{⌊x⌋ + 1}$
44	42 23 43	abssuble0d	$⊢ (⊤ \land x \in (1, +∞)) \to \|0 - (\frac{x}{⌊x⌋ + 1})\| = (\frac{x}{⌊x⌋ + 1}) - 0$
45	23	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} \in ℂ$
46	45	subid1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1}) - 0 = \frac{x}{⌊x⌋ + 1}$
47	41 44 46	3eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{⌊x⌋ + 1})\| = \frac{x}{⌊x⌋ + 1}$
48	16	nn0red	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ \in ℝ$
49	1	pntsval2	$⊢ ⌊x⌋ \in ℝ \to S (⌊x⌋) = \sum_{n = 1}^{⌊⌊x⌋⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$
50	48 49	syl	$⊢ (⊤ \land x \in (1, +∞)) \to S (⌊x⌋) = \sum_{n = 1}^{⌊⌊x⌋⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$
51	16	nn0cnd	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ \in ℂ$
52		1cnd	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℂ$
53	51 52	pncand	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ + 1 - 1 = ⌊x⌋$
54	53	fveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to S (⌊x⌋ + 1 - 1) = S (⌊x⌋)$
55	1	pntsval2	$⊢ x \in ℝ \to S (x) = \sum_{n = 1}^{⌊x⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$
56	5 55	syl	$⊢ (⊤ \land x \in (1, +∞)) \to S (x) = \sum_{n = 1}^{⌊x⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$
57		flidm	$⊢ x \in ℝ \to ⌊⌊x⌋⌋ = ⌊x⌋$
58	5 57	syl	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊⌊x⌋⌋ = ⌊x⌋$
59	58	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊⌊x⌋⌋) = (1 \dots ⌊x⌋)$
60	59	sumeq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊⌊x⌋⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})) = \sum_{n = 1}^{⌊x⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$
61	56 60	eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to S (x) = \sum_{n = 1}^{⌊⌊x⌋⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$
62	50 54 61	3eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to S (⌊x⌋ + 1 - 1) = S (x)$
63	53	fveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to T (⌊x⌋ + 1 - 1) = T (⌊x⌋)$
64	63	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 T (⌊x⌋ + 1 - 1) = 2 T (⌊x⌋)$
65	62 64	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1) = S (x) - 2 T (⌊x⌋)$
66	47 65	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{⌊x⌋ + 1})\| (S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1)) = (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋))$
67	5	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℂ$
68	67	div1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x}{1} = x$
69	68	fveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to R (\frac{x}{1}) = R (x)$
70	2	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
71	70	ffvelcdmi	$⊢ x \in ℝ^{+} \to R (x) \in ℝ$
72	13 71	syl	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \in ℝ$
73	69 72	eqeltrd	$⊢ (⊤ \land x \in (1, +∞)) \to R (\frac{x}{1}) \in ℝ$
74	73	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to R (\frac{x}{1}) \in ℂ$
75	74	abscld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{1})\| \in ℝ$
76	75	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{1})\| \in ℂ$
77	76	mul01d	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{1})\| \cdot 0 = 0$
78	66 77	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{⌊x⌋ + 1})\| (S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1)) - \|R (\frac{x}{1})\| \cdot 0 = (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) - 0$
79	1	pntsf	$⊢ S : ℝ ⟶ ℝ$
80	79	ffvelcdmi	$⊢ x \in ℝ \to S (x) \in ℝ$
81	5 80	syl	$⊢ (⊤ \land x \in (1, +∞)) \to S (x) \in ℝ$
82		relogcl	$⊢ a \in ℝ^{+} \to \log a \in ℝ$
83		remulcl	$⊢ (a \in ℝ \land \log a \in ℝ) \to a \log a \in ℝ$
84	82 83	sylan2	$⊢ (a \in ℝ \land a \in ℝ^{+}) \to a \log a \in ℝ$
85		0red	$⊢ (a \in ℝ \land \neg a \in ℝ^{+}) \to 0 \in ℝ$
86	84 85	ifclda	$⊢ a \in ℝ \to if (a \in ℝ^{+}, a \log a, 0) \in ℝ$
87	3 86	fmpti	$⊢ T : ℝ ⟶ ℝ$
88	87	ffvelcdmi	$⊢ ⌊x⌋ \in ℝ \to T (⌊x⌋) \in ℝ$
89	48 88	syl	$⊢ (⊤ \land x \in (1, +∞)) \to T (⌊x⌋) \in ℝ$
90	25 89	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 T (⌊x⌋) \in ℝ$
91	81 90	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to S (x) - 2 T (⌊x⌋) \in ℝ$
92	23 91	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) \in ℝ$
93	92	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) \in ℂ$
94	93	subid1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) - 0 = (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋))$
95	78 94	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{⌊x⌋ + 1})\| (S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1)) - \|R (\frac{x}{1})\| \cdot 0 = (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋))$
96	5	flcld	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ \in ℤ$
97		fzval3	$⊢ ⌊x⌋ \in ℤ \to (1 \dots ⌊x⌋) = (1 ..^⌊x⌋ + 1)$
98	96 97	syl	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) = (1 ..^⌊x⌋ + 1)$
99	98	eqcomd	$⊢ (⊤ \land x \in (1, +∞)) \to (1 ..^⌊x⌋ + 1) = (1 \dots ⌊x⌋)$
100	13	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
101		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
102	101	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
103	102	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
104	100 103	rpdivcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
105	70	ffvelcdmi	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) \in ℝ$
106	104 105	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℝ$
107	106	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℂ$
108	107	abscld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \in ℝ$
109	108	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \in ℂ$
110	6	a1i	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ^{+}$
111	103 110	rpaddcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \in ℝ^{+}$
112	100 111	rpdivcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n + 1} \in ℝ^{+}$
113	70	ffvelcdmi	$⊢ \frac{x}{n + 1} \in ℝ^{+} \to R (\frac{x}{n + 1}) \in ℝ$
114	112 113	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) \in ℝ$
115	114	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) \in ℂ$
116	115	abscld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1})\| \in ℝ$
117	116	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1})\| \in ℂ$
118	109 117	negsubdi2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to - (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) = \|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\|$
119	118	eqcomd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\| = - (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|)$
120	102	nncnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
121		1cnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
122	120 121	pncand	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - 1 = n$
123	122	fveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n + 1 - 1) = S (n)$
124	122	fveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n + 1 - 1) = T (n)$
125		rpre	$⊢ n \in ℝ^{+} \to n \in ℝ$
126		eleq1	$⊢ a = n \to (a \in ℝ^{+} \leftrightarrow n \in ℝ^{+})$
127		id	$⊢ a = n \to a = n$
128		fveq2	$⊢ a = n \to \log a = \log n$
129	127 128	oveq12d	$⊢ a = n \to a \log a = n \log n$
130	126 129	ifbieq1d	$⊢ a = n \to if (a \in ℝ^{+}, a \log a, 0) = if (n \in ℝ^{+}, n \log n, 0)$
131		ovex	$⊢ n \log n \in V$
132		c0ex	$⊢ 0 \in V$
133	131 132	ifex	$⊢ if (n \in ℝ^{+}, n \log n, 0) \in V$
134	130 3 133	fvmpt	$⊢ n \in ℝ \to T (n) = if (n \in ℝ^{+}, n \log n, 0)$
135	125 134	syl	$⊢ n \in ℝ^{+} \to T (n) = if (n \in ℝ^{+}, n \log n, 0)$
136		iftrue	$⊢ n \in ℝ^{+} \to if (n \in ℝ^{+}, n \log n, 0) = n \log n$
137	135 136	eqtrd	$⊢ n \in ℝ^{+} \to T (n) = n \log n$
138	103 137	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n) = n \log n$
139	124 138	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n + 1 - 1) = n \log n$
140	139	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 T (n + 1 - 1) = 2 n \log n$
141	123 140	oveq12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n + 1 - 1) - 2 T (n + 1 - 1) = S (n) - 2 n \log n$
142	119 141	oveq12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\|) (S (n + 1 - 1) - 2 T (n + 1 - 1)) = (- (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|)) (S (n) - 2 n \log n)$
143	108 116	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\| \in ℝ$
144	143	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\| \in ℂ$
145	102	nnred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
146	79	ffvelcdmi	$⊢ n \in ℝ \to S (n) \in ℝ$
147	145 146	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) \in ℝ$
148	24	a1i	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℝ$
149	103	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
150	145 149	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \log n \in ℝ$
151	148 150	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 n \log n \in ℝ$
152	147 151	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - 2 n \log n \in ℝ$
153	152	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - 2 n \log n \in ℂ$
154	144 153	mulneg1d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (- (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|)) (S (n) - 2 n \log n) = - (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)$
155	142 154	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\|) (S (n + 1 - 1) - 2 T (n + 1 - 1)) = - (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)$
156	99 155	sumeq12rdv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} (\|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\|) (S (n + 1 - 1) - 2 T (n + 1 - 1)) = \sum_{n = 1}^{⌊x⌋} (- (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n))$
157		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
158	143 152	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℝ$
159	158	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℂ$
160	157 159	fsumneg	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (- (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)) = - \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)$
161	156 160	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} (\|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\|) (S (n + 1 - 1) - 2 T (n + 1 - 1)) = - \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)$
162	95 161	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{⌊x⌋ + 1})\| (S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1)) - \|R (\frac{x}{1})\| \cdot 0 - \sum_{n \in (1 ..^⌊x⌋ + 1)} (\|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\|) (S (n + 1 - 1) - 2 T (n + 1 - 1)) = (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) - (- \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n))$
163		oveq2	$⊢ m = n \to \frac{x}{m} = \frac{x}{n}$
164	163	fveq2d	$⊢ m = n \to R (\frac{x}{m}) = R (\frac{x}{n})$
165	164	fveq2d	$⊢ m = n \to \|R (\frac{x}{m})\| = \|R (\frac{x}{n})\|$
166		fvoveq1	$⊢ m = n \to S (m - 1) = S (n - 1)$
167		fvoveq1	$⊢ m = n \to T (m - 1) = T (n - 1)$
168	167	oveq2d	$⊢ m = n \to 2 T (m - 1) = 2 T (n - 1)$
169	166 168	oveq12d	$⊢ m = n \to S (m - 1) - 2 T (m - 1) = S (n - 1) - 2 T (n - 1)$
170	165 169	jca	$⊢ m = n \to (\|R (\frac{x}{m})\| = \|R (\frac{x}{n})\| \land S (m - 1) - 2 T (m - 1) = S (n - 1) - 2 T (n - 1))$
171		oveq2	$⊢ m = n + 1 \to \frac{x}{m} = \frac{x}{n + 1}$
172	171	fveq2d	$⊢ m = n + 1 \to R (\frac{x}{m}) = R (\frac{x}{n + 1})$
173	172	fveq2d	$⊢ m = n + 1 \to \|R (\frac{x}{m})\| = \|R (\frac{x}{n + 1})\|$
174		fvoveq1	$⊢ m = n + 1 \to S (m - 1) = S (n + 1 - 1)$
175		fvoveq1	$⊢ m = n + 1 \to T (m - 1) = T (n + 1 - 1)$
176	175	oveq2d	$⊢ m = n + 1 \to 2 T (m - 1) = 2 T (n + 1 - 1)$
177	174 176	oveq12d	$⊢ m = n + 1 \to S (m - 1) - 2 T (m - 1) = S (n + 1 - 1) - 2 T (n + 1 - 1)$
178	173 177	jca	$⊢ m = n + 1 \to (\|R (\frac{x}{m})\| = \|R (\frac{x}{n + 1})\| \land S (m - 1) - 2 T (m - 1) = S (n + 1 - 1) - 2 T (n + 1 - 1))$
179		oveq2	$⊢ m = 1 \to \frac{x}{m} = \frac{x}{1}$
180	179	fveq2d	$⊢ m = 1 \to R (\frac{x}{m}) = R (\frac{x}{1})$
181	180	fveq2d	$⊢ m = 1 \to \|R (\frac{x}{m})\| = \|R (\frac{x}{1})\|$
182		oveq1	$⊢ m = 1 \to m - 1 = 1 - 1$
183		1m1e0	$⊢ 1 - 1 = 0$
184	182 183	eqtrdi	$⊢ m = 1 \to m - 1 = 0$
185	184	fveq2d	$⊢ m = 1 \to S (m - 1) = S (0)$
186		0re	$⊢ 0 \in ℝ$
187		fveq2	$⊢ a = 0 \to ⌊a⌋ = ⌊0⌋$
188		0z	$⊢ 0 \in ℤ$
189		flid	$⊢ 0 \in ℤ \to ⌊0⌋ = 0$
190	188 189	ax-mp	$⊢ ⌊0⌋ = 0$
191	187 190	eqtrdi	$⊢ a = 0 \to ⌊a⌋ = 0$
192	191	oveq2d	$⊢ a = 0 \to (1 \dots ⌊a⌋) = (1 \dots 0)$
193		fz10	$⊢ (1 \dots 0) = \emptyset$
194	192 193	eqtrdi	$⊢ a = 0 \to (1 \dots ⌊a⌋) = \emptyset$
195	194	sumeq1d	$⊢ a = 0 \to \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})) = \sum_{i \in \emptyset} Λ (i) (\log i + ψ (\frac{a}{i}))$
196		sum0	$⊢ \sum_{i \in \emptyset} Λ (i) (\log i + ψ (\frac{a}{i})) = 0$
197	195 196	eqtrdi	$⊢ a = 0 \to \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})) = 0$
198	197 1 132	fvmpt	$⊢ 0 \in ℝ \to S (0) = 0$
199	186 198	ax-mp	$⊢ S (0) = 0$
200	185 199	eqtrdi	$⊢ m = 1 \to S (m - 1) = 0$
201	184	fveq2d	$⊢ m = 1 \to T (m - 1) = T (0)$
202		rpne0	$⊢ a \in ℝ^{+} \to a \neq 0$
203	202	necon2bi	$⊢ a = 0 \to \neg a \in ℝ^{+}$
204	203	iffalsed	$⊢ a = 0 \to if (a \in ℝ^{+}, a \log a, 0) = 0$
205	204 3 132	fvmpt	$⊢ 0 \in ℝ \to T (0) = 0$
206	186 205	ax-mp	$⊢ T (0) = 0$
207	201 206	eqtrdi	$⊢ m = 1 \to T (m - 1) = 0$
208	207	oveq2d	$⊢ m = 1 \to 2 T (m - 1) = 2 \cdot 0$
209		2t0e0	$⊢ 2 \cdot 0 = 0$
210	208 209	eqtrdi	$⊢ m = 1 \to 2 T (m - 1) = 0$
211	200 210	oveq12d	$⊢ m = 1 \to S (m - 1) - 2 T (m - 1) = 0 - 0$
212		0m0e0	$⊢ 0 - 0 = 0$
213	211 212	eqtrdi	$⊢ m = 1 \to S (m - 1) - 2 T (m - 1) = 0$
214	181 213	jca	$⊢ m = 1 \to (\|R (\frac{x}{m})\| = \|R (\frac{x}{1})\| \land S (m - 1) - 2 T (m - 1) = 0)$
215		oveq2	$⊢ m = ⌊x⌋ + 1 \to \frac{x}{m} = \frac{x}{⌊x⌋ + 1}$
216	215	fveq2d	$⊢ m = ⌊x⌋ + 1 \to R (\frac{x}{m}) = R (\frac{x}{⌊x⌋ + 1})$
217	216	fveq2d	$⊢ m = ⌊x⌋ + 1 \to \|R (\frac{x}{m})\| = \|R (\frac{x}{⌊x⌋ + 1})\|$
218		fvoveq1	$⊢ m = ⌊x⌋ + 1 \to S (m - 1) = S (⌊x⌋ + 1 - 1)$
219		fvoveq1	$⊢ m = ⌊x⌋ + 1 \to T (m - 1) = T (⌊x⌋ + 1 - 1)$
220	219	oveq2d	$⊢ m = ⌊x⌋ + 1 \to 2 T (m - 1) = 2 T (⌊x⌋ + 1 - 1)$
221	218 220	oveq12d	$⊢ m = ⌊x⌋ + 1 \to S (m - 1) - 2 T (m - 1) = S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1)$
222	217 221	jca	$⊢ m = ⌊x⌋ + 1 \to (\|R (\frac{x}{m})\| = \|R (\frac{x}{⌊x⌋ + 1})\| \land S (m - 1) - 2 T (m - 1) = S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1))$
223		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
224	18 223	eleqtrdi	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \in ℤ_{\geq 1}$
225	13	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to x \in ℝ^{+}$
226		elfznn	$⊢ m \in (1 \dots ⌊x⌋ + 1) \to m \in ℕ$
227	226	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℕ$
228	227	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℝ^{+}$
229	225 228	rpdivcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to \frac{x}{m} \in ℝ^{+}$
230	70	ffvelcdmi	$⊢ \frac{x}{m} \in ℝ^{+} \to R (\frac{x}{m}) \in ℝ$
231	229 230	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to R (\frac{x}{m}) \in ℝ$
232	231	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to R (\frac{x}{m}) \in ℂ$
233	232	abscld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to \|R (\frac{x}{m})\| \in ℝ$
234	233	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to \|R (\frac{x}{m})\| \in ℂ$
235	227	nnred	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℝ$
236		1red	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to 1 \in ℝ$
237	235 236	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to m - 1 \in ℝ$
238	79	ffvelcdmi	$⊢ m - 1 \in ℝ \to S (m - 1) \in ℝ$
239	237 238	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to S (m - 1) \in ℝ$
240	24	a1i	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to 2 \in ℝ$
241	87	ffvelcdmi	$⊢ m - 1 \in ℝ \to T (m - 1) \in ℝ$
242	237 241	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to T (m - 1) \in ℝ$
243	240 242	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to 2 T (m - 1) \in ℝ$
244	239 243	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to S (m - 1) - 2 T (m - 1) \in ℝ$
245	244	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to S (m - 1) - 2 T (m - 1) \in ℂ$
246	170 178 214 222 224 234 245	fsumparts	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} \|R (\frac{x}{n})\| (S (n + 1 - 1) - 2 T (n + 1 - 1) - (S (n - 1) - 2 T (n - 1))) = \|R (\frac{x}{⌊x⌋ + 1})\| (S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1)) - \|R (\frac{x}{1})\| \cdot 0 - \sum_{n \in (1 ..^⌊x⌋ + 1)} (\|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\|) (S (n + 1 - 1) - 2 T (n + 1 - 1))$
247	147	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) \in ℂ$
248	87	ffvelcdmi	$⊢ n \in ℝ \to T (n) \in ℝ$
249	145 248	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n) \in ℝ$
250	148 249	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 T (n) \in ℝ$
251	250	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 T (n) \in ℂ$
252		1red	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
253	145 252	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℝ$
254	79	ffvelcdmi	$⊢ n - 1 \in ℝ \to S (n - 1) \in ℝ$
255	253 254	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n - 1) \in ℝ$
256	255	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n - 1) \in ℂ$
257	87	ffvelcdmi	$⊢ n - 1 \in ℝ \to T (n - 1) \in ℝ$
258	253 257	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n - 1) \in ℝ$
259	148 258	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 T (n - 1) \in ℝ$
260	259	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 T (n - 1) \in ℂ$
261	247 251 256 260	sub4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - 2 T (n) - (S (n - 1) - 2 T (n - 1)) = S (n) - S (n - 1) - (2 T (n) - 2 T (n - 1))$
262	124	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 T (n + 1 - 1) = 2 T (n)$
263	123 262	oveq12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n + 1 - 1) - 2 T (n + 1 - 1) = S (n) - 2 T (n)$
264	263	oveq1d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n + 1 - 1) - 2 T (n + 1 - 1) - (S (n - 1) - 2 T (n - 1)) = S (n) - 2 T (n) - (S (n - 1) - 2 T (n - 1))$
265		2cnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
266	249	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n) \in ℂ$
267	258	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n - 1) \in ℂ$
268	265 266 267	subdid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (T (n) - T (n - 1)) = 2 T (n) - 2 T (n - 1)$
269	268	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) - 2 (T (n) - T (n - 1)) = S (n) - S (n - 1) - (2 T (n) - 2 T (n - 1))$
270	261 264 269	3eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n + 1 - 1) - 2 T (n + 1 - 1) - (S (n - 1) - 2 T (n - 1)) = S (n) - S (n - 1) - 2 (T (n) - T (n - 1))$
271	270	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n + 1 - 1) - 2 T (n + 1 - 1) - (S (n - 1) - 2 T (n - 1))) = \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))$
272	99 271	sumeq12rdv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} \|R (\frac{x}{n})\| (S (n + 1 - 1) - 2 T (n + 1 - 1) - (S (n - 1) - 2 T (n - 1))) = \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))$
273	246 272	eqtr3d	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (\frac{x}{⌊x⌋ + 1})\| (S (⌊x⌋ + 1 - 1) - 2 T (⌊x⌋ + 1 - 1)) - \|R (\frac{x}{1})\| \cdot 0 - \sum_{n \in (1 ..^⌊x⌋ + 1)} (\|R (\frac{x}{n + 1})\| - \|R (\frac{x}{n})\|) (S (n + 1 - 1) - 2 T (n + 1 - 1)) = \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))$
274	157 159	fsumcl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℂ$
275	93 274	subnegd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) - (- \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)) = (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)$
276	162 273 275	3eqtr3rd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) = \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))$
277	13	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
278	277	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
279	67 278	mulcomd	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x = \log x x$
280	276 279	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x} = \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x x}$
281	147 255	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) \in ℝ$
282	249 258	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n) - T (n - 1) \in ℝ$
283	148 282	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (T (n) - T (n - 1)) \in ℝ$
284	281 283	resubcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) - 2 (T (n) - T (n - 1)) \in ℝ$
285	108 284	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1))) \in ℝ$
286	157 285	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1))) \in ℝ$
287	286	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1))) \in ℂ$
288	5 11	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
289	288	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
290	13	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \neq 0$
291	287 278 67 289 290	divdiv1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x}}{x} = \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x x}$
292	280 291	eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x} = \frac{\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x}}{x}$
293	292	oveq2d	$⊢ (⊤ \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}) + (\frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) = (\frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x}) + (\frac{\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x}}{x})$
294	72	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \in ℂ$
295	294	abscld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \in ℝ$
296	295 277	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℝ$
297	108 281	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n) - S (n - 1)) \in ℝ$
298	157 297	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1)) \in ℝ$
299	298 288	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x} \in ℝ$
300	296 299	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 ℝ$
301	300	recnd	$⊢ (⊤ \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 ℂ$
302	287 278 289	divcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x} \in ℂ$
303	301 302 67 290	divdird	$⊢ (⊤ \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}) + (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x})}{x} = (\frac{\|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x})}{x}) + (\frac{\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x}}{x})$
304	296	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℂ$
305	299	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x} \in ℂ$
306	304 305 302	subsubd	$⊢ (⊤ \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}) - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x})) = \|R (x)\| \log x - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x})$
307		2cnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℂ$
308	266 267	subcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n) - T (n - 1) \in ℂ$
309	109 308	mulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \in ℂ$
310	157 307 309	fsummulc2	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1)) = \sum_{n = 1}^{⌊x⌋} 2 \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
311	281	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) \in ℂ$
312	265 308	mulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 (T (n) - T (n - 1)) \in ℂ$
313	311 312	nncand	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) - (S (n) - S (n - 1) - 2 (T (n) - T (n - 1))) = 2 (T (n) - T (n - 1))$
314	313	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n) - S (n - 1) - (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))) = \|R (\frac{x}{n})\| 2 (T (n) - T (n - 1))$
315	284	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - S (n - 1) - 2 (T (n) - T (n - 1)) \in ℂ$
316	109 311 315	subdid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n) - S (n - 1) - (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))) = \|R (\frac{x}{n})\| (S (n) - S (n - 1)) - \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))$
317	109 265 308	mul12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| 2 (T (n) - T (n - 1)) = 2 \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
318	314 316 317	3eqtr3d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n) - S (n - 1)) - \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1))) = 2 \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
319	318	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| (S (n) - S (n - 1)) - \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))) = \sum_{n = 1}^{⌊x⌋} 2 \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
320	297	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n) - S (n - 1)) \in ℂ$
321	285	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1))) \in ℂ$
322	157 320 321	fsumsub	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| (S (n) - S (n - 1)) - \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))) = \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1)) - \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))$
323	310 319 322	3eqtr2rd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1)) - \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1))) = 2 \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
324	323	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1)) - \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x} = \frac{2 \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{\log x}$
325	298	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1)) \in ℂ$
326	325 287 278 289	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1)) - \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x} = (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x})$
327	108 282	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \in ℝ$
328	157 327	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \in ℝ$
329	328	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \in ℂ$
330	307 329 278 289	div23d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{\log x} = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
331	324 326 330	3eqtr3d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1))}{\log x}) - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
332	331	oveq2d	$⊢ (⊤ \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}) - (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x})) = \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
333	306 332	eqtr3d	$⊢ (⊤ \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}) + (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x}) = \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
334	333	oveq1d	$⊢ (⊤ \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}) + (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (S (n) - S (n - 1) - 2 (T (n) - T (n - 1)))}{\log x})}{x} = \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{x}$
335	293 303 334	3eqtr2d	$⊢ (⊤ \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}) + (\frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) = \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{x}$
336	335	mpteq2dva	$⊢ ⊤ \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}) + (\frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x})) = (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{x})$
337	300 13	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 ℝ$
338	157 158	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℝ$
339	92 338	readdcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℝ$
340	13 288	rpmulcld	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℝ^{+}$
341	339 340	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x} \in ℝ$
342	1 2	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)$
343	342	a1i	$⊢ ⊤ \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)$
344	340	rpcnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℂ$
345	340	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \neq 0$
346	93 274 344 345	divdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x} = (\frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋))}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x})$
347	91	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to S (x) - 2 T (⌊x⌋) \in ℂ$
348	45 347 344 345	divassd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋))}{x \log x} = (\frac{x}{⌊x⌋ + 1}) (\frac{S (x) - 2 T (⌊x⌋)}{x \log x})$
349	348	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋))}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) = (\frac{x}{⌊x⌋ + 1}) (\frac{S (x) - 2 T (⌊x⌋)}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x})$
350	346 349	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x} = (\frac{x}{⌊x⌋ + 1}) (\frac{S (x) - 2 T (⌊x⌋)}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x})$
351	350	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) = (x \in (1, +∞) ⟼ (\frac{x}{⌊x⌋ + 1}) (\frac{S (x) - 2 T (⌊x⌋)}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}))$
352	91 340	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{S (x) - 2 T (⌊x⌋)}{x \log x} \in ℝ$
353	23 352	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1}) (\frac{S (x) - 2 T (⌊x⌋)}{x \log x}) \in ℝ$
354	338 340	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x} \in ℝ$
355		ioossre	$⊢ (1, +∞) \subseteq ℝ$
356	355	a1i	$⊢ ⊤ \to (1, +∞) \subseteq ℝ$
357		1red	$⊢ ⊤ \to 1 \in ℝ$
358	23 8 32	ltled	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} \leq 1$
359	358	adantrr	$⊢ (⊤ \land (x \in (1, +∞) \land 1 \leq x)) \to \frac{x}{⌊x⌋ + 1} \leq 1$
360	356 23 357 357 359	ello1d	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{x}{⌊x⌋ + 1}) \in \leq 𝑂 (1)$
361	81	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to S (x) \in ℂ$
362	90	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 T (⌊x⌋) \in ℂ$
363	361 362 344 345	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{S (x) - 2 T (⌊x⌋)}{x \log x} = (\frac{S (x)}{x \log x}) - (\frac{2 T (⌊x⌋)}{x \log x})$
364	363	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{S (x) - 2 T (⌊x⌋)}{x \log x}) = (x \in (1, +∞) ⟼ (\frac{S (x)}{x \log x}) - (\frac{2 T (⌊x⌋)}{x \log x}))$
365	81 340	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{S (x)}{x \log x} \in ℝ$
366	90 340	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 T (⌊x⌋)}{x \log x} \in ℝ$
367		2cnd	$⊢ ⊤ \to 2 \in ℂ$
368		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 2 \in ℂ) \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
369	355 367 368	sylancr	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
370	365	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{S (x)}{x \log x} \in ℂ$
371	81 13	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{S (x)}{x} \in ℝ$
372	371	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{S (x)}{x} \in ℂ$
373	307 278	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \log x \in ℂ$
374	372 373 278 289	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{S (x)}{x}) - 2 \log x}{\log x} = (\frac{\frac{S (x)}{x}}{\log x}) - (\frac{2 \log x}{\log x})$
375	25 277	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \log x \in ℝ$
376	371 375	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{S (x)}{x}) - 2 \log x \in ℝ$
377	376	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{S (x)}{x}) - 2 \log x \in ℂ$
378	377 278 289	divrecd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{S (x)}{x}) - 2 \log x}{\log x} = ((\frac{S (x)}{x}) - 2 \log x) (\frac{1}{\log x})$
379	361 67 278 290 289	divdiv1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{S (x)}{x}}{\log x} = \frac{S (x)}{x \log x}$
380	307 278 289	divcan4d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 \log x}{\log x} = 2$
381	379 380	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\frac{S (x)}{x}}{\log x}) - (\frac{2 \log x}{\log x}) = (\frac{S (x)}{x \log x}) - 2$
382	374 378 381	3eqtr3rd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{S (x)}{x \log x}) - 2 = ((\frac{S (x)}{x}) - 2 \log x) (\frac{1}{\log x})$
383	382	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{S (x)}{x \log x}) - 2) = (x \in (1, +∞) ⟼ ((\frac{S (x)}{x}) - 2 \log x) (\frac{1}{\log x}))$
384	8 288	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{1}{\log x} \in ℝ$
385	13	ex	$⊢ ⊤ \to (x \in (1, +∞) \to x \in ℝ^{+})$
386	385	ssrdv	$⊢ ⊤ \to (1, +∞) \subseteq ℝ^{+}$
387	1	selbergs	$⊢ (x \in ℝ^{+} ⟼ (\frac{S (x)}{x}) - 2 \log x) \in 𝑂 (1)$
388	387	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{S (x)}{x}) - 2 \log x) \in 𝑂 (1)$
389	386 388	o1res2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{S (x)}{x}) - 2 \log x) \in 𝑂 (1)$
390		divlogrlim	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0$
391		rlimo1	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0 \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
392	390 391	mp1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
393	376 384 389 392	o1mul2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ ((\frac{S (x)}{x}) - 2 \log x) (\frac{1}{\log x})) \in 𝑂 (1)$
394	383 393	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{S (x)}{x \log x}) - 2) \in 𝑂 (1)$
395	370 307 394	o1dif	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ \frac{S (x)}{x \log x}) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ 2) \in 𝑂 (1))$
396	369 395	mpbird	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{S (x)}{x \log x}) \in 𝑂 (1)$
397	24	a1i	$⊢ ⊤ \to 2 \in ℝ$
398	5 277	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℝ$
399		2rp	$⊢ 2 \in ℝ^{+}$
400	399	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℝ^{+}$
401	400	rpge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq 2$
402		flge1nn	$⊢ (x \in ℝ \land 1 \leq x) \to ⌊x⌋ \in ℕ$
403	5 12 402	syl2anc	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ \in ℕ$
404	403	nnrpd	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ \in ℝ^{+}$
405		rpre	$⊢ ⌊x⌋ \in ℝ^{+} \to ⌊x⌋ \in ℝ$
406		eleq1	$⊢ a = ⌊x⌋ \to (a \in ℝ^{+} \leftrightarrow ⌊x⌋ \in ℝ^{+})$
407		id	$⊢ a = ⌊x⌋ \to a = ⌊x⌋$
408		fveq2	$⊢ a = ⌊x⌋ \to \log a = \log ⌊x⌋$
409	407 408	oveq12d	$⊢ a = ⌊x⌋ \to a \log a = ⌊x⌋ \log ⌊x⌋$
410	406 409	ifbieq1d	$⊢ a = ⌊x⌋ \to if (a \in ℝ^{+}, a \log a, 0) = if (⌊x⌋ \in ℝ^{+}, ⌊x⌋ \log ⌊x⌋, 0)$
411		ovex	$⊢ ⌊x⌋ \log ⌊x⌋ \in V$
412	411 132	ifex	$⊢ if (⌊x⌋ \in ℝ^{+}, ⌊x⌋ \log ⌊x⌋, 0) \in V$
413	410 3 412	fvmpt	$⊢ ⌊x⌋ \in ℝ \to T (⌊x⌋) = if (⌊x⌋ \in ℝ^{+}, ⌊x⌋ \log ⌊x⌋, 0)$
414	405 413	syl	$⊢ ⌊x⌋ \in ℝ^{+} \to T (⌊x⌋) = if (⌊x⌋ \in ℝ^{+}, ⌊x⌋ \log ⌊x⌋, 0)$
415		iftrue	$⊢ ⌊x⌋ \in ℝ^{+} \to if (⌊x⌋ \in ℝ^{+}, ⌊x⌋ \log ⌊x⌋, 0) = ⌊x⌋ \log ⌊x⌋$
416	414 415	eqtrd	$⊢ ⌊x⌋ \in ℝ^{+} \to T (⌊x⌋) = ⌊x⌋ \log ⌊x⌋$
417	404 416	syl	$⊢ (⊤ \land x \in (1, +∞)) \to T (⌊x⌋) = ⌊x⌋ \log ⌊x⌋$
418	404	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log ⌊x⌋ \in ℝ$
419	16	nn0ge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq ⌊x⌋$
420	403	nnge1d	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \leq ⌊x⌋$
421	48 420	logge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq \log ⌊x⌋$
422		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
423	5 422	syl	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ \leq x$
424	404 13	logled	$⊢ (⊤ \land x \in (1, +∞)) \to (⌊x⌋ \leq x \leftrightarrow \log ⌊x⌋ \leq \log x)$
425	423 424	mpbid	$⊢ (⊤ \land x \in (1, +∞)) \to \log ⌊x⌋ \leq \log x$
426	48 5 418 277 419 421 423 425	lemul12ad	$⊢ (⊤ \land x \in (1, +∞)) \to ⌊x⌋ \log ⌊x⌋ \leq x \log x$
427	417 426	eqbrtrd	$⊢ (⊤ \land x \in (1, +∞)) \to T (⌊x⌋) \leq x \log x$
428	89 398 25 401 427	lemul2ad	$⊢ (⊤ \land x \in (1, +∞)) \to 2 T (⌊x⌋) \leq 2 x \log x$
429	90 25 340	ledivmul2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2 T (⌊x⌋)}{x \log x} \leq 2 \leftrightarrow 2 T (⌊x⌋) \leq 2 x \log x)$
430	428 429	mpbird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 T (⌊x⌋)}{x \log x} \leq 2$
431	430	adantrr	$⊢ (⊤ \land (x \in (1, +∞) \land 1 \leq x)) \to \frac{2 T (⌊x⌋)}{x \log x} \leq 2$
432	356 366 357 397 431	ello1d	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{2 T (⌊x⌋)}{x \log x}) \in \leq 𝑂 (1)$
433		0red	$⊢ ⊤ \to 0 \in ℝ$
434	48 418 419 421	mulge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq ⌊x⌋ \log ⌊x⌋$
435	434 417	breqtrrd	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq T (⌊x⌋)$
436	25 89 401 435	mulge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq 2 T (⌊x⌋)$
437	90 340 436	divge0d	$⊢ (⊤ \land x \in (1, +∞)) \to 0 \leq \frac{2 T (⌊x⌋)}{x \log x}$
438	366 433 437	o1lo12	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ \frac{2 T (⌊x⌋)}{x \log x}) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ \frac{2 T (⌊x⌋)}{x \log x}) \in \leq 𝑂 (1))$
439	432 438	mpbird	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{2 T (⌊x⌋)}{x \log x}) \in 𝑂 (1)$
440	365 366 396 439	o1sub2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{S (x)}{x \log x}) - (\frac{2 T (⌊x⌋)}{x \log x})) \in 𝑂 (1)$
441	364 440	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{S (x) - 2 T (⌊x⌋)}{x \log x}) \in 𝑂 (1)$
442	352 441	o1lo1d	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{S (x) - 2 T (⌊x⌋)}{x \log x}) \in \leq 𝑂 (1)$
443	23 352 360 442 43	lo1mul	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{x}{⌊x⌋ + 1}) (\frac{S (x) - 2 T (⌊x⌋)}{x \log x})) \in \leq 𝑂 (1)$
444	1	selbergsb	$⊢ \exists c \in ℝ^{+} \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq c$
445		simpl	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq c) \to c \in ℝ^{+}$
446		simpr	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq c) \to \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq c$
447	1 2 445 446	pntrlog2bndlem3	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq c) \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) \in 𝑂 (1)$
448	447	rexlimiva	$⊢ \exists c \in ℝ^{+} \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq c \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) \in 𝑂 (1)$
449	444 448	mp1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) \in 𝑂 (1)$
450	354 449	o1lo1d	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) \in \leq 𝑂 (1)$
451	353 354 443 450	lo1add	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{x}{⌊x⌋ + 1}) (\frac{S (x) - 2 T (⌊x⌋)}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x})) \in \leq 𝑂 (1)$
452	351 451	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) \in \leq 𝑂 (1)$
453	337 341 343 452	lo1add	$⊢ ⊤ \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}) + (\frac{(\frac{x}{⌊x⌋ + 1}) (S (x) - 2 T (⌊x⌋)) + \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x})) \in \leq 𝑂 (1)$
454	336 453	eqeltrrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{x}) \in \leq 𝑂 (1)$
455	454	mptru	$⊢ (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{x}) \in \leq 𝑂 (1)$

Metamath Proof Explorer

Theorem pntrlog2bndlem4

Proof