pntibndlem3

	Ref	Expression
Hypotheses	pntibnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntibndlem1.1	$⊢ φ \to A \in ℝ^{+}$
	pntibndlem1.l	$⊢ L = \frac{\frac{1}{4}}{A + 3}$
	pntibndlem3.2	$⊢ φ \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
	pntibndlem3.3	$⊢ φ \to B \in ℝ^{+}$
	pntibndlem3.k	$⊢ K = e^{\frac{B}{\frac{E}{2}}}$
	pntibndlem3.c	$⊢ C = 2 B + \log 2$
	pntibndlem3.4	$⊢ φ \to E \in (0, 1)$
	pntibndlem3.6	$⊢ φ \to Z \in ℝ^{+}$
	pntibndlem3.5	$⊢ φ \to \forall m \in [K, +∞) \forall v \in (Z, +∞) \exists i \in ℕ ((v < i \land i \leq m v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2})$
Assertion	pntibndlem3	$⊢ φ \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$

Proof

Step	Hyp	Ref	Expression
1		pntibnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		pntibndlem1.1	$⊢ φ \to A \in ℝ^{+}$
3		pntibndlem1.l	$⊢ L = \frac{\frac{1}{4}}{A + 3}$
4		pntibndlem3.2	$⊢ φ \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
5		pntibndlem3.3	$⊢ φ \to B \in ℝ^{+}$
6		pntibndlem3.k	$⊢ K = e^{\frac{B}{\frac{E}{2}}}$
7		pntibndlem3.c	$⊢ C = 2 B + \log 2$
8		pntibndlem3.4	$⊢ φ \to E \in (0, 1)$
9		pntibndlem3.6	$⊢ φ \to Z \in ℝ^{+}$
10		pntibndlem3.5	$⊢ φ \to \forall m \in [K, +∞) \forall v \in (Z, +∞) \exists i \in ℕ ((v < i \land i \leq m v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2})$
11		2re	$⊢ 2 \in ℝ$
12		1le2	$⊢ 1 \leq 2$
13		chpdifbnd	$⊢ (2 \in ℝ \land 1 \leq 2) \to \exists t \in ℝ^{+} \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v})$
14	11 12 13	mp2an	$⊢ \exists t \in ℝ^{+} \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v})$
15		simpr	$⊢ (φ \land t \in ℝ^{+}) \to t \in ℝ^{+}$
16		ioossre	$⊢ (0, 1) \subseteq ℝ$
17	16 8	sselid	$⊢ φ \to E \in ℝ$
18		eliooord	$⊢ E \in (0, 1) \to (0 < E \land E < 1)$
19	8 18	syl	$⊢ φ \to (0 < E \land E < 1)$
20	19	simpld	$⊢ φ \to 0 < E$
21	17 20	elrpd	$⊢ φ \to E \in ℝ^{+}$
22	21	adantr	$⊢ (φ \land t \in ℝ^{+}) \to E \in ℝ^{+}$
23		4nn	$⊢ 4 \in ℕ$
24		nnrp	$⊢ 4 \in ℕ \to 4 \in ℝ^{+}$
25	23 24	ax-mp	$⊢ 4 \in ℝ^{+}$
26		rpdivcl	$⊢ (E \in ℝ^{+} \land 4 \in ℝ^{+}) \to \frac{E}{4} \in ℝ^{+}$
27	22 25 26	sylancl	$⊢ (φ \land t \in ℝ^{+}) \to \frac{E}{4} \in ℝ^{+}$
28	15 27	rpdivcld	$⊢ (φ \land t \in ℝ^{+}) \to \frac{t}{\frac{E}{4}} \in ℝ^{+}$
29	28	rpred	$⊢ (φ \land t \in ℝ^{+}) \to \frac{t}{\frac{E}{4}} \in ℝ$
30	29	rpefcld	$⊢ (φ \land t \in ℝ^{+}) \to e^{\frac{t}{\frac{E}{4}}} \in ℝ^{+}$
31	9	adantr	$⊢ (φ \land t \in ℝ^{+}) \to Z \in ℝ^{+}$
32	30 31	rpaddcld	$⊢ (φ \land t \in ℝ^{+}) \to e^{\frac{t}{\frac{E}{4}}} + Z \in ℝ^{+}$
33	32	adantrr	$⊢ (φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \to e^{\frac{t}{\frac{E}{4}}} + Z \in ℝ^{+}$
34		breq2	$⊢ i = n \to (v < i \leftrightarrow v < n)$
35		breq1	$⊢ i = n \to (i \leq (\frac{k}{2}) v \leftrightarrow n \leq (\frac{k}{2}) v)$
36	34 35	anbi12d	$⊢ i = n \to ((v < i \land i \leq (\frac{k}{2}) v) \leftrightarrow (v < n \land n \leq (\frac{k}{2}) v))$
37		fveq2	$⊢ i = n \to R (i) = R (n)$
38		id	$⊢ i = n \to i = n$
39	37 38	oveq12d	$⊢ i = n \to \frac{R (i)}{i} = \frac{R (n)}{n}$
40	39	fveq2d	$⊢ i = n \to \|\frac{R (i)}{i}\| = \|\frac{R (n)}{n}\|$
41	40	breq1d	$⊢ i = n \to (\|\frac{R (i)}{i}\| \leq \frac{E}{2} \leftrightarrow \|\frac{R (n)}{n}\| \leq \frac{E}{2})$
42	36 41	anbi12d	$⊢ i = n \to (((v < i \land i \leq (\frac{k}{2}) v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}) \leftrightarrow ((v < n \land n \leq (\frac{k}{2}) v) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2}))$
43	42	cbvrexvw	$⊢ \exists i \in ℕ ((v < i \land i \leq (\frac{k}{2}) v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}) \leftrightarrow \exists n \in ℕ ((v < n \land n \leq (\frac{k}{2}) v) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})$
44		breq1	$⊢ v = y \to (v < n \leftrightarrow y < n)$
45		oveq2	$⊢ v = y \to (\frac{k}{2}) v = (\frac{k}{2}) y$
46	45	breq2d	$⊢ v = y \to (n \leq (\frac{k}{2}) v \leftrightarrow n \leq (\frac{k}{2}) y)$
47	44 46	anbi12d	$⊢ v = y \to ((v < n \land n \leq (\frac{k}{2}) v) \leftrightarrow (y < n \land n \leq (\frac{k}{2}) y))$
48	47	anbi1d	$⊢ v = y \to (((v < n \land n \leq (\frac{k}{2}) v) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2}) \leftrightarrow ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2}))$
49	48	rexbidv	$⊢ v = y \to (\exists n \in ℕ ((v < n \land n \leq (\frac{k}{2}) v) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2}) \leftrightarrow \exists n \in ℕ ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2}))$
50	43 49	bitrid	$⊢ v = y \to (\exists i \in ℕ ((v < i \land i \leq (\frac{k}{2}) v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}) \leftrightarrow \exists n \in ℕ ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2}))$
51		oveq1	$⊢ m = \frac{k}{2} \to m v = (\frac{k}{2}) v$
52	51	breq2d	$⊢ m = \frac{k}{2} \to (i \leq m v \leftrightarrow i \leq (\frac{k}{2}) v)$
53	52	anbi2d	$⊢ m = \frac{k}{2} \to ((v < i \land i \leq m v) \leftrightarrow (v < i \land i \leq (\frac{k}{2}) v))$
54	53	anbi1d	$⊢ m = \frac{k}{2} \to (((v < i \land i \leq m v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}) \leftrightarrow ((v < i \land i \leq (\frac{k}{2}) v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}))$
55	54	rexbidv	$⊢ m = \frac{k}{2} \to (\exists i \in ℕ ((v < i \land i \leq m v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}) \leftrightarrow \exists i \in ℕ ((v < i \land i \leq (\frac{k}{2}) v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}))$
56	55	ralbidv	$⊢ m = \frac{k}{2} \to (\forall v \in (Z, +∞) \exists i \in ℕ ((v < i \land i \leq m v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}) \leftrightarrow \forall v \in (Z, +∞) \exists i \in ℕ ((v < i \land i \leq (\frac{k}{2}) v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2}))$
57	10	ad2antrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to \forall m \in [K, +∞) \forall v \in (Z, +∞) \exists i \in ℕ ((v < i \land i \leq m v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2})$
58	5	adantr	$⊢ (φ \land t \in ℝ^{+}) \to B \in ℝ^{+}$
59	58	rpred	$⊢ (φ \land t \in ℝ^{+}) \to B \in ℝ$
60		remulcl	$⊢ (2 \in ℝ \land B \in ℝ) \to 2 B \in ℝ$
61	11 59 60	sylancr	$⊢ (φ \land t \in ℝ^{+}) \to 2 B \in ℝ$
62		2rp	$⊢ 2 \in ℝ^{+}$
63		relogcl	$⊢ 2 \in ℝ^{+} \to \log 2 \in ℝ$
64	62 63	ax-mp	$⊢ \log 2 \in ℝ$
65		readdcl	$⊢ (2 B \in ℝ \land \log 2 \in ℝ) \to 2 B + \log 2 \in ℝ$
66	61 64 65	sylancl	$⊢ (φ \land t \in ℝ^{+}) \to 2 B + \log 2 \in ℝ$
67	7 66	eqeltrid	$⊢ (φ \land t \in ℝ^{+}) \to C \in ℝ$
68	67 22	rerpdivcld	$⊢ (φ \land t \in ℝ^{+}) \to \frac{C}{E} \in ℝ$
69	68	reefcld	$⊢ (φ \land t \in ℝ^{+}) \to e^{\frac{C}{E}} \in ℝ$
70		elicopnf	$⊢ e^{\frac{C}{E}} \in ℝ \to (k \in [e^{\frac{C}{E}}, +∞) \leftrightarrow (k \in ℝ \land e^{\frac{C}{E}} \leq k))$
71	69 70	syl	$⊢ (φ \land t \in ℝ^{+}) \to (k \in [e^{\frac{C}{E}}, +∞) \leftrightarrow (k \in ℝ \land e^{\frac{C}{E}} \leq k))$
72	71	simprbda	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to k \in ℝ$
73	72	rehalfcld	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to \frac{k}{2} \in ℝ$
74	22	rphalfcld	$⊢ (φ \land t \in ℝ^{+}) \to \frac{E}{2} \in ℝ^{+}$
75	59 74	rerpdivcld	$⊢ (φ \land t \in ℝ^{+}) \to \frac{B}{\frac{E}{2}} \in ℝ$
76	75	reefcld	$⊢ (φ \land t \in ℝ^{+}) \to e^{\frac{B}{\frac{E}{2}}} \in ℝ$
77		remulcl	$⊢ (e^{\frac{B}{\frac{E}{2}}} \in ℝ \land 2 \in ℝ) \to e^{\frac{B}{\frac{E}{2}}} \cdot 2 \in ℝ$
78	76 11 77	sylancl	$⊢ (φ \land t \in ℝ^{+}) \to e^{\frac{B}{\frac{E}{2}}} \cdot 2 \in ℝ$
79	78	adantr	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to e^{\frac{B}{\frac{E}{2}}} \cdot 2 \in ℝ$
80	69	adantr	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to e^{\frac{C}{E}} \in ℝ$
81	75	recnd	$⊢ (φ \land t \in ℝ^{+}) \to \frac{B}{\frac{E}{2}} \in ℂ$
82	64	recni	$⊢ \log 2 \in ℂ$
83		efadd	$⊢ (\frac{B}{\frac{E}{2}} \in ℂ \land \log 2 \in ℂ) \to e^{(\frac{B}{\frac{E}{2}}) + \log 2} = e^{\frac{B}{\frac{E}{2}}} e^{\log 2}$
84	81 82 83	sylancl	$⊢ (φ \land t \in ℝ^{+}) \to e^{(\frac{B}{\frac{E}{2}}) + \log 2} = e^{\frac{B}{\frac{E}{2}}} e^{\log 2}$
85		reeflog	$⊢ 2 \in ℝ^{+} \to e^{\log 2} = 2$
86	62 85	ax-mp	$⊢ e^{\log 2} = 2$
87	86	oveq2i	$⊢ e^{\frac{B}{\frac{E}{2}}} e^{\log 2} = e^{\frac{B}{\frac{E}{2}}} \cdot 2$
88	84 87	eqtrdi	$⊢ (φ \land t \in ℝ^{+}) \to e^{(\frac{B}{\frac{E}{2}}) + \log 2} = e^{\frac{B}{\frac{E}{2}}} \cdot 2$
89	64	a1i	$⊢ (φ \land t \in ℝ^{+}) \to \log 2 \in ℝ$
90		rerpdivcl	$⊢ (\log 2 \in ℝ \land E \in ℝ^{+}) \to \frac{\log 2}{E} \in ℝ$
91	64 22 90	sylancr	$⊢ (φ \land t \in ℝ^{+}) \to \frac{\log 2}{E} \in ℝ$
92	82	div1i	$⊢ \frac{\log 2}{1} = \log 2$
93	19	simprd	$⊢ φ \to E < 1$
94	93	adantr	$⊢ (φ \land t \in ℝ^{+}) \to E < 1$
95	17	adantr	$⊢ (φ \land t \in ℝ^{+}) \to E \in ℝ$
96		1re	$⊢ 1 \in ℝ$
97		ltle	$⊢ (E \in ℝ \land 1 \in ℝ) \to (E < 1 \to E \leq 1)$
98	95 96 97	sylancl	$⊢ (φ \land t \in ℝ^{+}) \to (E < 1 \to E \leq 1)$
99	94 98	mpd	$⊢ (φ \land t \in ℝ^{+}) \to E \leq 1$
100	22	rpregt0d	$⊢ (φ \land t \in ℝ^{+}) \to (E \in ℝ \land 0 < E)$
101		1rp	$⊢ 1 \in ℝ^{+}$
102		rpregt0	$⊢ 1 \in ℝ^{+} \to (1 \in ℝ \land 0 < 1)$
103	101 102	mp1i	$⊢ (φ \land t \in ℝ^{+}) \to (1 \in ℝ \land 0 < 1)$
104		1lt2	$⊢ 1 < 2$
105		rplogcl	$⊢ (2 \in ℝ \land 1 < 2) \to \log 2 \in ℝ^{+}$
106	11 104 105	mp2an	$⊢ \log 2 \in ℝ^{+}$
107		rpregt0	$⊢ \log 2 \in ℝ^{+} \to (\log 2 \in ℝ \land 0 < \log 2)$
108	106 107	mp1i	$⊢ (φ \land t \in ℝ^{+}) \to (\log 2 \in ℝ \land 0 < \log 2)$
109		lediv2	$⊢ ((E \in ℝ \land 0 < E) \land (1 \in ℝ \land 0 < 1) \land (\log 2 \in ℝ \land 0 < \log 2)) \to (E \leq 1 \leftrightarrow \frac{\log 2}{1} \leq \frac{\log 2}{E})$
110	100 103 108 109	syl3anc	$⊢ (φ \land t \in ℝ^{+}) \to (E \leq 1 \leftrightarrow \frac{\log 2}{1} \leq \frac{\log 2}{E})$
111	99 110	mpbid	$⊢ (φ \land t \in ℝ^{+}) \to \frac{\log 2}{1} \leq \frac{\log 2}{E}$
112	92 111	eqbrtrrid	$⊢ (φ \land t \in ℝ^{+}) \to \log 2 \leq \frac{\log 2}{E}$
113	89 91 75 112	leadd2dd	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{B}{\frac{E}{2}}) + \log 2 \leq (\frac{B}{\frac{E}{2}}) + (\frac{\log 2}{E})$
114	7	oveq1i	$⊢ \frac{C}{E} = \frac{2 B + \log 2}{E}$
115	61	recnd	$⊢ (φ \land t \in ℝ^{+}) \to 2 B \in ℂ$
116	82	a1i	$⊢ (φ \land t \in ℝ^{+}) \to \log 2 \in ℂ$
117		rpcnne0	$⊢ E \in ℝ^{+} \to (E \in ℂ \land E \neq 0)$
118	22 117	syl	$⊢ (φ \land t \in ℝ^{+}) \to (E \in ℂ \land E \neq 0)$
119		divdir	$⊢ (2 B \in ℂ \land \log 2 \in ℂ \land (E \in ℂ \land E \neq 0)) \to \frac{2 B + \log 2}{E} = (\frac{2 B}{E}) + (\frac{\log 2}{E})$
120	115 116 118 119	syl3anc	$⊢ (φ \land t \in ℝ^{+}) \to \frac{2 B + \log 2}{E} = (\frac{2 B}{E}) + (\frac{\log 2}{E})$
121	114 120	eqtrid	$⊢ (φ \land t \in ℝ^{+}) \to \frac{C}{E} = (\frac{2 B}{E}) + (\frac{\log 2}{E})$
122	11	recni	$⊢ 2 \in ℂ$
123	59	recnd	$⊢ (φ \land t \in ℝ^{+}) \to B \in ℂ$
124		mulcom	$⊢ (2 \in ℂ \land B \in ℂ) \to 2 B = B \cdot 2$
125	122 123 124	sylancr	$⊢ (φ \land t \in ℝ^{+}) \to 2 B = B \cdot 2$
126	125	oveq1d	$⊢ (φ \land t \in ℝ^{+}) \to \frac{2 B}{E} = \frac{B \cdot 2}{E}$
127		rpcnne0	$⊢ 2 \in ℝ^{+} \to (2 \in ℂ \land 2 \neq 0)$
128	62 127	mp1i	$⊢ (φ \land t \in ℝ^{+}) \to (2 \in ℂ \land 2 \neq 0)$
129		divdiv2	$⊢ (B \in ℂ \land (E \in ℂ \land E \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{B}{\frac{E}{2}} = \frac{B \cdot 2}{E}$
130	123 118 128 129	syl3anc	$⊢ (φ \land t \in ℝ^{+}) \to \frac{B}{\frac{E}{2}} = \frac{B \cdot 2}{E}$
131	126 130	eqtr4d	$⊢ (φ \land t \in ℝ^{+}) \to \frac{2 B}{E} = \frac{B}{\frac{E}{2}}$
132	131	oveq1d	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{2 B}{E}) + (\frac{\log 2}{E}) = (\frac{B}{\frac{E}{2}}) + (\frac{\log 2}{E})$
133	121 132	eqtrd	$⊢ (φ \land t \in ℝ^{+}) \to \frac{C}{E} = (\frac{B}{\frac{E}{2}}) + (\frac{\log 2}{E})$
134	113 133	breqtrrd	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{B}{\frac{E}{2}}) + \log 2 \leq \frac{C}{E}$
135		readdcl	$⊢ (\frac{B}{\frac{E}{2}} \in ℝ \land \log 2 \in ℝ) \to (\frac{B}{\frac{E}{2}}) + \log 2 \in ℝ$
136	75 64 135	sylancl	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{B}{\frac{E}{2}}) + \log 2 \in ℝ$
137		efle	$⊢ ((\frac{B}{\frac{E}{2}}) + \log 2 \in ℝ \land \frac{C}{E} \in ℝ) \to ((\frac{B}{\frac{E}{2}}) + \log 2 \leq \frac{C}{E} \leftrightarrow e^{(\frac{B}{\frac{E}{2}}) + \log 2} \leq e^{\frac{C}{E}})$
138	136 68 137	syl2anc	$⊢ (φ \land t \in ℝ^{+}) \to ((\frac{B}{\frac{E}{2}}) + \log 2 \leq \frac{C}{E} \leftrightarrow e^{(\frac{B}{\frac{E}{2}}) + \log 2} \leq e^{\frac{C}{E}})$
139	134 138	mpbid	$⊢ (φ \land t \in ℝ^{+}) \to e^{(\frac{B}{\frac{E}{2}}) + \log 2} \leq e^{\frac{C}{E}}$
140	88 139	eqbrtrrd	$⊢ (φ \land t \in ℝ^{+}) \to e^{\frac{B}{\frac{E}{2}}} \cdot 2 \leq e^{\frac{C}{E}}$
141	140	adantr	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to e^{\frac{B}{\frac{E}{2}}} \cdot 2 \leq e^{\frac{C}{E}}$
142	71	simplbda	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to e^{\frac{C}{E}} \leq k$
143	79 80 72 141 142	letrd	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to e^{\frac{B}{\frac{E}{2}}} \cdot 2 \leq k$
144	76	adantr	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to e^{\frac{B}{\frac{E}{2}}} \in ℝ$
145		rpregt0	$⊢ 2 \in ℝ^{+} \to (2 \in ℝ \land 0 < 2)$
146	62 145	mp1i	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to (2 \in ℝ \land 0 < 2)$
147		lemuldiv	$⊢ (e^{\frac{B}{\frac{E}{2}}} \in ℝ \land k \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (e^{\frac{B}{\frac{E}{2}}} \cdot 2 \leq k \leftrightarrow e^{\frac{B}{\frac{E}{2}}} \leq \frac{k}{2})$
148	144 72 146 147	syl3anc	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to (e^{\frac{B}{\frac{E}{2}}} \cdot 2 \leq k \leftrightarrow e^{\frac{B}{\frac{E}{2}}} \leq \frac{k}{2})$
149	143 148	mpbid	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to e^{\frac{B}{\frac{E}{2}}} \leq \frac{k}{2}$
150	6 149	eqbrtrid	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to K \leq \frac{k}{2}$
151	6 144	eqeltrid	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to K \in ℝ$
152		elicopnf	$⊢ K \in ℝ \to (\frac{k}{2} \in [K, +∞) \leftrightarrow (\frac{k}{2} \in ℝ \land K \leq \frac{k}{2}))$
153	151 152	syl	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to (\frac{k}{2} \in [K, +∞) \leftrightarrow (\frac{k}{2} \in ℝ \land K \leq \frac{k}{2}))$
154	73 150 153	mpbir2and	$⊢ ((φ \land t \in ℝ^{+}) \land k \in [e^{\frac{C}{E}}, +∞)) \to \frac{k}{2} \in [K, +∞)$
155	154	adantrr	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to \frac{k}{2} \in [K, +∞)$
156	155	adantlrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to \frac{k}{2} \in [K, +∞)$
157	56 57 156	rspcdva	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to \forall v \in (Z, +∞) \exists i \in ℕ ((v < i \land i \leq (\frac{k}{2}) v) \land \|\frac{R (i)}{i}\| \leq \frac{E}{2})$
158		elioore	$⊢ y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞) \to y \in ℝ$
159	158	ad2antll	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to y \in ℝ$
160	31	rpred	$⊢ (φ \land t \in ℝ^{+}) \to Z \in ℝ$
161	160	adantr	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to Z \in ℝ$
162	29	reefcld	$⊢ (φ \land t \in ℝ^{+}) \to e^{\frac{t}{\frac{E}{4}}} \in ℝ$
163	162 160	readdcld	$⊢ (φ \land t \in ℝ^{+}) \to e^{\frac{t}{\frac{E}{4}}} + Z \in ℝ$
164	163	adantr	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to e^{\frac{t}{\frac{E}{4}}} + Z \in ℝ$
165	160 30	ltaddrp2d	$⊢ (φ \land t \in ℝ^{+}) \to Z < e^{\frac{t}{\frac{E}{4}}} + Z$
166	165	adantr	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to Z < e^{\frac{t}{\frac{E}{4}}} + Z$
167		eliooord	$⊢ y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞) \to (e^{\frac{t}{\frac{E}{4}}} + Z < y \land y < +∞)$
168	167	simpld	$⊢ y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞) \to e^{\frac{t}{\frac{E}{4}}} + Z < y$
169	168	ad2antll	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to e^{\frac{t}{\frac{E}{4}}} + Z < y$
170	161 164 159 166 169	lttrd	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to Z < y$
171	161	rexrd	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to Z \in ℝ^{*}$
172		elioopnf	$⊢ Z \in ℝ^{*} \to (y \in (Z, +∞) \leftrightarrow (y \in ℝ \land Z < y))$
173	171 172	syl	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to (y \in (Z, +∞) \leftrightarrow (y \in ℝ \land Z < y))$
174	159 170 173	mpbir2and	$⊢ ((φ \land t \in ℝ^{+}) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to y \in (Z, +∞)$
175	174	adantlrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to y \in (Z, +∞)$
176	50 157 175	rspcdva	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to \exists n \in ℕ ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})$
177	2	ad2antrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to A \in ℝ^{+}$
178		fveq2	$⊢ x = v \to R (x) = R (v)$
179		id	$⊢ x = v \to x = v$
180	178 179	oveq12d	$⊢ x = v \to \frac{R (x)}{x} = \frac{R (v)}{v}$
181	180	fveq2d	$⊢ x = v \to \|\frac{R (x)}{x}\| = \|\frac{R (v)}{v}\|$
182	181	breq1d	$⊢ x = v \to (\|\frac{R (x)}{x}\| \leq A \leftrightarrow \|\frac{R (v)}{v}\| \leq A)$
183	182	cbvralvw	$⊢ \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A \leftrightarrow \forall v \in ℝ^{+} \|\frac{R (v)}{v}\| \leq A$
184	4 183	sylib	$⊢ φ \to \forall v \in ℝ^{+} \|\frac{R (v)}{v}\| \leq A$
185	184	ad2antrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to \forall v \in ℝ^{+} \|\frac{R (v)}{v}\| \leq A$
186	5	ad2antrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to B \in ℝ^{+}$
187	8	ad2antrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to E \in (0, 1)$
188	9	ad2antrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to Z \in ℝ^{+}$
189		simprrl	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to n \in ℕ$
190		simplrl	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to t \in ℝ^{+}$
191		simplrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v})$
192		eqid	$⊢ e^{\frac{t}{\frac{E}{4}}} + Z = e^{\frac{t}{\frac{E}{4}}} + Z$
193		simprll	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to k \in [e^{\frac{C}{E}}, +∞)$
194		simprlr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)$
195		simprrr	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})$
196	1 177 3 185 186 6 7 187 188 189 190 191 192 193 194 195	pntibndlem2	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land ((k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2})))) \to \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
197	196	anassrs	$⊢ (((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \land (n \in ℕ \land ((y < n \land n \leq (\frac{k}{2}) y) \land \|\frac{R (n)}{n}\| \leq \frac{E}{2}))) \to \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
198	176 197	rexlimddv	$⊢ ((φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \land (k \in [e^{\frac{C}{E}}, +∞) \land y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞))) \to \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
199	198	ralrimivva	$⊢ (φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \to \forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
200		oveq1	$⊢ x = e^{\frac{t}{\frac{E}{4}}} + Z \to (x, +∞) = (e^{\frac{t}{\frac{E}{4}}} + Z, +∞)$
201	200	raleqdv	$⊢ x = e^{\frac{t}{\frac{E}{4}}} + Z \to (\forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E) \leftrightarrow \forall y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E))$
202	201	ralbidv	$⊢ x = e^{\frac{t}{\frac{E}{4}}} + Z \to (\forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E) \leftrightarrow \forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E))$
203	202	rspcev	$⊢ (e^{\frac{t}{\frac{E}{4}}} + Z \in ℝ^{+} \land \forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (e^{\frac{t}{\frac{E}{4}}} + Z, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)) \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
204	33 199 203	syl2anc	$⊢ (φ \land (t \in ℝ^{+} \land \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}))) \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
205	204	rexlimdvaa	$⊢ φ \to (\exists t \in ℝ^{+} \forall v \in (1, +∞) \forall w \in [v, 2 v] ψ (w) - ψ (v) \leq 2 (w - v) + t (\frac{v}{\log v}) \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E))$
206	14 205	mpi	$⊢ φ \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{C}{E}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$

Metamath Proof Explorer

Theorem pntibndlem3

Proof