pntrlog2bndlem2

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)$
	pntrlog2bndlem2.1	$⊢ φ \to A \in ℝ^{+}$
	pntrlog2bndlem2.2	$⊢ φ \to \forall y \in ℝ^{+} ψ (y) \leq A y$
Assertion	pntrlog2bndlem2	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}) \in 𝑂 (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		pntrlog2bndlem2.1	$⊢ φ \to A \in ℝ^{+}$
4		pntrlog2bndlem2.2	$⊢ φ \to \forall y \in ℝ^{+} ψ (y) \leq A y$
5		1red	$⊢ φ \to 1 \in ℝ$
6		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
7	6	adantl	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ$
8		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
9	7 8	syl	$⊢ (φ \land x \in (1, +∞)) \to ψ (x) \in ℝ$
10	9	recnd	$⊢ (φ \land x \in (1, +∞)) \to ψ (x) \in ℂ$
11		fzfid	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
12	7	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
13		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
14	13	adantl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
15	14	peano2nnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \in ℕ$
16	12 15	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n + 1} \in ℝ$
17		chpcl	$⊢ \frac{x}{n + 1} \in ℝ \to ψ (\frac{x}{n + 1}) \in ℝ$
18	16 17	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) \in ℝ$
19	18 16	readdcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) \in ℝ$
20	11 19	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \in ℝ$
21	20	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \in ℂ$
22	7	recnd	$⊢ (φ \land x \in (1, +∞)) \to x \in ℂ$
23		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
24	23	adantl	$⊢ (φ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
25	24	simpld	$⊢ (φ \land x \in (1, +∞)) \to 1 < x$
26	7 25	rplogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
27	26	rpcnd	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℂ$
28	22 27	mulcld	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℂ$
29		1rp	$⊢ 1 \in ℝ^{+}$
30	29	a1i	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
31		1red	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ$
32	31 7 25	ltled	$⊢ (φ \land x \in (1, +∞)) \to 1 \leq x$
33	7 30 32	rpgecld	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ^{+}$
34	33	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to x \neq 0$
35	26	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to \log x \neq 0$
36	22 27 34 35	mulne0d	$⊢ (φ \land x \in (1, +∞)) \to x \log x \neq 0$
37	10 21 28 36	divdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x} = (\frac{ψ (x)}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x})$
38	37	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}) = (x \in (1, +∞) ⟼ (\frac{ψ (x)}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}))$
39	33 26	rpmulcld	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℝ^{+}$
40	9 39	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{ψ (x)}{x \log x} \in ℝ$
41	20 39	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x} \in ℝ$
42	10 22 27 34 35	divdiv1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{ψ (x)}{x}}{\log x} = \frac{ψ (x)}{x \log x}$
43	9 33	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{ψ (x)}{x} \in ℝ$
44	43	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{ψ (x)}{x} \in ℂ$
45	44 27 35	divrecd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{ψ (x)}{x}}{\log x} = (\frac{ψ (x)}{x}) (\frac{1}{\log x})$
46	42 45	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to \frac{ψ (x)}{x \log x} = (\frac{ψ (x)}{x}) (\frac{1}{\log x})$
47	46	mpteq2dva	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{ψ (x)}{x \log x}) = (x \in (1, +∞) ⟼ (\frac{ψ (x)}{x}) (\frac{1}{\log x}))$
48	26	rprecred	$⊢ (φ \land x \in (1, +∞)) \to \frac{1}{\log x} \in ℝ$
49	33	ex	$⊢ φ \to (x \in (1, +∞) \to x \in ℝ^{+})$
50	49	ssrdv	$⊢ φ \to (1, +∞) \subseteq ℝ^{+}$
51		chpo1ub	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
52	51	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
53	50 52	o1res2	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
54		divlogrlim	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0$
55		rlimo1	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0 \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
56	54 55	mp1i	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{1}{\log x}) \in 𝑂 (1)$
57	43 48 53 56	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{ψ (x)}{x}) (\frac{1}{\log x})) \in 𝑂 (1)$
58	47 57	eqeltrd	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{ψ (x)}{x \log x}) \in 𝑂 (1)$
59	3	rpred	$⊢ φ \to A \in ℝ$
60	59 5	readdcld	$⊢ φ \to A + 1 \in ℝ$
61	60	adantr	$⊢ (φ \land x \in (1, +∞)) \to A + 1 \in ℝ$
62	31 48	readdcld	$⊢ (φ \land x \in (1, +∞)) \to 1 + (\frac{1}{\log x}) \in ℝ$
63		ioossre	$⊢ (1, +∞) \subseteq ℝ$
64	60	recnd	$⊢ φ \to A + 1 \in ℂ$
65		o1const	$⊢ ((1, +∞) \subseteq ℝ \land A + 1 \in ℂ) \to (x \in (1, +∞) ⟼ A + 1) \in 𝑂 (1)$
66	63 64 65	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ A + 1) \in 𝑂 (1)$
67		1cnd	$⊢ φ \to 1 \in ℂ$
68		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 1 \in ℂ) \to (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
69	63 67 68	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ 1) \in 𝑂 (1)$
70	31 48 69 56	o1add2	$⊢ φ \to (x \in (1, +∞) ⟼ 1 + (\frac{1}{\log x})) \in 𝑂 (1)$
71	61 62 66 70	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ (A + 1) (1 + (\frac{1}{\log x}))) \in 𝑂 (1)$
72	61 62	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) (1 + (\frac{1}{\log x})) \in ℝ$
73	41	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x} \in ℂ$
74		chpge0	$⊢ \frac{x}{n + 1} \in ℝ \to 0 \leq ψ (\frac{x}{n + 1})$
75	16 74	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq ψ (\frac{x}{n + 1})$
76	14	nnrpd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
77	29	a1i	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ^{+}$
78	76 77	rpaddcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \in ℝ^{+}$
79	33	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
80	79	rpge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq x$
81	12 78 80	divge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{x}{n + 1}$
82	18 16 75 81	addge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})$
83	11 19 82	fsumge0	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
84	20 39 83	divge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}$
85	41 84	absidd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}\| = \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}$
86	72	recnd	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) (1 + (\frac{1}{\log x})) \in ℂ$
87	86	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|(A + 1) (1 + (\frac{1}{\log x}))\| \in ℝ$
88	20 33	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x} \in ℝ$
89	33	relogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ$
90	89 31	readdcld	$⊢ (φ \land x \in (1, +∞)) \to \log x + 1 \in ℝ$
91	61 90	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) (\log x + 1) \in ℝ$
92	61 7	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) x \in ℝ$
93	14	nnrecred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℝ$
94	11 93	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \in ℝ$
95	92 94	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) x \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \in ℝ$
96	92 90	remulcld	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) x (\log x + 1) \in ℝ$
97	59	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℝ$
98		1red	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
99	97 98	readdcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A + 1 \in ℝ$
100	99 12	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (A + 1) x \in ℝ$
101	100 93	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (A + 1) x (\frac{1}{n}) \in ℝ$
102	100 15	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{(A + 1) x}{n + 1} \in ℝ$
103	100 14	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{(A + 1) x}{n} \in ℝ$
104	97 16	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A (\frac{x}{n + 1}) \in ℝ$
105		fveq2	$⊢ y = \frac{x}{n + 1} \to ψ (y) = ψ (\frac{x}{n + 1})$
106		oveq2	$⊢ y = \frac{x}{n + 1} \to A y = A (\frac{x}{n + 1})$
107	105 106	breq12d	$⊢ y = \frac{x}{n + 1} \to (ψ (y) \leq A y \leftrightarrow ψ (\frac{x}{n + 1}) \leq A (\frac{x}{n + 1}))$
108	4	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \forall y \in ℝ^{+} ψ (y) \leq A y$
109	79 78	rpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n + 1} \in ℝ^{+}$
110	107 108 109	rspcdva	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) \leq A (\frac{x}{n + 1})$
111	18 104 16 110	leadd1dd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) \leq A (\frac{x}{n + 1}) + (\frac{x}{n + 1})$
112	64	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A + 1 \in ℂ$
113	22	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
114	14	nncnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
115		1cnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
116	114 115	addcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \in ℂ$
117	15	nnne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \neq 0$
118	112 113 116 117	divassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{(A + 1) x}{n + 1} = (A + 1) (\frac{x}{n + 1})$
119	97	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℂ$
120	113 116 117	divcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n + 1} \in ℂ$
121	119 115 120	adddird	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (A + 1) (\frac{x}{n + 1}) = A (\frac{x}{n + 1}) + 1 (\frac{x}{n + 1})$
122	120	mullidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 (\frac{x}{n + 1}) = \frac{x}{n + 1}$
123	122	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A (\frac{x}{n + 1}) + 1 (\frac{x}{n + 1}) = A (\frac{x}{n + 1}) + (\frac{x}{n + 1})$
124	118 121 123	3eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{(A + 1) x}{n + 1} = A (\frac{x}{n + 1}) + (\frac{x}{n + 1})$
125	111 124	breqtrrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) \leq \frac{(A + 1) x}{n + 1}$
126	59	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ$
127	3	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ^{+}$
128	127	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq A$
129	30	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq 1$
130	126 31 128 129	addge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq A + 1$
131	33	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq x$
132	61 7 130 131	mulge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq (A + 1) x$
133	132	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq (A + 1) x$
134	14	nnred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
135	134	lep1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \leq n + 1$
136	76 78 100 133 135	lediv2ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{(A + 1) x}{n + 1} \leq \frac{(A + 1) x}{n}$
137	19 102 103 125 136	letrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) \leq \frac{(A + 1) x}{n}$
138	100	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (A + 1) x \in ℂ$
139	14	nnne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
140	138 114 139	divrecd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{(A + 1) x}{n} = (A + 1) x (\frac{1}{n})$
141	137 140	breqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) \leq (A + 1) x (\frac{1}{n})$
142	11 19 101 141	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \leq \sum_{n = 1}^{⌊x⌋} (A + 1) x (\frac{1}{n})$
143	92	recnd	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) x \in ℂ$
144	114 139	reccld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℂ$
145	11 143 144	fsummulc2	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) x \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) = \sum_{n = 1}^{⌊x⌋} (A + 1) x (\frac{1}{n})$
146	142 145	breqtrrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \leq (A + 1) x \sum_{n = 1}^{⌊x⌋} (\frac{1}{n})$
147		harmonicubnd	$⊢ (x \in ℝ \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1$
148	7 32 147	syl2anc	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1$
149	94 90 92 132 148	lemul2ad	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) x \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq (A + 1) x (\log x + 1)$
150	20 95 96 146 149	letrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \leq (A + 1) x (\log x + 1)$
151	64	adantr	$⊢ (φ \land x \in (1, +∞)) \to A + 1 \in ℂ$
152	90	recnd	$⊢ (φ \land x \in (1, +∞)) \to \log x + 1 \in ℂ$
153	151 22 152	mul32d	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) x (\log x + 1) = (A + 1) (\log x + 1) x$
154	150 153	breqtrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \leq (A + 1) (\log x + 1) x$
155	20 91 33	ledivmul2d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x} \leq (A + 1) (\log x + 1) \leftrightarrow \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \leq (A + 1) (\log x + 1) x)$
156	154 155	mpbird	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x} \leq (A + 1) (\log x + 1)$
157	88 91 26 156	lediv1dd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x}}{\log x} \leq \frac{(A + 1) (\log x + 1)}{\log x}$
158	21 22 27 34 35	divdiv1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x}}{\log x} = \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}$
159		1cnd	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℂ$
160	27 159	addcld	$⊢ (φ \land x \in (1, +∞)) \to \log x + 1 \in ℂ$
161	151 160 27 35	divassd	$⊢ (φ \land x \in (1, +∞)) \to \frac{(A + 1) (\log x + 1)}{\log x} = (A + 1) (\frac{\log x + 1}{\log x})$
162	27 159 27 35	divdird	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x + 1}{\log x} = (\frac{\log x}{\log x}) + (\frac{1}{\log x})$
163	27 35	dividd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\log x}{\log x} = 1$
164	163	oveq1d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{\log x}{\log x}) + (\frac{1}{\log x}) = 1 + (\frac{1}{\log x})$
165	162 164	eqtr2d	$⊢ (φ \land x \in (1, +∞)) \to 1 + (\frac{1}{\log x}) = \frac{\log x + 1}{\log x}$
166	165	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) (1 + (\frac{1}{\log x})) = (A + 1) (\frac{\log x + 1}{\log x})$
167	161 166	eqtr4d	$⊢ (φ \land x \in (1, +∞)) \to \frac{(A + 1) (\log x + 1)}{\log x} = (A + 1) (1 + (\frac{1}{\log x}))$
168	157 158 167	3brtr3d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x} \leq (A + 1) (1 + (\frac{1}{\log x}))$
169	72	leabsd	$⊢ (φ \land x \in (1, +∞)) \to (A + 1) (1 + (\frac{1}{\log x})) \leq \|(A + 1) (1 + (\frac{1}{\log x}))\|$
170	41 72 87 168 169	letrd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x} \leq \|(A + 1) (1 + (\frac{1}{\log x}))\|$
171	85 170	eqbrtrd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}\| \leq \|(A + 1) (1 + (\frac{1}{\log x}))\|$
172	171	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}\| \leq \|(A + 1) (1 + (\frac{1}{\log x}))\|$
173	5 71 72 73 172	o1le	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}) \in 𝑂 (1)$
174	40 41 58 173	o1add2	$⊢ φ \to (x \in (1, +∞) ⟼ (\frac{ψ (x)}{x \log x}) + (\frac{\sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x})) \in 𝑂 (1)$
175	38 174	eqeltrd	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}) \in 𝑂 (1)$
176	9 20	readdcld	$⊢ (φ \land x \in (1, +∞)) \to ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \in ℝ$
177	176 39	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x} \in ℝ$
178	2	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
179	178	ffvelcdmi	$⊢ \frac{x}{n + 1} \in ℝ^{+} \to R (\frac{x}{n + 1}) \in ℝ$
180	109 179	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) \in ℝ$
181	180	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) \in ℂ$
182	79 76	rpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
183	178	ffvelcdmi	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) \in ℝ$
184	182 183	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℝ$
185	184	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℂ$
186	181 185	subcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) - R (\frac{x}{n}) \in ℂ$
187	186	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℝ$
188	134 187	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℝ$
189	11 188	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℝ$
190	189 39	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x} \in ℝ$
191	190	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x} \in ℂ$
192	76	rpge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq n$
193	186	absge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
194	134 187 192 193	mulge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
195	11 188 194	fsumge0	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
196	189 39 195	divge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}$
197	190 196	absidd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}\| = \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}$
198	10 21	addcld	$⊢ (φ \land x \in (1, +∞)) \to ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \in ℂ$
199	198 28 36	divcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x} \in ℂ$
200	199	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}\| \in ℝ$
201	12 14	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
202		chpcl	$⊢ \frac{x}{n} \in ℝ \to ψ (\frac{x}{n}) \in ℝ$
203	201 202	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℝ$
204	203 201	readdcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) + (\frac{x}{n}) \in ℝ$
205	204 19	resubcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \in ℝ$
206	134 205	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))) \in ℝ$
207	2	pntrval	$⊢ \frac{x}{n + 1} \in ℝ^{+} \to R (\frac{x}{n + 1}) = ψ (\frac{x}{n + 1}) - (\frac{x}{n + 1})$
208	109 207	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) = ψ (\frac{x}{n + 1}) - (\frac{x}{n + 1})$
209	2	pntrval	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) = ψ (\frac{x}{n}) - (\frac{x}{n})$
210	182 209	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) = ψ (\frac{x}{n}) - (\frac{x}{n})$
211	208 210	oveq12d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) - R (\frac{x}{n}) = ψ (\frac{x}{n + 1}) - (\frac{x}{n + 1}) - (ψ (\frac{x}{n}) - (\frac{x}{n}))$
212	18	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) \in ℂ$
213	203	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℂ$
214	113 114 139	divcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℂ$
215	212 120 213 214	sub4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) - (\frac{x}{n + 1}) - (ψ (\frac{x}{n}) - (\frac{x}{n})) = ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n}) - ((\frac{x}{n + 1}) - (\frac{x}{n}))$
216	211 215	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) - R (\frac{x}{n}) = ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n}) - ((\frac{x}{n + 1}) - (\frac{x}{n}))$
217	216	fveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| = \|ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n}) - ((\frac{x}{n + 1}) - (\frac{x}{n}))\|$
218	212 213	subcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n}) \in ℂ$
219	120 214	subcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{x}{n + 1}) - (\frac{x}{n}) \in ℂ$
220	218 219	abs2dif2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n}) - ((\frac{x}{n + 1}) - (\frac{x}{n}))\| \leq \|ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n})\| + \|(\frac{x}{n + 1}) - (\frac{x}{n})\|$
221	217 220	eqbrtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \leq \|ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n})\| + \|(\frac{x}{n + 1}) - (\frac{x}{n})\|$
222	76 78 12 80 135	lediv2ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n + 1} \leq \frac{x}{n}$
223		chpwordi	$⊢ (\frac{x}{n + 1} \in ℝ \land \frac{x}{n} \in ℝ \land \frac{x}{n + 1} \leq \frac{x}{n}) \to ψ (\frac{x}{n + 1}) \leq ψ (\frac{x}{n})$
224	16 201 222 223	syl3anc	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) \leq ψ (\frac{x}{n})$
225	18 203 224	abssuble0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n})\| = ψ (\frac{x}{n}) - ψ (\frac{x}{n + 1})$
226	16 201 222	abssuble0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{x}{n + 1}) - (\frac{x}{n})\| = (\frac{x}{n}) - (\frac{x}{n + 1})$
227	225 226	oveq12d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n})\| + \|(\frac{x}{n + 1}) - (\frac{x}{n})\| = (ψ (\frac{x}{n}) - ψ (\frac{x}{n + 1})) + (\frac{x}{n}) - (\frac{x}{n + 1})$
228	213 214 212 120	addsub4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) = (ψ (\frac{x}{n}) - ψ (\frac{x}{n + 1})) + (\frac{x}{n}) - (\frac{x}{n + 1})$
229	227 228	eqtr4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|ψ (\frac{x}{n + 1}) - ψ (\frac{x}{n})\| + \|(\frac{x}{n + 1}) - (\frac{x}{n})\| = ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
230	221 229	breqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \leq ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
231	187 205 134 192 230	lemul2ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \leq n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))$
232	11 188 206 231	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \leq \sum_{n = 1}^{⌊x⌋} n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))$
233	205	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) \in ℂ$
234	114 233	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))) \in ℂ$
235	11 234	fsumcl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))) \in ℂ$
236	10 21	negdi2d	$⊢ (φ \land x \in (1, +∞)) \to - (ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))) = - ψ (x) - \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
237	33	rprege0d	$⊢ (φ \land x \in (1, +∞)) \to (x \in ℝ \land 0 \leq x)$
238		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
239		nn0p1nn	$⊢ ⌊x⌋ \in ℕ_{0} \to ⌊x⌋ + 1 \in ℕ$
240	237 238 239	3syl	$⊢ (φ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \in ℕ$
241	7 240	nndivred	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} \in ℝ$
242		2re	$⊢ 2 \in ℝ$
243	242	a1i	$⊢ (φ \land x \in (1, +∞)) \to 2 \in ℝ$
244		flltp1	$⊢ x \in ℝ \to x < ⌊x⌋ + 1$
245	7 244	syl	$⊢ (φ \land x \in (1, +∞)) \to x < ⌊x⌋ + 1$
246	240	nncnd	$⊢ (φ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \in ℂ$
247	246	mulridd	$⊢ (φ \land x \in (1, +∞)) \to (⌊x⌋ + 1) \cdot 1 = ⌊x⌋ + 1$
248	245 247	breqtrrd	$⊢ (φ \land x \in (1, +∞)) \to x < (⌊x⌋ + 1) \cdot 1$
249	240	nnrpd	$⊢ (φ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \in ℝ^{+}$
250	7 31 249	ltdivmuld	$⊢ (φ \land x \in (1, +∞)) \to (\frac{x}{⌊x⌋ + 1} < 1 \leftrightarrow x < (⌊x⌋ + 1) \cdot 1)$
251	248 250	mpbird	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} < 1$
252		1lt2	$⊢ 1 < 2$
253	252	a1i	$⊢ (φ \land x \in (1, +∞)) \to 1 < 2$
254	241 31 243 251 253	lttrd	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} < 2$
255		chpeq0	$⊢ \frac{x}{⌊x⌋ + 1} \in ℝ \to (ψ (\frac{x}{⌊x⌋ + 1}) = 0 \leftrightarrow \frac{x}{⌊x⌋ + 1} < 2)$
256	241 255	syl	$⊢ (φ \land x \in (1, +∞)) \to (ψ (\frac{x}{⌊x⌋ + 1}) = 0 \leftrightarrow \frac{x}{⌊x⌋ + 1} < 2)$
257	254 256	mpbird	$⊢ (φ \land x \in (1, +∞)) \to ψ (\frac{x}{⌊x⌋ + 1}) = 0$
258	257	oveq1d	$⊢ (φ \land x \in (1, +∞)) \to ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1}) = 0 + (\frac{x}{⌊x⌋ + 1})$
259	241	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{⌊x⌋ + 1} \in ℂ$
260	259	addlidd	$⊢ (φ \land x \in (1, +∞)) \to 0 + (\frac{x}{⌊x⌋ + 1}) = \frac{x}{⌊x⌋ + 1}$
261	258 260	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1}) = \frac{x}{⌊x⌋ + 1}$
262	261	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to (⌊x⌋ + 1) (ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1})) = (⌊x⌋ + 1) (\frac{x}{⌊x⌋ + 1})$
263	240	nnne0d	$⊢ (φ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \neq 0$
264	22 246 263	divcan2d	$⊢ (φ \land x \in (1, +∞)) \to (⌊x⌋ + 1) (\frac{x}{⌊x⌋ + 1}) = x$
265	262 264	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to (⌊x⌋ + 1) (ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1})) = x$
266	22	div1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{1} = x$
267	266	fveq2d	$⊢ (φ \land x \in (1, +∞)) \to ψ (\frac{x}{1}) = ψ (x)$
268	267 266	oveq12d	$⊢ (φ \land x \in (1, +∞)) \to ψ (\frac{x}{1}) + (\frac{x}{1}) = ψ (x) + x$
269	268	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to 1 (ψ (\frac{x}{1}) + (\frac{x}{1})) = 1 (ψ (x) + x)$
270	9 7	readdcld	$⊢ (φ \land x \in (1, +∞)) \to ψ (x) + x \in ℝ$
271	270	recnd	$⊢ (φ \land x \in (1, +∞)) \to ψ (x) + x \in ℂ$
272	271	mullidd	$⊢ (φ \land x \in (1, +∞)) \to 1 (ψ (x) + x) = ψ (x) + x$
273	269 272	eqtrd	$⊢ (φ \land x \in (1, +∞)) \to 1 (ψ (\frac{x}{1}) + (\frac{x}{1})) = ψ (x) + x$
274	265 273	oveq12d	$⊢ (φ \land x \in (1, +∞)) \to (⌊x⌋ + 1) (ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1})) - 1 (ψ (\frac{x}{1}) + (\frac{x}{1})) = x - (ψ (x) + x)$
275	271 22	negsubdi2d	$⊢ (φ \land x \in (1, +∞)) \to - (ψ (x) + x - x) = x - (ψ (x) + x)$
276	10 22	pncand	$⊢ (φ \land x \in (1, +∞)) \to ψ (x) + x - x = ψ (x)$
277	276	negeqd	$⊢ (φ \land x \in (1, +∞)) \to - (ψ (x) + x - x) = - ψ (x)$
278	274 275 277	3eqtr2d	$⊢ (φ \land x \in (1, +∞)) \to (⌊x⌋ + 1) (ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1})) - 1 (ψ (\frac{x}{1}) + (\frac{x}{1})) = - ψ (x)$
279	7	flcld	$⊢ (φ \land x \in (1, +∞)) \to ⌊x⌋ \in ℤ$
280		fzval3	$⊢ ⌊x⌋ \in ℤ \to (1 \dots ⌊x⌋) = (1 ..^⌊x⌋ + 1)$
281	279 280	syl	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) = (1 ..^⌊x⌋ + 1)$
282	281	eqcomd	$⊢ (φ \land x \in (1, +∞)) \to (1 ..^⌊x⌋ + 1) = (1 \dots ⌊x⌋)$
283	114 115	pncan2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - n = 1$
284	283	oveq1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (n + 1 - n) (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) = 1 (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
285	19	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) \in ℂ$
286	285	mullidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) = ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})$
287	284 286	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (n + 1 - n) (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) = ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})$
288	282 287	sumeq12rdv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} (n + 1 - n) (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) = \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
289	278 288	oveq12d	$⊢ (φ \land x \in (1, +∞)) \to (⌊x⌋ + 1) (ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1})) - 1 (ψ (\frac{x}{1}) + (\frac{x}{1})) - \sum_{n \in (1 ..^⌊x⌋ + 1)} (n + 1 - n) (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) = - ψ (x) - \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
290		oveq2	$⊢ m = n \to \frac{x}{m} = \frac{x}{n}$
291	290	fveq2d	$⊢ m = n \to ψ (\frac{x}{m}) = ψ (\frac{x}{n})$
292	291 290	oveq12d	$⊢ m = n \to ψ (\frac{x}{m}) + (\frac{x}{m}) = ψ (\frac{x}{n}) + (\frac{x}{n})$
293	292	ancli	$⊢ m = n \to (m = n \land ψ (\frac{x}{m}) + (\frac{x}{m}) = ψ (\frac{x}{n}) + (\frac{x}{n}))$
294		oveq2	$⊢ m = n + 1 \to \frac{x}{m} = \frac{x}{n + 1}$
295	294	fveq2d	$⊢ m = n + 1 \to ψ (\frac{x}{m}) = ψ (\frac{x}{n + 1})$
296	295 294	oveq12d	$⊢ m = n + 1 \to ψ (\frac{x}{m}) + (\frac{x}{m}) = ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})$
297	296	ancli	$⊢ m = n + 1 \to (m = n + 1 \land ψ (\frac{x}{m}) + (\frac{x}{m}) = ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
298		oveq2	$⊢ m = 1 \to \frac{x}{m} = \frac{x}{1}$
299	298	fveq2d	$⊢ m = 1 \to ψ (\frac{x}{m}) = ψ (\frac{x}{1})$
300	299 298	oveq12d	$⊢ m = 1 \to ψ (\frac{x}{m}) + (\frac{x}{m}) = ψ (\frac{x}{1}) + (\frac{x}{1})$
301	300	ancli	$⊢ m = 1 \to (m = 1 \land ψ (\frac{x}{m}) + (\frac{x}{m}) = ψ (\frac{x}{1}) + (\frac{x}{1}))$
302		oveq2	$⊢ m = ⌊x⌋ + 1 \to \frac{x}{m} = \frac{x}{⌊x⌋ + 1}$
303	302	fveq2d	$⊢ m = ⌊x⌋ + 1 \to ψ (\frac{x}{m}) = ψ (\frac{x}{⌊x⌋ + 1})$
304	303 302	oveq12d	$⊢ m = ⌊x⌋ + 1 \to ψ (\frac{x}{m}) + (\frac{x}{m}) = ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1})$
305	304	ancli	$⊢ m = ⌊x⌋ + 1 \to (m = ⌊x⌋ + 1 \land ψ (\frac{x}{m}) + (\frac{x}{m}) = ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1}))$
306		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
307	240 306	eleqtrdi	$⊢ (φ \land x \in (1, +∞)) \to ⌊x⌋ + 1 \in ℤ_{\geq 1}$
308		elfznn	$⊢ m \in (1 \dots ⌊x⌋ + 1) \to m \in ℕ$
309	308	adantl	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℕ$
310	309	nncnd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℂ$
311	7	adantr	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to x \in ℝ$
312	311 309	nndivred	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to \frac{x}{m} \in ℝ$
313		chpcl	$⊢ \frac{x}{m} \in ℝ \to ψ (\frac{x}{m}) \in ℝ$
314	312 313	syl	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to ψ (\frac{x}{m}) \in ℝ$
315	314 312	readdcld	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to ψ (\frac{x}{m}) + (\frac{x}{m}) \in ℝ$
316	315	recnd	$⊢ ((φ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋ + 1)) \to ψ (\frac{x}{m}) + (\frac{x}{m}) \in ℂ$
317	293 297 301 305 307 310 316	fsumparts	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} n (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) - (ψ (\frac{x}{n}) + (\frac{x}{n}))) = (⌊x⌋ + 1) (ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1})) - 1 (ψ (\frac{x}{1}) + (\frac{x}{1})) - \sum_{n \in (1 ..^⌊x⌋ + 1)} (n + 1 - n) (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
318	213 214	addcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) + (\frac{x}{n}) \in ℂ$
319	212 120	addcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) \in ℂ$
320	318 319	negsubdi2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to - (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))) = ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) - (ψ (\frac{x}{n}) + (\frac{x}{n}))$
321	320	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n (- (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))) = n (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) - (ψ (\frac{x}{n}) + (\frac{x}{n})))$
322	114 233	mulneg2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n (- (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))) = - n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))$
323	321 322	eqtr3d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) - (ψ (\frac{x}{n}) + (\frac{x}{n}))) = - n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))$
324	282 323	sumeq12rdv	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} n (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}) - (ψ (\frac{x}{n}) + (\frac{x}{n}))) = \sum_{n = 1}^{⌊x⌋} (- n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))))$
325	317 324	eqtr3d	$⊢ (φ \land x \in (1, +∞)) \to (⌊x⌋ + 1) (ψ (\frac{x}{⌊x⌋ + 1}) + (\frac{x}{⌊x⌋ + 1})) - 1 (ψ (\frac{x}{1}) + (\frac{x}{1})) - \sum_{n \in (1 ..^⌊x⌋ + 1)} (n + 1 - n) (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})) = \sum_{n = 1}^{⌊x⌋} (- n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))))$
326	236 289 325	3eqtr2d	$⊢ (φ \land x \in (1, +∞)) \to - (ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))) = \sum_{n = 1}^{⌊x⌋} (- n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))))$
327	11 234	fsumneg	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (- n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))) = - \sum_{n = 1}^{⌊x⌋} n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))$
328	326 327	eqtr2d	$⊢ (φ \land x \in (1, +∞)) \to - \sum_{n = 1}^{⌊x⌋} n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))) = - (ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1})))$
329	235 198 328	neg11d	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} n (ψ (\frac{x}{n}) + (\frac{x}{n}) - (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))) = ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
330	232 329	breqtrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \leq ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))$
331	189 176 39 330	lediv1dd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x} \leq \frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}$
332	177	leabsd	$⊢ (φ \land x \in (1, +∞)) \to \frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x} \leq \|\frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}\|$
333	190 177 200 331 332	letrd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x} \leq \|\frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}\|$
334	197 333	eqbrtrd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}\| \leq \|\frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}\|$
335	334	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}\| \leq \|\frac{ψ (x) + \sum_{n = 1}^{⌊x⌋} (ψ (\frac{x}{n + 1}) + (\frac{x}{n + 1}))}{x \log x}\|$
336	5 175 177 191 335	o1le	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem pntrlog2bndlem2

Proof