chpdifbndlem1

	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$
	chpdifbnd.x	$⊢ φ \to X \in (1, +∞)$
	chpdifbnd.y	$⊢ φ \to Y \in [X, A X]$
Assertion	chpdifbndlem1	$⊢ φ \to ψ (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		chpdifbnd.x	$⊢ φ \to X \in (1, +∞)$
7		chpdifbnd.y	$⊢ φ \to Y \in [X, A X]$
8		ioossre	$⊢ (1, +∞) \subseteq ℝ$
9	8 6	sseldi	$⊢ φ \to X \in ℝ$
10	1	rpred	$⊢ φ \to A \in ℝ$
11	10 9	remulcld	$⊢ φ \to A X \in ℝ$
12		elicc2	$⊢ (X \in ℝ \land A X \in ℝ) \to (Y \in [X, A X] \leftrightarrow (Y \in ℝ \land X \leq Y \land Y \leq A X))$
13	9 11 12	syl2anc	$⊢ φ \to (Y \in [X, A X] \leftrightarrow (Y \in ℝ \land X \leq Y \land Y \leq A X))$
14	7 13	mpbid	$⊢ φ \to (Y \in ℝ \land X \leq Y \land Y \leq A X)$
15	14	simp1d	$⊢ φ \to Y \in ℝ$
16		chpcl	$⊢ Y \in ℝ \to ψ (Y) \in ℝ$
17	15 16	syl	$⊢ φ \to ψ (Y) \in ℝ$
18		chpcl	$⊢ X \in ℝ \to ψ (X) \in ℝ$
19	9 18	syl	$⊢ φ \to ψ (X) \in ℝ$
20	17 19	resubcld	$⊢ φ \to ψ (Y) - ψ (X) \in ℝ$
21		0red	$⊢ φ \to 0 \in ℝ$
22		1re	$⊢ 1 \in ℝ$
23	22	a1i	$⊢ φ \to 1 \in ℝ$
24		0lt1	$⊢ 0 < 1$
25	24	a1i	$⊢ φ \to 0 < 1$
26		eliooord	$⊢ X \in (1, +∞) \to (1 < X \land X < +∞)$
27	6 26	syl	$⊢ φ \to (1 < X \land X < +∞)$
28	27	simpld	$⊢ φ \to 1 < X$
29	21 23 9 25 28	lttrd	$⊢ φ \to 0 < X$
30	9 29	elrpd	$⊢ φ \to X \in ℝ^{+}$
31	30	relogcld	$⊢ φ \to \log X \in ℝ$
32	20 31	remulcld	$⊢ φ \to (ψ (Y) - ψ (X)) \log X \in ℝ$
33		2re	$⊢ 2 \in ℝ$
34	15 9	resubcld	$⊢ φ \to Y - X \in ℝ$
35		remulcl	$⊢ (2 \in ℝ \land Y - X \in ℝ) \to 2 (Y - X) \in ℝ$
36	33 34 35	sylancr	$⊢ φ \to 2 (Y - X) \in ℝ$
37	36 31	remulcld	$⊢ φ \to 2 (Y - X) \log X \in ℝ$
38	3	rpred	$⊢ φ \to B \in ℝ$
39	15 9	readdcld	$⊢ φ \to Y + X \in ℝ$
40	38 39	remulcld	$⊢ φ \to B (Y + X) \in ℝ$
41	1	relogcld	$⊢ φ \to \log A \in ℝ$
42		remulcl	$⊢ (2 \in ℝ \land \log A \in ℝ) \to 2 \log A \in ℝ$
43	33 41 42	sylancr	$⊢ φ \to 2 \log A \in ℝ$
44	43 15	remulcld	$⊢ φ \to 2 \log A Y \in ℝ$
45	40 44	readdcld	$⊢ φ \to B (Y + X) + 2 \log A Y \in ℝ$
46	37 45	readdcld	$⊢ φ \to 2 (Y - X) \log X + B (Y + X) + 2 \log A Y \in ℝ$
47		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
48	10 47	syl	$⊢ φ \to A + 1 \in ℝ$
49	38 48	remulcld	$⊢ φ \to B (A + 1) \in ℝ$
50		remulcl	$⊢ (2 \in ℝ \land A \in ℝ) \to 2 A \in ℝ$
51	33 10 50	sylancr	$⊢ φ \to 2 A \in ℝ$
52	51 41	remulcld	$⊢ φ \to 2 A \log A \in ℝ$
53	49 52	readdcld	$⊢ φ \to B (A + 1) + 2 A \log A \in ℝ$
54	5 53	eqeltrid	$⊢ φ \to C \in ℝ$
55	54 9	remulcld	$⊢ φ \to C X \in ℝ$
56	37 55	readdcld	$⊢ φ \to 2 (Y - X) \log X + C X \in ℝ$
57	17 31	remulcld	$⊢ φ \to ψ (Y) \log X \in ℝ$
58		fzfid	$⊢ φ \to (1 \dots ⌊X⌋) \in Fin$
59	14	simp2d	$⊢ φ \to X \leq Y$
60		flword2	$⊢ (X \in ℝ \land Y \in ℝ \land X \leq Y) \to ⌊Y⌋ \in ℤ_{\geq ⌊X⌋}$
61	9 15 59 60	syl3anc	$⊢ φ \to ⌊Y⌋ \in ℤ_{\geq ⌊X⌋}$
62		fzss2	$⊢ ⌊Y⌋ \in ℤ_{\geq ⌊X⌋} \to (1 \dots ⌊X⌋) \subseteq (1 \dots ⌊Y⌋)$
63	61 62	syl	$⊢ φ \to (1 \dots ⌊X⌋) \subseteq (1 \dots ⌊Y⌋)$
64	63	sselda	$⊢ (φ \land n \in (1 \dots ⌊X⌋)) \to n \in (1 \dots ⌊Y⌋)$
65		elfznn	$⊢ n \in (1 \dots ⌊Y⌋) \to n \in ℕ$
66	65	adantl	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to n \in ℕ$
67		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
68	66 67	syl	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to Λ (n) \in ℝ$
69		nndivre	$⊢ (X \in ℝ \land n \in ℕ) \to \frac{X}{n} \in ℝ$
70	9 65 69	syl2an	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to \frac{X}{n} \in ℝ$
71		chpcl	$⊢ \frac{X}{n} \in ℝ \to ψ (\frac{X}{n}) \in ℝ$
72	70 71	syl	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to ψ (\frac{X}{n}) \in ℝ$
73	68 72	remulcld	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to Λ (n) ψ (\frac{X}{n}) \in ℝ$
74	64 73	syldan	$⊢ (φ \land n \in (1 \dots ⌊X⌋)) \to Λ (n) ψ (\frac{X}{n}) \in ℝ$
75	58 74	fsumrecl	$⊢ φ \to \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \in ℝ$
76	57 75	readdcld	$⊢ φ \to ψ (Y) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \in ℝ$
77		remulcl	$⊢ (2 \in ℝ \land \log X \in ℝ) \to 2 \log X \in ℝ$
78	33 31 77	sylancr	$⊢ φ \to 2 \log X \in ℝ$
79	78 38	resubcld	$⊢ φ \to 2 \log X - B \in ℝ$
80	79 9	remulcld	$⊢ φ \to (2 \log X - B) X \in ℝ$
81	1 30	rpmulcld	$⊢ φ \to A X \in ℝ^{+}$
82	81	relogcld	$⊢ φ \to \log A X \in ℝ$
83		remulcl	$⊢ (2 \in ℝ \land \log A X \in ℝ) \to 2 \log A X \in ℝ$
84	33 82 83	sylancr	$⊢ φ \to 2 \log A X \in ℝ$
85	38 84	readdcld	$⊢ φ \to B + 2 \log A X \in ℝ$
86	85 15	remulcld	$⊢ φ \to (B + 2 \log A X) Y \in ℝ$
87	19 31	remulcld	$⊢ φ \to ψ (X) \log X \in ℝ$
88	87 75	readdcld	$⊢ φ \to ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \in ℝ$
89	21 9 15 29 59	ltletrd	$⊢ φ \to 0 < Y$
90	15 89	elrpd	$⊢ φ \to Y \in ℝ^{+}$
91	90	relogcld	$⊢ φ \to \log Y \in ℝ$
92	17 91	remulcld	$⊢ φ \to ψ (Y) \log Y \in ℝ$
93		fzfid	$⊢ φ \to (1 \dots ⌊Y⌋) \in Fin$
94		nndivre	$⊢ (Y \in ℝ \land n \in ℕ) \to \frac{Y}{n} \in ℝ$
95	15 65 94	syl2an	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to \frac{Y}{n} \in ℝ$
96		chpcl	$⊢ \frac{Y}{n} \in ℝ \to ψ (\frac{Y}{n}) \in ℝ$
97	95 96	syl	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to ψ (\frac{Y}{n}) \in ℝ$
98	68 97	remulcld	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to Λ (n) ψ (\frac{Y}{n}) \in ℝ$
99	93 98	fsumrecl	$⊢ φ \to \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n}) \in ℝ$
100	92 99	readdcld	$⊢ φ \to ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n}) \in ℝ$
101		chpge0	$⊢ Y \in ℝ \to 0 \leq ψ (Y)$
102	15 101	syl	$⊢ φ \to 0 \leq ψ (Y)$
103	30 90	logled	$⊢ φ \to (X \leq Y \leftrightarrow \log X \leq \log Y)$
104	59 103	mpbid	$⊢ φ \to \log X \leq \log Y$
105	31 91 17 102 104	lemul2ad	$⊢ φ \to ψ (Y) \log X \leq ψ (Y) \log Y$
106	93 73	fsumrecl	$⊢ φ \to \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{X}{n}) \in ℝ$
107		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
108	66 107	syl	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to 0 \leq Λ (n)$
109		chpge0	$⊢ \frac{X}{n} \in ℝ \to 0 \leq ψ (\frac{X}{n})$
110	70 109	syl	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to 0 \leq ψ (\frac{X}{n})$
111	68 72 108 110	mulge0d	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to 0 \leq Λ (n) ψ (\frac{X}{n})$
112	93 73 111 63	fsumless	$⊢ φ \to \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \leq \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{X}{n})$
113	9	adantr	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to X \in ℝ$
114	15	adantr	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to Y \in ℝ$
115	66	nnrpd	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to n \in ℝ^{+}$
116	59	adantr	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to X \leq Y$
117	113 114 115 116	lediv1dd	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to \frac{X}{n} \leq \frac{Y}{n}$
118		chpwordi	$⊢ (\frac{X}{n} \in ℝ \land \frac{Y}{n} \in ℝ \land \frac{X}{n} \leq \frac{Y}{n}) \to ψ (\frac{X}{n}) \leq ψ (\frac{Y}{n})$
119	70 95 117 118	syl3anc	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to ψ (\frac{X}{n}) \leq ψ (\frac{Y}{n})$
120	72 97 68 108 119	lemul2ad	$⊢ (φ \land n \in (1 \dots ⌊Y⌋)) \to Λ (n) ψ (\frac{X}{n}) \leq Λ (n) ψ (\frac{Y}{n})$
121	93 73 98 120	fsumle	$⊢ φ \to \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{X}{n}) \leq \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})$
122	75 106 99 112 121	letrd	$⊢ φ \to \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \leq \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})$
123	57 75 92 99 105 122	le2addd	$⊢ φ \to ψ (Y) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \leq ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})$
124	100 90	rerpdivcld	$⊢ φ \to \frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y} \in ℝ$
125		remulcl	$⊢ (2 \in ℝ \land \log Y \in ℝ) \to 2 \log Y \in ℝ$
126	33 91 125	sylancr	$⊢ φ \to 2 \log Y \in ℝ$
127	38 126	readdcld	$⊢ φ \to B + 2 \log Y \in ℝ$
128	124 126	resubcld	$⊢ φ \to (\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y \in ℝ$
129	128	recnd	$⊢ φ \to (\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y \in ℂ$
130	129	abscld	$⊢ φ \to \|(\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y\| \in ℝ$
131	128	leabsd	$⊢ φ \to (\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y \leq \|(\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y\|$
132		fveq2	$⊢ z = Y \to ψ (z) = ψ (Y)$
133		fveq2	$⊢ z = Y \to \log z = \log Y$
134	132 133	oveq12d	$⊢ z = Y \to ψ (z) \log z = ψ (Y) \log Y$
135		fveq2	$⊢ m = n \to Λ (m) = Λ (n)$
136		oveq2	$⊢ m = n \to \frac{z}{m} = \frac{z}{n}$
137	136	fveq2d	$⊢ m = n \to ψ (\frac{z}{m}) = ψ (\frac{z}{n})$
138	135 137	oveq12d	$⊢ m = n \to Λ (m) ψ (\frac{z}{m}) = Λ (n) ψ (\frac{z}{n})$
139	138	cbvsumv	$⊢ \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m}) = \sum_{n = 1}^{⌊z⌋} Λ (n) ψ (\frac{z}{n})$
140		fveq2	$⊢ z = Y \to ⌊z⌋ = ⌊Y⌋$
141	140	oveq2d	$⊢ z = Y \to (1 \dots ⌊z⌋) = (1 \dots ⌊Y⌋)$
142		simpl	$⊢ (z = Y \land n \in (1 \dots ⌊Y⌋)) \to z = Y$
143	142	fvoveq1d	$⊢ (z = Y \land n \in (1 \dots ⌊Y⌋)) \to ψ (\frac{z}{n}) = ψ (\frac{Y}{n})$
144	143	oveq2d	$⊢ (z = Y \land n \in (1 \dots ⌊Y⌋)) \to Λ (n) ψ (\frac{z}{n}) = Λ (n) ψ (\frac{Y}{n})$
145	141 144	sumeq12rdv	$⊢ z = Y \to \sum_{n = 1}^{⌊z⌋} Λ (n) ψ (\frac{z}{n}) = \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})$
146	139 145	syl5eq	$⊢ z = Y \to \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m}) = \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})$
147	134 146	oveq12d	$⊢ z = Y \to ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m}) = ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})$
148		id	$⊢ z = Y \to z = Y$
149	147 148	oveq12d	$⊢ z = Y \to \frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z} = \frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}$
150	133	oveq2d	$⊢ z = Y \to 2 \log z = 2 \log Y$
151	149 150	oveq12d	$⊢ z = Y \to (\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z = (\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y$
152	151	fveq2d	$⊢ z = Y \to \|(\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z\| = \|(\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y\|$
153	152	breq1d	$⊢ z = Y \to (\|(\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z\| \leq B \leftrightarrow \|(\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y\| \leq B)$
154	23 9 28	ltled	$⊢ φ \to 1 \leq X$
155	23 9 15 154 59	letrd	$⊢ φ \to 1 \leq Y$
156		elicopnf	$⊢ 1 \in ℝ \to (Y \in [1, +∞) \leftrightarrow (Y \in ℝ \land 1 \leq Y))$
157	22 156	ax-mp	$⊢ Y \in [1, +∞) \leftrightarrow (Y \in ℝ \land 1 \leq Y)$
158	15 155 157	sylanbrc	$⊢ φ \to Y \in [1, +∞)$
159	153 4 158	rspcdva	$⊢ φ \to \|(\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y\| \leq B$
160	128 130 38 131 159	letrd	$⊢ φ \to (\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y \leq B$
161	124 126 38	lesubaddd	$⊢ φ \to ((\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y}) - 2 \log Y \leq B \leftrightarrow \frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y} \leq B + 2 \log Y)$
162	160 161	mpbid	$⊢ φ \to \frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y} \leq B + 2 \log Y$
163	14	simp3d	$⊢ φ \to Y \leq A X$
164	90 81	logled	$⊢ φ \to (Y \leq A X \leftrightarrow \log Y \leq \log A X)$
165	163 164	mpbid	$⊢ φ \to \log Y \leq \log A X$
166		2pos	$⊢ 0 < 2$
167	33 166	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
168	167	a1i	$⊢ φ \to (2 \in ℝ \land 0 < 2)$
169		lemul2	$⊢ (\log Y \in ℝ \land \log A X \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\log Y \leq \log A X \leftrightarrow 2 \log Y \leq 2 \log A X)$
170	91 82 168 169	syl3anc	$⊢ φ \to (\log Y \leq \log A X \leftrightarrow 2 \log Y \leq 2 \log A X)$
171	165 170	mpbid	$⊢ φ \to 2 \log Y \leq 2 \log A X$
172	126 84 38 171	leadd2dd	$⊢ φ \to B + 2 \log Y \leq B + 2 \log A X$
173	124 127 85 162 172	letrd	$⊢ φ \to \frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y} \leq B + 2 \log A X$
174	100 85 90	ledivmul2d	$⊢ φ \to (\frac{ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n})}{Y} \leq B + 2 \log A X \leftrightarrow ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n}) \leq (B + 2 \log A X) Y)$
175	173 174	mpbid	$⊢ φ \to ψ (Y) \log Y + \sum_{n = 1}^{⌊Y⌋} Λ (n) ψ (\frac{Y}{n}) \leq (B + 2 \log A X) Y$
176	76 100 86 123 175	letrd	$⊢ φ \to ψ (Y) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \leq (B + 2 \log A X) Y$
177		fveq2	$⊢ z = X \to ψ (z) = ψ (X)$
178		fveq2	$⊢ z = X \to \log z = \log X$
179	177 178	oveq12d	$⊢ z = X \to ψ (z) \log z = ψ (X) \log X$
180		fveq2	$⊢ z = X \to ⌊z⌋ = ⌊X⌋$
181	180	oveq2d	$⊢ z = X \to (1 \dots ⌊z⌋) = (1 \dots ⌊X⌋)$
182		simpl	$⊢ (z = X \land n \in (1 \dots ⌊X⌋)) \to z = X$
183	182	fvoveq1d	$⊢ (z = X \land n \in (1 \dots ⌊X⌋)) \to ψ (\frac{z}{n}) = ψ (\frac{X}{n})$
184	183	oveq2d	$⊢ (z = X \land n \in (1 \dots ⌊X⌋)) \to Λ (n) ψ (\frac{z}{n}) = Λ (n) ψ (\frac{X}{n})$
185	181 184	sumeq12rdv	$⊢ z = X \to \sum_{n = 1}^{⌊z⌋} Λ (n) ψ (\frac{z}{n}) = \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})$
186	139 185	syl5eq	$⊢ z = X \to \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m}) = \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})$
187	179 186	oveq12d	$⊢ z = X \to ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m}) = ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})$
188		id	$⊢ z = X \to z = X$
189	187 188	oveq12d	$⊢ z = X \to \frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z} = \frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X}$
190	178	oveq2d	$⊢ z = X \to 2 \log z = 2 \log X$
191	189 190	oveq12d	$⊢ z = X \to (\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z = (\frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X}) - 2 \log X$
192	191	fveq2d	$⊢ z = X \to \|(\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z\| = \|(\frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X}) - 2 \log X\|$
193	192	breq1d	$⊢ z = X \to (\|(\frac{ψ (z) \log z + \sum_{m = 1}^{⌊z⌋} Λ (m) ψ (\frac{z}{m})}{z}) - 2 \log z\| \leq B \leftrightarrow \|(\frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X}) - 2 \log X\| \leq B)$
194		elicopnf	$⊢ 1 \in ℝ \to (X \in [1, +∞) \leftrightarrow (X \in ℝ \land 1 \leq X))$
195	22 194	ax-mp	$⊢ X \in [1, +∞) \leftrightarrow (X \in ℝ \land 1 \leq X)$
196	9 154 195	sylanbrc	$⊢ φ \to X \in [1, +∞)$
197	193 4 196	rspcdva	$⊢ φ \to \|(\frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X}) - 2 \log X\| \leq B$
198	88 30	rerpdivcld	$⊢ φ \to \frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X} \in ℝ$
199	198 78 38	absdifled	$⊢ φ \to (\|(\frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X}) - 2 \log X\| \leq B \leftrightarrow (2 \log X - B \leq \frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X} \land \frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X} \leq 2 \log X + B))$
200	197 199	mpbid	$⊢ φ \to (2 \log X - B \leq \frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X} \land \frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X} \leq 2 \log X + B)$
201	200	simpld	$⊢ φ \to 2 \log X - B \leq \frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X}$
202	79 88 30	lemuldivd	$⊢ φ \to ((2 \log X - B) X \leq ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \leftrightarrow 2 \log X - B \leq \frac{ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})}{X})$
203	201 202	mpbird	$⊢ φ \to (2 \log X - B) X \leq ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})$
204	76 80 86 88 176 203	le2subd	$⊢ φ \to ψ (Y) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) - (ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})) \leq (B + 2 \log A X) Y - (2 \log X - B) X$
205	57	recnd	$⊢ φ \to ψ (Y) \log X \in ℂ$
206	87	recnd	$⊢ φ \to ψ (X) \log X \in ℂ$
207	75	recnd	$⊢ φ \to \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) \in ℂ$
208	205 206 207	pnpcan2d	$⊢ φ \to ψ (Y) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) - (ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})) = ψ (Y) \log X - ψ (X) \log X$
209	17	recnd	$⊢ φ \to ψ (Y) \in ℂ$
210	19	recnd	$⊢ φ \to ψ (X) \in ℂ$
211	31	recnd	$⊢ φ \to \log X \in ℂ$
212	209 210 211	subdird	$⊢ φ \to (ψ (Y) - ψ (X)) \log X = ψ (Y) \log X - ψ (X) \log X$
213	208 212	eqtr4d	$⊢ φ \to ψ (Y) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n}) - (ψ (X) \log X + \sum_{n = 1}^{⌊X⌋} Λ (n) ψ (\frac{X}{n})) = (ψ (Y) - ψ (X)) \log X$
214	78 15	remulcld	$⊢ φ \to 2 \log X Y \in ℝ$
215	214	recnd	$⊢ φ \to 2 \log X Y \in ℂ$
216	38 43	readdcld	$⊢ φ \to B + 2 \log A \in ℝ$
217	216 15	remulcld	$⊢ φ \to (B + 2 \log A) Y \in ℝ$
218	217	recnd	$⊢ φ \to (B + 2 \log A) Y \in ℂ$
219	78 9	remulcld	$⊢ φ \to 2 \log X X \in ℝ$
220	219	recnd	$⊢ φ \to 2 \log X X \in ℂ$
221	38 9	remulcld	$⊢ φ \to B X \in ℝ$
222	221	recnd	$⊢ φ \to B X \in ℂ$
223	222	negcld	$⊢ φ \to - B X \in ℂ$
224	215 218 220 223	addsub4d	$⊢ φ \to 2 \log X Y + (B + 2 \log A) Y - (2 \log X X + (- B X)) = (2 \log X Y - 2 \log X X) + (B + 2 \log A) Y - (- B X)$
225	41	recnd	$⊢ φ \to \log A \in ℂ$
226	1 30	relogmuld	$⊢ φ \to \log A X = \log A + \log X$
227	225 211 226	comraddd	$⊢ φ \to \log A X = \log X + \log A$
228	227	oveq2d	$⊢ φ \to 2 \log A X = 2 (\log X + \log A)$
229		2cnd	$⊢ φ \to 2 \in ℂ$
230	229 211 225	adddid	$⊢ φ \to 2 (\log X + \log A) = 2 \log X + 2 \log A$
231	228 230	eqtrd	$⊢ φ \to 2 \log A X = 2 \log X + 2 \log A$
232	231	oveq2d	$⊢ φ \to B + 2 \log A X = B + 2 \log X + 2 \log A$
233	38	recnd	$⊢ φ \to B \in ℂ$
234	78	recnd	$⊢ φ \to 2 \log X \in ℂ$
235	43	recnd	$⊢ φ \to 2 \log A \in ℂ$
236	233 234 235	add12d	$⊢ φ \to B + 2 \log X + 2 \log A = 2 \log X + B + 2 \log A$
237	232 236	eqtrd	$⊢ φ \to B + 2 \log A X = 2 \log X + B + 2 \log A$
238	237	oveq1d	$⊢ φ \to (B + 2 \log A X) Y = (2 \log X + B + 2 \log A) Y$
239	216	recnd	$⊢ φ \to B + 2 \log A \in ℂ$
240	15	recnd	$⊢ φ \to Y \in ℂ$
241	234 239 240	adddird	$⊢ φ \to (2 \log X + B + 2 \log A) Y = 2 \log X Y + (B + 2 \log A) Y$
242	238 241	eqtrd	$⊢ φ \to (B + 2 \log A X) Y = 2 \log X Y + (B + 2 \log A) Y$
243	9	recnd	$⊢ φ \to X \in ℂ$
244	234 233 243	subdird	$⊢ φ \to (2 \log X - B) X = 2 \log X X - B X$
245	220 222	negsubd	$⊢ φ \to 2 \log X X + (- B X) = 2 \log X X - B X$
246	244 245	eqtr4d	$⊢ φ \to (2 \log X - B) X = 2 \log X X + (- B X)$
247	242 246	oveq12d	$⊢ φ \to (B + 2 \log A X) Y - (2 \log X - B) X = 2 \log X Y + (B + 2 \log A) Y - (2 \log X X + (- B X))$
248	34	recnd	$⊢ φ \to Y - X \in ℂ$
249	229 248 211	mul32d	$⊢ φ \to 2 (Y - X) \log X = 2 \log X (Y - X)$
250	234 240 243	subdid	$⊢ φ \to 2 \log X (Y - X) = 2 \log X Y - 2 \log X X$
251	249 250	eqtrd	$⊢ φ \to 2 (Y - X) \log X = 2 \log X Y - 2 \log X X$
252	38 15	remulcld	$⊢ φ \to B Y \in ℝ$
253	252	recnd	$⊢ φ \to B Y \in ℂ$
254	44	recnd	$⊢ φ \to 2 \log A Y \in ℂ$
255	253 222 254	add32d	$⊢ φ \to B Y + B X + 2 \log A Y = B Y + 2 \log A Y + B X$
256	233 240 243	adddid	$⊢ φ \to B (Y + X) = B Y + B X$
257	256	oveq1d	$⊢ φ \to B (Y + X) + 2 \log A Y = B Y + B X + 2 \log A Y$
258	233 235 240	adddird	$⊢ φ \to (B + 2 \log A) Y = B Y + 2 \log A Y$
259	258	oveq1d	$⊢ φ \to (B + 2 \log A) Y + B X = B Y + 2 \log A Y + B X$
260	255 257 259	3eqtr4d	$⊢ φ \to B (Y + X) + 2 \log A Y = (B + 2 \log A) Y + B X$
261	218 222	subnegd	$⊢ φ \to (B + 2 \log A) Y - (- B X) = (B + 2 \log A) Y + B X$
262	260 261	eqtr4d	$⊢ φ \to B (Y + X) + 2 \log A Y = (B + 2 \log A) Y - (- B X)$
263	251 262	oveq12d	$⊢ φ \to 2 (Y - X) \log X + B (Y + X) + 2 \log A Y = (2 \log X Y - 2 \log X X) + (B + 2 \log A) Y - (- B X)$
264	224 247 263	3eqtr4d	$⊢ φ \to (B + 2 \log A X) Y - (2 \log X - B) X = 2 (Y - X) \log X + B (Y + X) + 2 \log A Y$
265	204 213 264	3brtr3d	$⊢ φ \to (ψ (Y) - ψ (X)) \log X \leq 2 (Y - X) \log X + B (Y + X) + 2 \log A Y$
266	49 9	remulcld	$⊢ φ \to B (A + 1) X \in ℝ$
267	52 9	remulcld	$⊢ φ \to 2 A \log A X \in ℝ$
268	15 11 9 163	leadd1dd	$⊢ φ \to Y + X \leq A X + X$
269	10	recnd	$⊢ φ \to A \in ℂ$
270	269 243	adddirp1d	$⊢ φ \to (A + 1) X = A X + X$
271	268 270	breqtrrd	$⊢ φ \to Y + X \leq (A + 1) X$
272	48 9	remulcld	$⊢ φ \to (A + 1) X \in ℝ$
273	39 272 3	lemul2d	$⊢ φ \to (Y + X \leq (A + 1) X \leftrightarrow B (Y + X) \leq B (A + 1) X)$
274	271 273	mpbid	$⊢ φ \to B (Y + X) \leq B (A + 1) X$
275	48	recnd	$⊢ φ \to A + 1 \in ℂ$
276	233 275 243	mulassd	$⊢ φ \to B (A + 1) X = B (A + 1) X$
277	274 276	breqtrrd	$⊢ φ \to B (Y + X) \leq B (A + 1) X$
278	33	a1i	$⊢ φ \to 2 \in ℝ$
279		0le2	$⊢ 0 \leq 2$
280	279	a1i	$⊢ φ \to 0 \leq 2$
281		log1	$⊢ \log 1 = 0$
282		1rp	$⊢ 1 \in ℝ^{+}$
283		logleb	$⊢ (1 \in ℝ^{+} \land A \in ℝ^{+}) \to (1 \leq A \leftrightarrow \log 1 \leq \log A)$
284	282 1 283	sylancr	$⊢ φ \to (1 \leq A \leftrightarrow \log 1 \leq \log A)$
285	2 284	mpbid	$⊢ φ \to \log 1 \leq \log A$
286	281 285	eqbrtrrid	$⊢ φ \to 0 \leq \log A$
287	278 41 280 286	mulge0d	$⊢ φ \to 0 \leq 2 \log A$
288	15 11 43 287 163	lemul2ad	$⊢ φ \to 2 \log A Y \leq 2 \log A A X$
289	51	recnd	$⊢ φ \to 2 A \in ℂ$
290	289 225 243	mulassd	$⊢ φ \to 2 A \log A X = 2 A \log A X$
291	229 269 225 243	mul4d	$⊢ φ \to 2 A \log A X = 2 \log A A X$
292	290 291	eqtrd	$⊢ φ \to 2 A \log A X = 2 \log A A X$
293	288 292	breqtrrd	$⊢ φ \to 2 \log A Y \leq 2 A \log A X$
294	40 44 266 267 277 293	le2addd	$⊢ φ \to B (Y + X) + 2 \log A Y \leq B (A + 1) X + 2 A \log A X$
295	5	oveq1i	$⊢ C X = (B (A + 1) + 2 A \log A) X$
296	49	recnd	$⊢ φ \to B (A + 1) \in ℂ$
297	52	recnd	$⊢ φ \to 2 A \log A \in ℂ$
298	296 297 243	adddird	$⊢ φ \to (B (A + 1) + 2 A \log A) X = B (A + 1) X + 2 A \log A X$
299	295 298	syl5eq	$⊢ φ \to C X = B (A + 1) X + 2 A \log A X$
300	294 299	breqtrrd	$⊢ φ \to B (Y + X) + 2 \log A Y \leq C X$
301	45 55 37 300	leadd2dd	$⊢ φ \to 2 (Y - X) \log X + B (Y + X) + 2 \log A Y \leq 2 (Y - X) \log X + C X$
302	32 46 56 265 301	letrd	$⊢ φ \to (ψ (Y) - ψ (X)) \log X \leq 2 (Y - X) \log X + C X$
303	36	recnd	$⊢ φ \to 2 (Y - X) \in ℂ$
304	9 28	rplogcld	$⊢ φ \to \log X \in ℝ^{+}$
305	9 304	rerpdivcld	$⊢ φ \to \frac{X}{\log X} \in ℝ$
306	54 305	remulcld	$⊢ φ \to C (\frac{X}{\log X}) \in ℝ$
307	306	recnd	$⊢ φ \to C (\frac{X}{\log X}) \in ℂ$
308	303 307 211	adddird	$⊢ φ \to (2 (Y - X) + C (\frac{X}{\log X})) \log X = 2 (Y - X) \log X + C (\frac{X}{\log X}) \log X$
309	54	recnd	$⊢ φ \to C \in ℂ$
310	305	recnd	$⊢ φ \to \frac{X}{\log X} \in ℂ$
311	309 310 211	mulassd	$⊢ φ \to C (\frac{X}{\log X}) \log X = C (\frac{X}{\log X}) \log X$
312	304	rpne0d	$⊢ φ \to \log X \neq 0$
313	243 211 312	divcan1d	$⊢ φ \to (\frac{X}{\log X}) \log X = X$
314	313	oveq2d	$⊢ φ \to C (\frac{X}{\log X}) \log X = C X$
315	311 314	eqtrd	$⊢ φ \to C (\frac{X}{\log X}) \log X = C X$
316	315	oveq2d	$⊢ φ \to 2 (Y - X) \log X + C (\frac{X}{\log X}) \log X = 2 (Y - X) \log X + C X$
317	308 316	eqtrd	$⊢ φ \to (2 (Y - X) + C (\frac{X}{\log X})) \log X = 2 (Y - X) \log X + C X$
318	302 317	breqtrrd	$⊢ φ \to (ψ (Y) - ψ (X)) \log X \leq (2 (Y - X) + C (\frac{X}{\log X})) \log X$
319	36 306	readdcld	$⊢ φ \to 2 (Y - X) + C (\frac{X}{\log X}) \in ℝ$
320	20 319 304	lemul1d	$⊢ φ \to (ψ (Y) - ψ (X) \leq 2 (Y - X) + C (\frac{X}{\log X}) \leftrightarrow (ψ (Y) - ψ (X)) \log X \leq (2 (Y - X) + C (\frac{X}{\log X})) \log X)$
321	318 320	mpbird	$⊢ φ \to ψ (Y) - ψ (X) \leq 2 (Y - X) + C (\frac{X}{\log X})$

Metamath Proof Explorer

Theorem chpdifbndlem1

Proof