pntrlog2bndlem5

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))$
	pntrlog2bndlem5.1	$⊢ φ \to B \in ℝ^{+}$
	pntrlog2bndlem5.2	$⊢ φ \to \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq B$
Assertion	pntrlog2bndlem5	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{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		pntrlog2bndlem5.1	$⊢ φ \to B \in ℝ^{+}$
5		pntrlog2bndlem5.2	$⊢ φ \to \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq B$
6		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
7	6	adantl	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ$
8		1rp	$⊢ 1 \in ℝ^{+}$
9	8	a1i	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
10		1red	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ$
11		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
12	11	adantl	$⊢ (φ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
13	12	simpld	$⊢ (φ \land x \in (1, +∞)) \to 1 < x$
14	10 7 13	ltled	$⊢ (φ \land x \in (1, +∞)) \to 1 \leq x$
15	7 9 14	rpgecld	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ^{+}$
16	2	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
17	16	ffvelrni	$⊢ x \in ℝ^{+} \to R (x) \in ℝ$
18	15 17	syl	$⊢ (φ \land x \in (1, +∞)) \to R (x) \in ℝ$
19	18	recnd	$⊢ (φ \land x \in (1, +∞)) \to R (x) \in ℂ$
20	19	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \in ℝ$
21	20	recnd	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \in ℂ$
22	15	relogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ$
23	22	recnd	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℂ$
24	21 23	mulcld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℂ$
25		2cnd	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℂ$
26	7 13	rplogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
27	26	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to \log x \neq 0$
28	25 23 27	divcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℂ$
29		fzfid	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
30	15	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
31		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
32	31	adantl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
33	32	nnrpd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
34	30 33	rpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
35	16	ffvelrni	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) \in ℝ$
36	34 35	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℝ$
37	36	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℂ$
38	37	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \in ℝ$
39	33	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
40		1red	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
41	39 40	readdcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n + 1 \in ℝ$
42	38 41	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (\log n + 1) \in ℝ$
43	42	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (\log n + 1) \in ℂ$
44	29 43	fsumcl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) \in ℂ$
45	28 44	mulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) \in ℂ$
46	24 45	subcld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) \in ℂ$
47	38	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \in ℂ$
48	29 47	fsumcl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \in ℂ$
49	28 48	mulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \in ℂ$
50	7	recnd	$⊢ (φ \land x \in (1, +∞)) \to x \in ℂ$
51	15	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to x \neq 0$
52	46 49 50 51	divdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} = (\frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x})$
53	20 22	remulcld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℝ$
54	53	recnd	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℂ$
55	54 45 49	subsubd	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|) = \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|$
56	28 44 48	subdid	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) - \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|$
57	29 43 47	fsumsub	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| (\log n + 1) - \|R (\frac{x}{n})\|) = \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) - \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|$
58	41	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n + 1 \in ℂ$
59		1cnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
60	47 58 59	subdid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (\log n + 1 - 1) = \|R (\frac{x}{n})\| (\log n + 1) - \|R (\frac{x}{n})\| \cdot 1$
61	39	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
62	61 59	pncand	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n + 1 - 1 = \log n$
63	62	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (\log n + 1 - 1) = \|R (\frac{x}{n})\| \log n$
64	47	mulid1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \cdot 1 = \|R (\frac{x}{n})\|$
65	64	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (\log n + 1) - \|R (\frac{x}{n})\| \cdot 1 = \|R (\frac{x}{n})\| (\log n + 1) - \|R (\frac{x}{n})\|$
66	60 63 65	3eqtr3rd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (\log n + 1) - \|R (\frac{x}{n})\| = \|R (\frac{x}{n})\| \log n$
67	66	sumeq2dv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| (\log n + 1) - \|R (\frac{x}{n})\|) = \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
68	57 67	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) - \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| = \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
69	68	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) - \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
70	56 69	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
71	70	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|) = \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
72	55 71	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| = \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
73	72	oveq1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} = \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x}$
74	52 73	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x}) = \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x}$
75	74	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x})) = (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x})$
76		2re	$⊢ 2 \in ℝ$
77	76	a1i	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℝ$
78	77 26	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
79	29 42	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) \in ℝ$
80	78 79	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) \in ℝ$
81	53 80	resubcld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) \in ℝ$
82	81 15	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)}{x} \in ℝ$
83	29 38	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \in ℝ$
84	78 83	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \in ℝ$
85	84 15	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} \in ℝ$
86		1red	$⊢ φ \to 1 \in ℝ$
87	1 2 3	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)$
88	87	a1i	$⊢ φ \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)$
89	32	nnred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
90		simpl	$⊢ (a \in ℝ \land a \in ℝ^{+}) \to a \in ℝ$
91		simpr	$⊢ (a \in ℝ \land a \in ℝ^{+}) \to a \in ℝ^{+}$
92	91	relogcld	$⊢ (a \in ℝ \land a \in ℝ^{+}) \to \log a \in ℝ$
93	90 92	remulcld	$⊢ (a \in ℝ \land a \in ℝ^{+}) \to a \log a \in ℝ$
94		0red	$⊢ (a \in ℝ \land \neg a \in ℝ^{+}) \to 0 \in ℝ$
95	93 94	ifclda	$⊢ a \in ℝ \to if (a \in ℝ^{+}, a \log a, 0) \in ℝ$
96	3 95	fmpti	$⊢ T : ℝ ⟶ ℝ$
97	96	ffvelrni	$⊢ n \in ℝ \to T (n) \in ℝ$
98	89 97	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n) \in ℝ$
99	89 40	resubcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℝ$
100	96	ffvelrni	$⊢ n - 1 \in ℝ \to T (n - 1) \in ℝ$
101	99 100	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n - 1) \in ℝ$
102	98 101	resubcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n) - T (n - 1) \in ℝ$
103	38 102	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \in ℝ$
104	29 103	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \in ℝ$
105	78 104	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \in ℝ$
106	53 105	resubcld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \in ℝ$
107	106 15	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{x} \in ℝ$
108		2rp	$⊢ 2 \in ℝ^{+}$
109	108	a1i	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℝ^{+}$
110	109	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq 2$
111	77 26 110	divge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \frac{2}{\log x}$
112	37	absge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|R (\frac{x}{n})\|$
113	33	adantr	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n \in ℝ^{+}$
114	113	rpcnd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n \in ℂ$
115	61	adantr	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log n \in ℂ$
116	114 115	mulcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n \log n \in ℂ$
117		simpr	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to 1 < n$
118		1re	$⊢ 1 \in ℝ$
119	113	rpred	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n \in ℝ$
120		difrp	$⊢ (1 \in ℝ \land n \in ℝ) \to (1 < n \leftrightarrow n - 1 \in ℝ^{+})$
121	118 119 120	sylancr	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to (1 < n \leftrightarrow n - 1 \in ℝ^{+})$
122	117 121	mpbid	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n - 1 \in ℝ^{+}$
123	122	relogcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log (n - 1) \in ℝ$
124	123	recnd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log (n - 1) \in ℂ$
125	114 124	mulcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n \log (n - 1) \in ℂ$
126	116 125 124	subsubd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n \log n - (n \log (n - 1) - \log (n - 1)) = n \log n - n \log (n - 1) + \log (n - 1)$
127		rpre	$⊢ n \in ℝ^{+} \to n \in ℝ$
128		eleq1	$⊢ a = n \to (a \in ℝ^{+} \leftrightarrow n \in ℝ^{+})$
129		id	$⊢ a = n \to a = n$
130		fveq2	$⊢ a = n \to \log a = \log n$
131	129 130	oveq12d	$⊢ a = n \to a \log a = n \log n$
132	128 131	ifbieq1d	$⊢ a = n \to if (a \in ℝ^{+}, a \log a, 0) = if (n \in ℝ^{+}, n \log n, 0)$
133		ovex	$⊢ n \log n \in V$
134		c0ex	$⊢ 0 \in V$
135	133 134	ifex	$⊢ if (n \in ℝ^{+}, n \log n, 0) \in V$
136	132 3 135	fvmpt	$⊢ n \in ℝ \to T (n) = if (n \in ℝ^{+}, n \log n, 0)$
137	127 136	syl	$⊢ n \in ℝ^{+} \to T (n) = if (n \in ℝ^{+}, n \log n, 0)$
138		iftrue	$⊢ n \in ℝ^{+} \to if (n \in ℝ^{+}, n \log n, 0) = n \log n$
139	137 138	eqtrd	$⊢ n \in ℝ^{+} \to T (n) = n \log n$
140	113 139	syl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to T (n) = n \log n$
141		rpre	$⊢ n - 1 \in ℝ^{+} \to n - 1 \in ℝ$
142		eleq1	$⊢ a = n - 1 \to (a \in ℝ^{+} \leftrightarrow n - 1 \in ℝ^{+})$
143		id	$⊢ a = n - 1 \to a = n - 1$
144		fveq2	$⊢ a = n - 1 \to \log a = \log (n - 1)$
145	143 144	oveq12d	$⊢ a = n - 1 \to a \log a = (n - 1) \log (n - 1)$
146	142 145	ifbieq1d	$⊢ a = n - 1 \to if (a \in ℝ^{+}, a \log a, 0) = if (n - 1 \in ℝ^{+}, (n - 1) \log (n - 1), 0)$
147		ovex	$⊢ (n - 1) \log (n - 1) \in V$
148	147 134	ifex	$⊢ if (n - 1 \in ℝ^{+}, (n - 1) \log (n - 1), 0) \in V$
149	146 3 148	fvmpt	$⊢ n - 1 \in ℝ \to T (n - 1) = if (n - 1 \in ℝ^{+}, (n - 1) \log (n - 1), 0)$
150	141 149	syl	$⊢ n - 1 \in ℝ^{+} \to T (n - 1) = if (n - 1 \in ℝ^{+}, (n - 1) \log (n - 1), 0)$
151		iftrue	$⊢ n - 1 \in ℝ^{+} \to if (n - 1 \in ℝ^{+}, (n - 1) \log (n - 1), 0) = (n - 1) \log (n - 1)$
152	150 151	eqtrd	$⊢ n - 1 \in ℝ^{+} \to T (n - 1) = (n - 1) \log (n - 1)$
153	122 152	syl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to T (n - 1) = (n - 1) \log (n - 1)$
154		1cnd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to 1 \in ℂ$
155	114 154 124	subdird	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to (n - 1) \log (n - 1) = n \log (n - 1) - 1 \log (n - 1)$
156	124	mulid2d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to 1 \log (n - 1) = \log (n - 1)$
157	156	oveq2d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n \log (n - 1) - 1 \log (n - 1) = n \log (n - 1) - \log (n - 1)$
158	153 155 157	3eqtrd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to T (n - 1) = n \log (n - 1) - \log (n - 1)$
159	140 158	oveq12d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to T (n) - T (n - 1) = n \log n - (n \log (n - 1) - \log (n - 1))$
160	114 115 124	subdid	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) = n \log n - n \log (n - 1)$
161	160	oveq1d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) + \log (n - 1) = n \log n - n \log (n - 1) + \log (n - 1)$
162	126 159 161	3eqtr4d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to T (n) - T (n - 1) = n (\log n - \log (n - 1)) + \log (n - 1)$
163	113	relogcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log n \in ℝ$
164	163 123	resubcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log n - \log (n - 1) \in ℝ$
165	164	recnd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log n - \log (n - 1) \in ℂ$
166	114 154 165	subdird	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to (n - 1) (\log n - \log (n - 1)) = n (\log n - \log (n - 1)) - 1 (\log n - \log (n - 1))$
167	165	mulid2d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to 1 (\log n - \log (n - 1)) = \log n - \log (n - 1)$
168	167	oveq2d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) - 1 (\log n - \log (n - 1)) = n (\log n - \log (n - 1)) - (\log n - \log (n - 1))$
169	119 164	remulcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) \in ℝ$
170	169	recnd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) \in ℂ$
171	170 115 124	subsub3d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) - (\log n - \log (n - 1)) = n (\log n - \log (n - 1)) + \log (n - 1) - \log n$
172	166 168 171	3eqtrd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to (n - 1) (\log n - \log (n - 1)) = n (\log n - \log (n - 1)) + \log (n - 1) - \log n$
173	114 154	npcand	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n - 1 + 1 = n$
174	173	fveq2d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log (n - 1 + 1) = \log n$
175	174	oveq1d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log (n - 1 + 1) - \log (n - 1) = \log n - \log (n - 1)$
176		logdifbnd	$⊢ n - 1 \in ℝ^{+} \to \log (n - 1 + 1) - \log (n - 1) \leq \frac{1}{n - 1}$
177	122 176	syl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log (n - 1 + 1) - \log (n - 1) \leq \frac{1}{n - 1}$
178	175 177	eqbrtrrd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to \log n - \log (n - 1) \leq \frac{1}{n - 1}$
179		1red	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to 1 \in ℝ$
180	164 179 122	lemuldiv2d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to ((n - 1) (\log n - \log (n - 1)) \leq 1 \leftrightarrow \log n - \log (n - 1) \leq \frac{1}{n - 1})$
181	178 180	mpbird	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to (n - 1) (\log n - \log (n - 1)) \leq 1$
182	172 181	eqbrtrrd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) + \log (n - 1) - \log n \leq 1$
183	169 123	readdcld	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) + \log (n - 1) \in ℝ$
184	183 163 179	lesubadd2d	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to (n (\log n - \log (n - 1)) + \log (n - 1) - \log n \leq 1 \leftrightarrow n (\log n - \log (n - 1)) + \log (n - 1) \leq \log n + 1)$
185	182 184	mpbid	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to n (\log n - \log (n - 1)) + \log (n - 1) \leq \log n + 1$
186	162 185	eqbrtrd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 < n) \to T (n) - T (n - 1) \leq \log n + 1$
187		fveq2	$⊢ n = 1 \to T (n) = T (1)$
188		id	$⊢ a = 1 \to a = 1$
189	188 8	eqeltrdi	$⊢ a = 1 \to a \in ℝ^{+}$
190	189	iftrued	$⊢ a = 1 \to if (a \in ℝ^{+}, a \log a, 0) = a \log a$
191		fveq2	$⊢ a = 1 \to \log a = \log 1$
192		log1	$⊢ \log 1 = 0$
193	191 192	eqtrdi	$⊢ a = 1 \to \log a = 0$
194	188 193	oveq12d	$⊢ a = 1 \to a \log a = 1 \cdot 0$
195		ax-1cn	$⊢ 1 \in ℂ$
196	195	mul01i	$⊢ 1 \cdot 0 = 0$
197	194 196	eqtrdi	$⊢ a = 1 \to a \log a = 0$
198	190 197	eqtrd	$⊢ a = 1 \to if (a \in ℝ^{+}, a \log a, 0) = 0$
199	198 3 134	fvmpt	$⊢ 1 \in ℝ \to T (1) = 0$
200	118 199	ax-mp	$⊢ T (1) = 0$
201	187 200	eqtrdi	$⊢ n = 1 \to T (n) = 0$
202		oveq1	$⊢ n = 1 \to n - 1 = 1 - 1$
203		1m1e0	$⊢ 1 - 1 = 0$
204	202 203	eqtrdi	$⊢ n = 1 \to n - 1 = 0$
205	204	fveq2d	$⊢ n = 1 \to T (n - 1) = T (0)$
206		0re	$⊢ 0 \in ℝ$
207		rpne0	$⊢ a \in ℝ^{+} \to a \neq 0$
208	207	necon2bi	$⊢ a = 0 \to \neg a \in ℝ^{+}$
209	208	iffalsed	$⊢ a = 0 \to if (a \in ℝ^{+}, a \log a, 0) = 0$
210	209 3 134	fvmpt	$⊢ 0 \in ℝ \to T (0) = 0$
211	206 210	ax-mp	$⊢ T (0) = 0$
212	205 211	eqtrdi	$⊢ n = 1 \to T (n - 1) = 0$
213	201 212	oveq12d	$⊢ n = 1 \to T (n) - T (n - 1) = 0 - 0$
214		0m0e0	$⊢ 0 - 0 = 0$
215	213 214	eqtrdi	$⊢ n = 1 \to T (n) - T (n - 1) = 0$
216	215	eqcoms	$⊢ 1 = n \to T (n) - T (n - 1) = 0$
217	216	adantl	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 = n) \to T (n) - T (n - 1) = 0$
218		0red	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \in ℝ$
219	32	nnge1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq n$
220	89 219	logge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \log n$
221	39	lep1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \leq \log n + 1$
222	218 39 41 220 221	letrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \log n + 1$
223	222	adantr	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 = n) \to 0 \leq \log n + 1$
224	217 223	eqbrtrd	$⊢ (((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land 1 = n) \to T (n) - T (n - 1) \leq \log n + 1$
225		elfzle1	$⊢ n \in (1 \dots ⌊x⌋) \to 1 \leq n$
226	225	adantl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq n$
227	40 89	leloed	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \leq n \leftrightarrow (1 < n \lor 1 = n))$
228	226 227	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 < n \lor 1 = n)$
229	186 224 228	mpjaodan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to T (n) - T (n - 1) \leq \log n + 1$
230	102 41 38 112 229	lemul2ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \leq \|R (\frac{x}{n})\| (\log n + 1)$
231	29 103 42 230	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \leq \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)$
232	104 79 78 111 231	lemul2ad	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1)) \leq (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)$
233	105 80 53 232	lesub2dd	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1) \leq \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))$
234	81 106 15 233	lediv1dd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)}{x} \leq \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{x}$
235	234	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)}{x} \leq \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (T (n) - T (n - 1))}{x}$
236	86 88 107 82 235	lo1le	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)}{x}) \in \leq 𝑂 (1)$
237	108	a1i	$⊢ φ \to 2 \in ℝ^{+}$
238	237 4	rpmulcld	$⊢ φ \to 2 B \in ℝ^{+}$
239	238	rpred	$⊢ φ \to 2 B \in ℝ$
240	239	adantr	$⊢ (φ \land x \in (1, +∞)) \to 2 B \in ℝ$
241	10 26	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{1}{\log x} \in ℝ$
242	10 241	readdcld	$⊢ (φ \land x \in (1, +∞)) \to 1 + (\frac{1}{\log x}) \in ℝ$
243		ioossre	$⊢ (1, +∞) \subseteq ℝ$
244		lo1const	$⊢ ((1, +∞) \subseteq ℝ \land 2 B \in ℝ) \to (x \in (1, +∞) ⟼ 2 B) \in \leq 𝑂 (1)$
245	243 239 244	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ 2 B) \in \leq 𝑂 (1)$
246		lo1const	$⊢ ((1, +∞) \subseteq ℝ \land 1 \in ℝ) \to (x \in (1, +∞) ⟼ 1) \in \leq 𝑂 (1)$
247	243 86 246	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ 1) \in \leq 𝑂 (1)$
248		divlogrlim	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0$
249		rlimo1	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0 \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
250	248 249	mp1i	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
251	241 250	o1lo1d	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in \leq 𝑂 (1)$
252	10 241 247 251	lo1add	$⊢ φ \to (x \in (1, +∞) ⟼ 1 + (\frac{1}{\log x})) \in \leq 𝑂 (1)$
253	238	adantr	$⊢ (φ \land x \in (1, +∞)) \to 2 B \in ℝ^{+}$
254	253	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq 2 B$
255	240 242 245 252 254	lo1mul	$⊢ φ \to (x \in (1, +∞) ⟼ 2 B (1 + (\frac{1}{\log x}))) \in \leq 𝑂 (1)$
256	240 242	remulcld	$⊢ (φ \land x \in (1, +∞)) \to 2 B (1 + (\frac{1}{\log x})) \in ℝ$
257	83 15	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} \in ℝ$
258	22 10	readdcld	$⊢ (φ \land x \in (1, +∞)) \to \log x + 1 \in ℝ$
259	4	adantr	$⊢ (φ \land x \in (1, +∞)) \to B \in ℝ^{+}$
260	259	rpred	$⊢ (φ \land x \in (1, +∞)) \to B \in ℝ$
261	258 260	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (\log x + 1) B \in ℝ$
262	32	nnrecred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℝ$
263	29 262	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \in ℝ$
264	263 260	remulcld	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) B \in ℝ$
265	38 30	rerpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\|}{x} \in ℝ$
266	260	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to B \in ℝ$
267	262 266	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{1}{n}) B \in ℝ$
268	34	rpcnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℂ$
269	34	rpne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \neq 0$
270	37 268 269	absdivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| = \frac{\|R (\frac{x}{n})\|}{\|\frac{x}{n}\|}$
271	7	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
272	271 32	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
273	34	rpge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{x}{n}$
274	272 273	absidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{x}{n}\| = \frac{x}{n}$
275	274	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\|}{\|\frac{x}{n}\|} = \frac{\|R (\frac{x}{n})\|}{\frac{x}{n}}$
276	270 275	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| = \frac{\|R (\frac{x}{n})\|}{\frac{x}{n}}$
277	50	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
278	89	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
279	51	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \neq 0$
280	32	nnne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
281	47 277 278 279 280	divdiv2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\|}{\frac{x}{n}} = \frac{\|R (\frac{x}{n})\| n}{x}$
282	47 278 277 279	div23d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\| n}{x} = (\frac{\|R (\frac{x}{n})\|}{x}) n$
283	276 281 282	3eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| = (\frac{\|R (\frac{x}{n})\|}{x}) n$
284		fveq2	$⊢ y = \frac{x}{n} \to R (y) = R (\frac{x}{n})$
285		id	$⊢ y = \frac{x}{n} \to y = \frac{x}{n}$
286	284 285	oveq12d	$⊢ y = \frac{x}{n} \to \frac{R (y)}{y} = \frac{R (\frac{x}{n})}{\frac{x}{n}}$
287	286	fveq2d	$⊢ y = \frac{x}{n} \to \|\frac{R (y)}{y}\| = \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\|$
288	287	breq1d	$⊢ y = \frac{x}{n} \to (\|\frac{R (y)}{y}\| \leq B \leftrightarrow \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| \leq B)$
289	5	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq B$
290	288 289 34	rspcdva	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| \leq B$
291	283 290	eqbrtrrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\|R (\frac{x}{n})\|}{x}) n \leq B$
292	265 266 33	lemuldivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{\|R (\frac{x}{n})\|}{x}) n \leq B \leftrightarrow \frac{\|R (\frac{x}{n})\|}{x} \leq \frac{B}{n})$
293	291 292	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\|}{x} \leq \frac{B}{n}$
294	266	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to B \in ℂ$
295	294 278 280	divrec2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{B}{n} = (\frac{1}{n}) B$
296	293 295	breqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\|}{x} \leq (\frac{1}{n}) B$
297	29 265 267 296	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{\|R (\frac{x}{n})\|}{x}) \leq \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) B$
298	29 50 47 51	fsumdivc	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{\|R (\frac{x}{n})\|}{x})$
299	259	rpcnd	$⊢ (φ \land x \in (1, +∞)) \to B \in ℂ$
300	262	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℂ$
301	29 299 300	fsummulc1	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) B = \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) B$
302	297 298 301	3brtr4d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} \leq \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) B$
303	259	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq B$
304		harmonicubnd	$⊢ (x \in ℝ \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1$
305	7 14 304	syl2anc	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1$
306	263 258 260 303 305	lemul1ad	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) B \leq (\log x + 1) B$
307	257 264 261 302 306	letrd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} \leq (\log x + 1) B$
308	257 261 78 111 307	lemul2ad	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x}) \leq (\frac{2}{\log x}) (\log x + 1) B$
309	28 48 50 51	divassd	$⊢ (φ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} = (\frac{2}{\log x}) (\frac{\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x})$
310	242	recnd	$⊢ (φ \land x \in (1, +∞)) \to 1 + (\frac{1}{\log x}) \in ℂ$
311	25 299 310	mul32d	$⊢ (φ \land x \in (1, +∞)) \to 2 B (1 + (\frac{1}{\log x})) = 2 (1 + (\frac{1}{\log x})) B$
312		1cnd	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℂ$
313	23 312 23 27	divdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x + 1}{\log x} = (\frac{\log x}{\log x}) + (\frac{1}{\log x})$
314	23 27	dividd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x}{\log x} = 1$
315	314	oveq1d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\log x}{\log x}) + (\frac{1}{\log x}) = 1 + (\frac{1}{\log x})$
316	313 315	eqtr2d	$⊢ (φ \land x \in (1, +∞)) \to 1 + (\frac{1}{\log x}) = \frac{\log x + 1}{\log x}$
317	316	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to 2 (1 + (\frac{1}{\log x})) = 2 (\frac{\log x + 1}{\log x})$
318	23 312	addcld	$⊢ (φ \land x \in (1, +∞)) \to \log x + 1 \in ℂ$
319	25 23 318 27	div32d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\log x + 1) = 2 (\frac{\log x + 1}{\log x})$
320	317 319	eqtr4d	$⊢ (φ \land x \in (1, +∞)) \to 2 (1 + (\frac{1}{\log x})) = (\frac{2}{\log x}) (\log x + 1)$
321	320	oveq1d	$⊢ (φ \land x \in (1, +∞)) \to 2 (1 + (\frac{1}{\log x})) B = (\frac{2}{\log x}) (\log x + 1) B$
322	28 318 299	mulassd	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\log x + 1) B = (\frac{2}{\log x}) (\log x + 1) B$
323	311 321 322	3eqtrd	$⊢ (φ \land x \in (1, +∞)) \to 2 B (1 + (\frac{1}{\log x})) = (\frac{2}{\log x}) (\log x + 1) B$
324	308 309 323	3brtr4d	$⊢ (φ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} \leq 2 B (1 + (\frac{1}{\log x}))$
325	324	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x} \leq 2 B (1 + (\frac{1}{\log x}))$
326	86 255 256 85 325	lo1le	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x}) \in \leq 𝑂 (1)$
327	82 85 236 326	lo1add	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| (\log n + 1)}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\|}{x})) \in \leq 𝑂 (1)$
328	75 327	eqeltrrd	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x}) \in \leq 𝑂 (1)$

Metamath Proof Explorer

Theorem pntrlog2bndlem5

Proof