pntrlog2bndlem6

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$
	pntrlog2bndlem6.1	$⊢ φ \to A \in ℝ$
	pntrlog2bndlem6.2	$⊢ φ \to 1 \leq A$
Assertion	pntrlog2bndlem6	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|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		pntrlog2bndlem6.1	$⊢ φ \to A \in ℝ$
7		pntrlog2bndlem6.2	$⊢ φ \to 1 \leq A$
8		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
9	8	adantl	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ$
10		1rp	$⊢ 1 \in ℝ^{+}$
11	10	a1i	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
12		1red	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ$
13		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
14	13	adantl	$⊢ (φ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
15	14	simpld	$⊢ (φ \land x \in (1, +∞)) \to 1 < x$
16	12 9 15	ltled	$⊢ (φ \land x \in (1, +∞)) \to 1 \leq x$
17	9 11 16	rpgecld	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ^{+}$
18	2	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
19	18	ffvelcdmi	$⊢ x \in ℝ^{+} \to R (x) \in ℝ$
20	17 19	syl	$⊢ (φ \land x \in (1, +∞)) \to R (x) \in ℝ$
21	20	recnd	$⊢ (φ \land x \in (1, +∞)) \to R (x) \in ℂ$
22	21	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \in ℝ$
23	17	relogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ$
24	22 23	remulcld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℝ$
25		2re	$⊢ 2 \in ℝ$
26	25	a1i	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℝ$
27	9 15	rplogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
28	26 27	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
29		fzfid	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
30	17	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	18	ffvelcdmi	$⊢ \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	38 39	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \log n \in ℝ$
41	29 40	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
42	28 41	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
43	24 42	resubcld	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
44	43	recnd	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℂ$
45		fzfid	$⊢ (φ \land x \in (1, +∞)) \to (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋) \in Fin$
46		ssun2	$⊢ (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋) \subseteq (1 \dots ⌊\frac{x}{A}⌋) \cup (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)$
47	1 2 3 4 5 6 7	pntrlog2bndlem6a	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) = (1 \dots ⌊\frac{x}{A}⌋) \cup (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)$
48	46 47	sseqtrrid	$⊢ (φ \land x \in (1, +∞)) \to (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋) \subseteq (1 \dots ⌊x⌋)$
49	48	sselda	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to n \in (1 \dots ⌊x⌋)$
50	49 40	syldan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \log n \in ℝ$
51	45 50	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
52	28 51	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
53	52	recnd	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℂ$
54	9	recnd	$⊢ (φ \land x \in (1, +∞)) \to x \in ℂ$
55	17	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to x \neq 0$
56	44 53 54 55	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 + (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x} = (\frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x})$
57	24	recnd	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℂ$
58	42	recnd	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℂ$
59	57 58 53	subsubd	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n - (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n) = \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n + (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
60	28	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℂ$
61	41	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℂ$
62	51	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \in ℂ$
63	60 61 62	subdid	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n - \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n - (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
64		fzfid	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊\frac{x}{A}⌋) \in Fin$
65		ssun1	$⊢ (1 \dots ⌊\frac{x}{A}⌋) \subseteq (1 \dots ⌊\frac{x}{A}⌋) \cup (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)$
66	65 47	sseqtrrid	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊\frac{x}{A}⌋) \subseteq (1 \dots ⌊x⌋)$
67	66	sselda	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to n \in (1 \dots ⌊x⌋)$
68	67 40	syldan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \|R (\frac{x}{n})\| \log n \in ℝ$
69	64 68	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
70	69	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \in ℂ$
71	10	a1i	$⊢ φ \to 1 \in ℝ^{+}$
72	6 71 7	rpgecld	$⊢ φ \to A \in ℝ^{+}$
73	72	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ^{+}$
74	9 73	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{A} \in ℝ$
75		reflcl	$⊢ \frac{x}{A} \in ℝ \to ⌊\frac{x}{A}⌋ \in ℝ$
76	74 75	syl	$⊢ (φ \land x \in (1, +∞)) \to ⌊\frac{x}{A}⌋ \in ℝ$
77	76	ltp1d	$⊢ (φ \land x \in (1, +∞)) \to ⌊\frac{x}{A}⌋ < ⌊\frac{x}{A}⌋ + 1$
78		fzdisj	$⊢ ⌊\frac{x}{A}⌋ < ⌊\frac{x}{A}⌋ + 1 \to (1 \dots ⌊\frac{x}{A}⌋) \cap (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋) = \emptyset$
79	77 78	syl	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊\frac{x}{A}⌋) \cap (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋) = \emptyset$
80	40	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \log n \in ℂ$
81	79 47 29 80	fsumsplit	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n = \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n + \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n$
82	70 62 81	mvrraddd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n - \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n = \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n$
83	82	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n - \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n$
84	63 83	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n - (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n = (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n$
85	84	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n - (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n) = \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n$
86	59 85	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n + (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n = \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n$
87	86	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 + (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x} = \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x}$
88	56 87	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}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x}) = \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x}$
89	88	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x})) = (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x})$
90	43 17	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}{x} \in ℝ$
91	52 17	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x} \in ℝ$
92	1 2 3 4 5	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)$
93		ioossre	$⊢ (1, +∞) \subseteq ℝ$
94	93	a1i	$⊢ φ \to (1, +∞) \subseteq ℝ$
95		1red	$⊢ φ \to 1 \in ℝ$
96	25	a1i	$⊢ φ \to 2 \in ℝ$
97	4	rpred	$⊢ φ \to B \in ℝ$
98	72	relogcld	$⊢ φ \to \log A \in ℝ$
99	98 95	readdcld	$⊢ φ \to \log A + 1 \in ℝ$
100	97 99	remulcld	$⊢ φ \to B (\log A + 1) \in ℝ$
101	96 100	remulcld	$⊢ φ \to 2 B (\log A + 1) \in ℝ$
102	51 27	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{\log x} \in ℝ$
103	97	adantr	$⊢ (φ \land x \in (1, +∞)) \to B \in ℝ$
104	73	relogcld	$⊢ (φ \land x \in (1, +∞)) \to \log A \in ℝ$
105	104 12	readdcld	$⊢ (φ \land x \in (1, +∞)) \to \log A + 1 \in ℝ$
106	103 105	remulcld	$⊢ (φ \land x \in (1, +∞)) \to B (\log A + 1) \in ℝ$
107	9 106	remulcld	$⊢ (φ \land x \in (1, +∞)) \to x B (\log A + 1) \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	103 9	remulcld	$⊢ (φ \land x \in (1, +∞)) \to B x \in ℝ$
112	49 31	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to n \in ℕ$
113	112	nnrecred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℝ$
114	45 113	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n}) \in ℝ$
115	111 114	remulcld	$⊢ (φ \land x \in (1, +∞)) \to B x \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n}) \in ℝ$
116	27	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \log x \in ℝ^{+}$
117	50 116	rerpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\| \log n}{\log x} \in ℝ$
118	103	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to B \in ℝ$
119	9	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to x \in ℝ$
120	118 119	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to B x \in ℝ$
121	120 113	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to B x (\frac{1}{n}) \in ℝ$
122	49 38	syldan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \in ℝ$
123	119 112	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
124	118 123	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to B (\frac{x}{n}) \in ℝ$
125	49 33	syldan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
126	125	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \log n \in ℝ$
127	17	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
128	127	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \log x \in ℝ$
129	49 37	syldan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℂ$
130	129	absge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to 0 \leq \|R (\frac{x}{n})\|$
131		elfzle2	$⊢ n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋) \to n \leq ⌊x⌋$
132	131	adantl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to n \leq ⌊x⌋$
133	112	nnzd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to n \in ℤ$
134		flge	$⊢ (x \in ℝ \land n \in ℤ) \to (n \leq x \leftrightarrow n \leq ⌊x⌋)$
135	119 133 134	syl2anc	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to (n \leq x \leftrightarrow n \leq ⌊x⌋)$
136	132 135	mpbird	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to n \leq x$
137	125 127	logled	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to (n \leq x \leftrightarrow \log n \leq \log x)$
138	136 137	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \log n \leq \log x$
139	126 128 122 130 138	lemul2ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \log n \leq \|R (\frac{x}{n})\| \log x$
140	50 122 116	ledivmul2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to (\frac{\|R (\frac{x}{n})\| \log n}{\log x} \leq \|R (\frac{x}{n})\| \leftrightarrow \|R (\frac{x}{n})\| \log n \leq \|R (\frac{x}{n})\| \log x)$
141	139 140	mpbird	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\| \log n}{\log x} \leq \|R (\frac{x}{n})\|$
142	123	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℂ$
143	49 34	syldan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
144	143	rpne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{x}{n} \neq 0$
145	129 142 144	absdivd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| = \frac{\|R (\frac{x}{n})\|}{\|\frac{x}{n}\|}$
146	17	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq x$
147	146	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to 0 \leq x$
148	119 125 147	divge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to 0 \leq \frac{x}{n}$
149	123 148	absidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|\frac{x}{n}\| = \frac{x}{n}$
150	149	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\|}{\|\frac{x}{n}\|} = \frac{\|R (\frac{x}{n})\|}{\frac{x}{n}}$
151	145 150	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| = \frac{\|R (\frac{x}{n})\|}{\frac{x}{n}}$
152		fveq2	$⊢ y = \frac{x}{n} \to R (y) = R (\frac{x}{n})$
153		id	$⊢ y = \frac{x}{n} \to y = \frac{x}{n}$
154	152 153	oveq12d	$⊢ y = \frac{x}{n} \to \frac{R (y)}{y} = \frac{R (\frac{x}{n})}{\frac{x}{n}}$
155	154	fveq2d	$⊢ y = \frac{x}{n} \to \|\frac{R (y)}{y}\| = \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\|$
156	155	breq1d	$⊢ y = \frac{x}{n} \to (\|\frac{R (y)}{y}\| \leq B \leftrightarrow \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| \leq B)$
157	5	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq B$
158	156 157 143	rspcdva	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|\frac{R (\frac{x}{n})}{\frac{x}{n}}\| \leq B$
159	151 158	eqbrtrrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\|}{\frac{x}{n}} \leq B$
160	122 118 143	ledivmul2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to (\frac{\|R (\frac{x}{n})\|}{\frac{x}{n}} \leq B \leftrightarrow \|R (\frac{x}{n})\| \leq B (\frac{x}{n}))$
161	159 160	mpbid	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \leq B (\frac{x}{n})$
162	117 122 124 141 161	letrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\| \log n}{\log x} \leq B (\frac{x}{n})$
163	118	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to B \in ℂ$
164	54	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to x \in ℂ$
165	112	nncnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to n \in ℂ$
166	112	nnne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to n \neq 0$
167	163 164 165 166	divassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{B x}{n} = B (\frac{x}{n})$
168	163 164	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to B x \in ℂ$
169	168 165 166	divrecd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{B x}{n} = B x (\frac{1}{n})$
170	167 169	eqtr3d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to B (\frac{x}{n}) = B x (\frac{1}{n})$
171	162 170	breqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{\|R (\frac{x}{n})\| \log n}{\log x} \leq B x (\frac{1}{n})$
172	45 117 121 171	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{\|R (\frac{x}{n})\| \log n}{\log x}) \leq \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} B x (\frac{1}{n})$
173	23	recnd	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℂ$
174	49 80	syldan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \log n \in ℂ$
175	27	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to \log x \neq 0$
176	45 173 174 175	fsumdivc	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{\log x} = \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{\|R (\frac{x}{n})\| \log n}{\log x})$
177	103	recnd	$⊢ (φ \land x \in (1, +∞)) \to B \in ℂ$
178	177 54	mulcld	$⊢ (φ \land x \in (1, +∞)) \to B x \in ℂ$
179	113	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℂ$
180	45 178 179	fsummulc2	$⊢ (φ \land x \in (1, +∞)) \to B x \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n}) = \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} B x (\frac{1}{n})$
181	172 176 180	3brtr4d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{\log x} \leq B x \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n})$
182	4	adantr	$⊢ (φ \land x \in (1, +∞)) \to B \in ℝ^{+}$
183	182	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq B$
184	103 9 183 146	mulge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq B x$
185	32	nnrecred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℝ$
186	29 185	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \in ℝ$
187	23 104	resubcld	$⊢ (φ \land x \in (1, +∞)) \to \log x - \log A \in ℝ$
188	23 12	readdcld	$⊢ (φ \land x \in (1, +∞)) \to \log x + 1 \in ℝ$
189	67 185	syldan	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \frac{1}{n} \in ℝ$
190	64 189	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n}) \in ℝ$
191		harmonicubnd	$⊢ (x \in ℝ \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1$
192	9 16 191	syl2anc	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1$
193	17 73	relogdivd	$⊢ (φ \land x \in (1, +∞)) \to \log (\frac{x}{A}) = \log x - \log A$
194	17 73	rpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{A} \in ℝ^{+}$
195		harmoniclbnd	$⊢ \frac{x}{A} \in ℝ^{+} \to \log (\frac{x}{A}) \leq \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n})$
196	194 195	syl	$⊢ (φ \land x \in (1, +∞)) \to \log (\frac{x}{A}) \leq \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n})$
197	193 196	eqbrtrrd	$⊢ (φ \land x \in (1, +∞)) \to \log x - \log A \leq \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n})$
198	186 187 188 190 192 197	le2subd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n}) \leq \log x + 1 - (\log x - \log A)$
199	67 31	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to n \in ℕ$
200	199	nnrecred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \frac{1}{n} \in ℝ$
201	64 200	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n}) \in ℝ$
202	201	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n}) \in ℂ$
203	114	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n}) \in ℂ$
204	32	nncnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
205	32	nnne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
206	204 205	reccld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℂ$
207	79 47 29 206	fsumsplit	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) = \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n}) + \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n})$
208	202 203 207	mvrladdd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \sum_{n = 1}^{⌊\frac{x}{A}⌋} (\frac{1}{n}) = \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n})$
209		1cnd	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℂ$
210	104	recnd	$⊢ (φ \land x \in (1, +∞)) \to \log A \in ℂ$
211	173 209 210	pnncand	$⊢ (φ \land x \in (1, +∞)) \to \log x + 1 - (\log x - \log A) = 1 + \log A$
212	209 210 211	comraddd	$⊢ (φ \land x \in (1, +∞)) \to \log x + 1 - (\log x - \log A) = \log A + 1$
213	198 208 212	3brtr3d	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n}) \leq \log A + 1$
214	114 105 111 184 213	lemul2ad	$⊢ (φ \land x \in (1, +∞)) \to B x \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n}) \leq B x (\log A + 1)$
215	105	recnd	$⊢ (φ \land x \in (1, +∞)) \to \log A + 1 \in ℂ$
216	177 54 215	mulassd	$⊢ (φ \land x \in (1, +∞)) \to B x (\log A + 1) = B x (\log A + 1)$
217	177 54 215	mul12d	$⊢ (φ \land x \in (1, +∞)) \to B x (\log A + 1) = x B (\log A + 1)$
218	216 217	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to B x (\log A + 1) = x B (\log A + 1)$
219	214 218	breqtrd	$⊢ (φ \land x \in (1, +∞)) \to B x \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} (\frac{1}{n}) \leq x B (\log A + 1)$
220	102 115 107 181 219	letrd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{\log x} \leq x B (\log A + 1)$
221	102 107 26 110 220	lemul2ad	$⊢ (φ \land x \in (1, +∞)) \to 2 (\frac{\sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{\log x}) \leq 2 x B (\log A + 1)$
222		2cnd	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℂ$
223	222 173 62 175	div32d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n = 2 (\frac{\sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{\log x})$
224	210 209	addcld	$⊢ (φ \land x \in (1, +∞)) \to \log A + 1 \in ℂ$
225	177 224	mulcld	$⊢ (φ \land x \in (1, +∞)) \to B (\log A + 1) \in ℂ$
226	54 222 225	mul12d	$⊢ (φ \land x \in (1, +∞)) \to x 2 B (\log A + 1) = 2 x B (\log A + 1)$
227	221 223 226	3brtr4d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \leq x 2 B (\log A + 1)$
228	101	adantr	$⊢ (φ \land x \in (1, +∞)) \to 2 B (\log A + 1) \in ℝ$
229	52 228 17	ledivmuld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x} \leq 2 B (\log A + 1) \leftrightarrow (\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n \leq x 2 B (\log A + 1))$
230	227 229	mpbird	$⊢ (φ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x} \leq 2 B (\log A + 1)$
231	230	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x} \leq 2 B (\log A + 1)$
232	94 91 95 101 231	ello1d	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x}) \in \leq 𝑂 (1)$
233	90 91 92 232	lo1add	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = ⌊\frac{x}{A}⌋ + 1}^{⌊x⌋} \|R (\frac{x}{n})\| \log n}{x})) \in \leq 𝑂 (1)$
234	89 233	eqeltrrd	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x}) \in \leq 𝑂 (1)$

Metamath Proof Explorer

Theorem pntrlog2bndlem6

Proof