chpdifbndlem2

	Ref	Expression
Hypotheses	chpdifbnd.a	$⊢ φ \to A \in ℝ^{+}$
	chpdifbnd.1	$⊢ φ \to 1 \leq A$
	chpdifbnd.b	$⊢ φ \to B \in ℝ^{+}$
	chpdifbnd.2	$⊢ φ \to \forall z \in [1, +∞) \|(\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z\| \leq B$
	chpdifbnd.c	$⊢ C = B (A + 1) + 2 A \log A$
Assertion	chpdifbndlem2	$⊢ φ \to \exists c \in ℝ^{+} \forall x \in (1, +∞) \forall y \in [x, A x] ψ (y) - ψ (x) \leq 2 (y - x) + c (\frac{x}{\log x})$

Proof

Step	Hyp	Ref	Expression
1		chpdifbnd.a	$⊢ φ \to A \in ℝ^{+}$
2		chpdifbnd.1	$⊢ φ \to 1 \leq A$
3		chpdifbnd.b	$⊢ φ \to B \in ℝ^{+}$
4		chpdifbnd.2	$⊢ φ \to \forall z \in [1, +∞) \|(\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z\| \leq B$
5		chpdifbnd.c	$⊢ C = B (A + 1) + 2 A \log A$
6		1rp	$⊢ 1 \in ℝ^{+}$
7		rpaddcl	$⊢ (A \in ℝ^{+} \land 1 \in ℝ^{+}) \to A + 1 \in ℝ^{+}$
8	1 6 7	sylancl	$⊢ φ \to A + 1 \in ℝ^{+}$
9	3 8	rpmulcld	$⊢ φ \to B (A + 1) \in ℝ^{+}$
10	9	rpred	$⊢ φ \to B (A + 1) \in ℝ$
11		2rp	$⊢ 2 \in ℝ^{+}$
12		rpmulcl	$⊢ (2 \in ℝ^{+} \land A \in ℝ^{+}) \to 2 A \in ℝ^{+}$
13	11 1 12	sylancr	$⊢ φ \to 2 A \in ℝ^{+}$
14	13	rpred	$⊢ φ \to 2 A \in ℝ$
15	1	relogcld	$⊢ φ \to \log A \in ℝ$
16	14 15	remulcld	$⊢ φ \to 2 A \log A \in ℝ$
17	10 16	readdcld	$⊢ φ \to B (A + 1) + 2 A \log A \in ℝ$
18	9	rpgt0d	$⊢ φ \to 0 < B (A + 1)$
19	13	rprege0d	$⊢ φ \to (2 A \in ℝ \land 0 \leq 2 A)$
20		log1	$⊢ \log 1 = 0$
21		logleb	$⊢ (1 \in ℝ^{+} \land A \in ℝ^{+}) \to (1 \leq A \leftrightarrow \log 1 \leq \log A)$
22	6 1 21	sylancr	$⊢ φ \to (1 \leq A \leftrightarrow \log 1 \leq \log A)$
23	2 22	mpbid	$⊢ φ \to \log 1 \leq \log A$
24	20 23	eqbrtrrid	$⊢ φ \to 0 \leq \log A$
25		mulge0	$⊢ ((2 A \in ℝ \land 0 \leq 2 A) \land (\log A \in ℝ \land 0 \leq \log A)) \to 0 \leq 2 A \log A$
26	19 15 24 25	syl12anc	$⊢ φ \to 0 \leq 2 A \log A$
27	10 16 18 26	addgtge0d	$⊢ φ \to 0 < B (A + 1) + 2 A \log A$
28	17 27	elrpd	$⊢ φ \to B (A + 1) + 2 A \log A \in ℝ^{+}$
29	5 28	eqeltrid	$⊢ φ \to C \in ℝ^{+}$
30	1	adantr	$⊢ (φ \land (x \in (1, +∞) \land y \in [x, A x])) \to A \in ℝ^{+}$
31	2	adantr	$⊢ (φ \land (x \in (1, +∞) \land y \in [x, A x])) \to 1 \leq A$
32	3	adantr	$⊢ (φ \land (x \in (1, +∞) \land y \in [x, A x])) \to B \in ℝ^{+}$
33	4	adantr	$⊢ (φ \land (x \in (1, +∞) \land y \in [x, A x])) \to \forall z \in [1, +∞) \|(\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z\| \leq B$
34		simprl	$⊢ (φ \land (x \in (1, +∞) \land y \in [x, A x])) \to x \in (1, +∞)$
35		simprr	$⊢ (φ \land (x \in (1, +∞) \land y \in [x, A x])) \to y \in [x, A x]$
36	30 31 32 33 5 34 35	chpdifbndlem1	$⊢ (φ \land (x \in (1, +∞) \land y \in [x, A x])) \to ψ (y) - ψ (x) \leq 2 (y - x) + C (\frac{x}{\log x})$
37	36	ralrimivva	$⊢ φ \to \forall x \in (1, +∞) \forall y \in [x, A x] ψ (y) - ψ (x) \leq 2 (y - x) + C (\frac{x}{\log x})$
38		oveq1	$⊢ c = C \to c (\frac{x}{\log x}) = C (\frac{x}{\log x})$
39	38	oveq2d	$⊢ c = C \to 2 (y - x) + c (\frac{x}{\log x}) = 2 (y - x) + C (\frac{x}{\log x})$
40	39	breq2d	$⊢ c = C \to (ψ (y) - ψ (x) \leq 2 (y - x) + c (\frac{x}{\log x}) \leftrightarrow ψ (y) - ψ (x) \leq 2 (y - x) + C (\frac{x}{\log x}))$
41	40	2ralbidv	$⊢ c = C \to (\forall x \in (1, +∞) \forall y \in [x, A x] ψ (y) - ψ (x) \leq 2 (y - x) + c (\frac{x}{\log x}) \leftrightarrow \forall x \in (1, +∞) \forall y \in [x, A x] ψ (y) - ψ (x) \leq 2 (y - x) + C (\frac{x}{\log x}))$
42	41	rspcev	$⊢ (C \in ℝ^{+} \land \forall x \in (1, +∞) \forall y \in [x, A x] ψ (y) - ψ (x) \leq 2 (y - x) + C (\frac{x}{\log x})) \to \exists c \in ℝ^{+} \forall x \in (1, +∞) \forall y \in [x, A x] ψ (y) - ψ (x) \leq 2 (y - x) + c (\frac{x}{\log x})$
43	29 37 42	syl2anc	$⊢ φ \to \exists c \in ℝ^{+} \forall x \in (1, +∞) \forall y \in [x, A x] ψ (y) - ψ (x) \leq 2 (y - x) + c (\frac{x}{\log x})$

Metamath Proof Explorer

Theorem chpdifbndlem2

Proof