pntibndlem2

Description: Lemma for pntibnd . The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016)

	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 ℝ^{+}$
	pntibndlem2.10	$⊢ φ \to N \in ℕ$
	pntibndlem2.5	$⊢ φ \to T \in ℝ^{+}$
	pntibndlem2.6	$⊢ φ \to \forall x \in (1, +∞) \forall y \in [x, 2 x] ψ (y) - ψ (x) \leq 2 (y - x) + T (\frac{x}{\log x})$
	pntibndlem2.7	$⊢ X = e^{\frac{T}{\frac{E}{4}}} + Z$
	pntibndlem2.8	$⊢ φ \to M \in [e^{\frac{C}{E}}, +∞)$
	pntibndlem2.9	$⊢ φ \to Y \in (X, +∞)$
	pntibndlem2.11	$⊢ φ \to ((Y < N \land N \leq (\frac{M}{2}) Y) \land \|\frac{R (N)}{N}\| \leq \frac{E}{2})$
Assertion	pntibndlem2	$⊢ φ \to \exists z \in ℝ^{+} ((Y < z \land (1 + L E) z < M 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		pntibndlem2.10	$⊢ φ \to N \in ℕ$
11		pntibndlem2.5	$⊢ φ \to T \in ℝ^{+}$
12		pntibndlem2.6	$⊢ φ \to \forall x \in (1, +∞) \forall y \in [x, 2 x] ψ (y) - ψ (x) \leq 2 (y - x) + T (\frac{x}{\log x})$
13		pntibndlem2.7	$⊢ X = e^{\frac{T}{\frac{E}{4}}} + Z$
14		pntibndlem2.8	$⊢ φ \to M \in [e^{\frac{C}{E}}, +∞)$
15		pntibndlem2.9	$⊢ φ \to Y \in (X, +∞)$
16		pntibndlem2.11	$⊢ φ \to ((Y < N \land N \leq (\frac{M}{2}) Y) \land \|\frac{R (N)}{N}\| \leq \frac{E}{2})$
17	10	nnrpd	$⊢ φ \to N \in ℝ^{+}$
18	16	simpld	$⊢ φ \to (Y < N \land N \leq (\frac{M}{2}) Y)$
19	18	simpld	$⊢ φ \to Y < N$
20		1red	$⊢ φ \to 1 \in ℝ$
21		ioossre	$⊢ (0, 1) \subseteq ℝ$
22	1 2 3	pntibndlem1	$⊢ φ \to L \in (0, 1)$
23	21 22	sselid	$⊢ φ \to L \in ℝ$
24	21 8	sselid	$⊢ φ \to E \in ℝ$
25	23 24	remulcld	$⊢ φ \to L E \in ℝ$
26	20 25	readdcld	$⊢ φ \to 1 + L E \in ℝ$
27	10	nnred	$⊢ φ \to N \in ℝ$
28	26 27	remulcld	$⊢ φ \to (1 + L E) \cdot N \in ℝ$
29		2re	$⊢ 2 \in ℝ$
30		remulcl	$⊢ (2 \in ℝ \land N \in ℝ) \to 2 \cdot N \in ℝ$
31	29 27 30	sylancr	$⊢ φ \to 2 \cdot N \in ℝ$
32	5	rpred	$⊢ φ \to B \in ℝ$
33		remulcl	$⊢ (2 \in ℝ \land B \in ℝ) \to 2 B \in ℝ$
34	29 32 33	sylancr	$⊢ φ \to 2 B \in ℝ$
35		2rp	$⊢ 2 \in ℝ^{+}$
36	35	a1i	$⊢ φ \to 2 \in ℝ^{+}$
37	36	relogcld	$⊢ φ \to \log 2 \in ℝ$
38	34 37	readdcld	$⊢ φ \to 2 B + \log 2 \in ℝ$
39	7 38	eqeltrid	$⊢ φ \to C \in ℝ$
40		eliooord	$⊢ E \in (0, 1) \to (0 < E \land E < 1)$
41	8 40	syl	$⊢ φ \to (0 < E \land E < 1)$
42	41	simpld	$⊢ φ \to 0 < E$
43	24 42	elrpd	$⊢ φ \to E \in ℝ^{+}$
44	39 43	rerpdivcld	$⊢ φ \to \frac{C}{E} \in ℝ$
45	44	reefcld	$⊢ φ \to e^{\frac{C}{E}} \in ℝ$
46		pnfxr	$⊢ +∞ \in ℝ^{*}$
47		icossre	$⊢ (e^{\frac{C}{E}} \in ℝ \land +∞ \in ℝ^{*}) \to [e^{\frac{C}{E}}, +∞) \subseteq ℝ$
48	45 46 47	sylancl	$⊢ φ \to [e^{\frac{C}{E}}, +∞) \subseteq ℝ$
49	48 14	sseldd	$⊢ φ \to M \in ℝ$
50		ioossre	$⊢ (X, +∞) \subseteq ℝ$
51	50 15	sselid	$⊢ φ \to Y \in ℝ$
52	49 51	remulcld	$⊢ φ \to M Y \in ℝ$
53	29	a1i	$⊢ φ \to 2 \in ℝ$
54		eliooord	$⊢ L \in (0, 1) \to (0 < L \land L < 1)$
55	22 54	syl	$⊢ φ \to (0 < L \land L < 1)$
56	55	simpld	$⊢ φ \to 0 < L$
57	23 56	elrpd	$⊢ φ \to L \in ℝ^{+}$
58	57	rpge0d	$⊢ φ \to 0 \leq L$
59	55	simprd	$⊢ φ \to L < 1$
60	43	rpge0d	$⊢ φ \to 0 \leq E$
61	41	simprd	$⊢ φ \to E < 1$
62	23 20 24 20 58 59 60 61	ltmul12ad	$⊢ φ \to L E < 1 \cdot 1$
63		1t1e1	$⊢ 1 \cdot 1 = 1$
64	62 63	breqtrdi	$⊢ φ \to L E < 1$
65	25 20 20 64	ltadd2dd	$⊢ φ \to 1 + L E < 1 + 1$
66		df-2	$⊢ 2 = 1 + 1$
67	65 66	breqtrrdi	$⊢ φ \to 1 + L E < 2$
68	26 53 17 67	ltmul1dd	$⊢ φ \to (1 + L E) \cdot N < 2 \cdot N$
69	18	simprd	$⊢ φ \to N \leq (\frac{M}{2}) Y$
70	49	recnd	$⊢ φ \to M \in ℂ$
71	51	recnd	$⊢ φ \to Y \in ℂ$
72		rpcnne0	$⊢ 2 \in ℝ^{+} \to (2 \in ℂ \land 2 \neq 0)$
73	35 72	mp1i	$⊢ φ \to (2 \in ℂ \land 2 \neq 0)$
74		div23	$⊢ (M \in ℂ \land Y \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{M Y}{2} = (\frac{M}{2}) Y$
75	70 71 73 74	syl3anc	$⊢ φ \to \frac{M Y}{2} = (\frac{M}{2}) Y$
76	69 75	breqtrrd	$⊢ φ \to N \leq \frac{M Y}{2}$
77	27 52 36	lemuldiv2d	$⊢ φ \to (2 \cdot N \leq M Y \leftrightarrow N \leq \frac{M Y}{2})$
78	76 77	mpbird	$⊢ φ \to 2 \cdot N \leq M Y$
79	28 31 52 68 78	ltletrd	$⊢ φ \to (1 + L E) \cdot N < M Y$
80	1 2 3 4 5 6 7 8 2 10	pntibndlem2a	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (u \in ℝ \land N \leq u \land u \leq (1 + L E) \cdot N)$
81	80	simp1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to u \in ℝ$
82	17	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to N \in ℝ^{+}$
83	80	simp2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to N \leq u$
84	81 82 83	rpgecld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to u \in ℝ^{+}$
85	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
86	85	ffvelcdmi	$⊢ u \in ℝ^{+} \to R (u) \in ℝ$
87	84 86	syl	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (u) \in ℝ$
88	87 84	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (u)}{u} \in ℝ$
89	88	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (u)}{u} \in ℂ$
90	89	abscld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| \in ℝ$
91	85	ffvelcdmi	$⊢ N \in ℝ^{+} \to R (N) \in ℝ$
92	17 91	syl	$⊢ φ \to R (N) \in ℝ$
93	92 10	nndivred	$⊢ φ \to \frac{R (N)}{N} \in ℝ$
94	93	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (N)}{N} \in ℝ$
95	94	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (N)}{N} \in ℂ$
96	89 95	subcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{R (u)}{u}) - (\frac{R (N)}{N}) \in ℂ$
97	96	abscld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| \in ℝ$
98	95	abscld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (N)}{N}\| \in ℝ$
99	97 98	readdcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| + \|\frac{R (N)}{N}\| \in ℝ$
100	24	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to E \in ℝ$
101	89 95	abs2difd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| - \|\frac{R (N)}{N}\| \leq \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\|$
102	90 98 97	lesubaddd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\|\frac{R (u)}{u}\| - \|\frac{R (N)}{N}\| \leq \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| \leftrightarrow \|\frac{R (u)}{u}\| \leq \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| + \|\frac{R (N)}{N}\|)$
103	101 102	mpbid	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| \leq \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| + \|\frac{R (N)}{N}\|$
104	100	rehalfcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{E}{2} \in ℝ$
105	27	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to N \in ℝ$
106	81 105	resubcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to u - N \in ℝ$
107	106 82	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u - N}{N} \in ℝ$
108		3re	$⊢ 3 \in ℝ$
109	108	a1i	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 3 \in ℝ$
110	90 109	readdcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| + 3 \in ℝ$
111	107 110	remulcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) \in ℝ$
112	11	rpred	$⊢ φ \to T \in ℝ$
113	112	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to T \in ℝ$
114		1red	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 1 \in ℝ$
115		4nn	$⊢ 4 \in ℕ$
116		nnrp	$⊢ 4 \in ℕ \to 4 \in ℝ^{+}$
117	115 116	mp1i	$⊢ φ \to 4 \in ℝ^{+}$
118	43 117	rpdivcld	$⊢ φ \to \frac{E}{4} \in ℝ^{+}$
119	11 118	rpdivcld	$⊢ φ \to \frac{T}{\frac{E}{4}} \in ℝ^{+}$
120	119	rpred	$⊢ φ \to \frac{T}{\frac{E}{4}} \in ℝ$
121	120	reefcld	$⊢ φ \to e^{\frac{T}{\frac{E}{4}}} \in ℝ$
122	121	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to e^{\frac{T}{\frac{E}{4}}} \in ℝ$
123		efgt1	$⊢ \frac{T}{\frac{E}{4}} \in ℝ^{+} \to 1 < e^{\frac{T}{\frac{E}{4}}}$
124	119 123	syl	$⊢ φ \to 1 < e^{\frac{T}{\frac{E}{4}}}$
125	124	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 1 < e^{\frac{T}{\frac{E}{4}}}$
126	9	rpred	$⊢ φ \to Z \in ℝ$
127	121 126	readdcld	$⊢ φ \to e^{\frac{T}{\frac{E}{4}}} + Z \in ℝ$
128	13 127	eqeltrid	$⊢ φ \to X \in ℝ$
129	121 9	ltaddrpd	$⊢ φ \to e^{\frac{T}{\frac{E}{4}}} < e^{\frac{T}{\frac{E}{4}}} + Z$
130	129 13	breqtrrdi	$⊢ φ \to e^{\frac{T}{\frac{E}{4}}} < X$
131		eliooord	$⊢ Y \in (X, +∞) \to (X < Y \land Y < +∞)$
132	15 131	syl	$⊢ φ \to (X < Y \land Y < +∞)$
133	132	simpld	$⊢ φ \to X < Y$
134	121 128 51 130 133	lttrd	$⊢ φ \to e^{\frac{T}{\frac{E}{4}}} < Y$
135	121 51 27 134 19	lttrd	$⊢ φ \to e^{\frac{T}{\frac{E}{4}}} < N$
136	135	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to e^{\frac{T}{\frac{E}{4}}} < N$
137	114 122 105 125 136	lttrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 1 < N$
138	105 137	rplogcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \log N \in ℝ^{+}$
139	113 138	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\log N} \in ℝ$
140	111 139	readdcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) + (\frac{T}{\log N}) \in ℝ$
141		peano2re	$⊢ \|\frac{R (u)}{u}\| \in ℝ \to \|\frac{R (u)}{u}\| + 1 \in ℝ$
142	90 141	syl	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| + 1 \in ℝ$
143	107 142	remulcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) \in ℝ$
144		chpcl	$⊢ u \in ℝ \to ψ (u) \in ℝ$
145	81 144	syl	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (u) \in ℝ$
146		chpcl	$⊢ N \in ℝ \to ψ (N) \in ℝ$
147	105 146	syl	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (N) \in ℝ$
148	145 147	resubcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (u) - ψ (N) \in ℝ$
149	148 82	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{ψ (u) - ψ (N)}{N} \in ℝ$
150	143 149	readdcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{ψ (u) - ψ (N)}{N}) \in ℝ$
151	107 90	remulcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \|\frac{R (u)}{u}\| \in ℝ$
152	92	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (N) \in ℝ$
153	87 152	resubcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (u) - R (N) \in ℝ$
154	153	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (u) - R (N) \in ℂ$
155	154	abscld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|R (u) - R (N)\| \in ℝ$
156	155 82	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{\|R (u) - R (N)\|}{N} \in ℝ$
157	151 156	readdcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{\|R (u) - R (N)\|}{N}) \in ℝ$
158	107 88	remulcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\frac{R (u)}{u}) \in ℝ$
159	158	renegcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to - (\frac{u - N}{N}) (\frac{R (u)}{u}) \in ℝ$
160	159	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to - (\frac{u - N}{N}) (\frac{R (u)}{u}) \in ℂ$
161	153 82	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (u) - R (N)}{N} \in ℝ$
162	161	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (u) - R (N)}{N} \in ℂ$
163	160 162	abstrid	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|- (\frac{u - N}{N}) (\frac{R (u)}{u}) + (\frac{R (u) - R (N)}{N})\| \leq \|- (\frac{u - N}{N}) (\frac{R (u)}{u})\| + \|\frac{R (u) - R (N)}{N}\|$
164	81	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to u \in ℂ$
165	105	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to N \in ℂ$
166	82	rpne0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to N \neq 0$
167	164 165 165 166	divsubdird	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u - N}{N} = (\frac{u}{N}) - (\frac{N}{N})$
168	165 166	dividd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{N}{N} = 1$
169	168	oveq2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u}{N}) - (\frac{N}{N}) = (\frac{u}{N}) - 1$
170	167 169	eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u - N}{N} = (\frac{u}{N}) - 1$
171	170	oveq1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\frac{R (u)}{u}) = ((\frac{u}{N}) - 1) (\frac{R (u)}{u})$
172	81 82	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u}{N} \in ℝ$
173	172	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u}{N} \in ℂ$
174		1cnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 1 \in ℂ$
175	173 174 89	subdird	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ((\frac{u}{N}) - 1) (\frac{R (u)}{u}) = (\frac{u}{N}) (\frac{R (u)}{u}) - 1 (\frac{R (u)}{u})$
176	84	rpcnne0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (u \in ℂ \land u \neq 0)$
177	82	rpcnne0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (N \in ℂ \land N \neq 0)$
178	87	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (u) \in ℂ$
179		dmdcan	$⊢ ((u \in ℂ \land u \neq 0) \land (N \in ℂ \land N \neq 0) \land R (u) \in ℂ) \to (\frac{u}{N}) (\frac{R (u)}{u}) = \frac{R (u)}{N}$
180	176 177 178 179	syl3anc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u}{N}) (\frac{R (u)}{u}) = \frac{R (u)}{N}$
181	89	mullidd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 1 (\frac{R (u)}{u}) = \frac{R (u)}{u}$
182	180 181	oveq12d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u}{N}) (\frac{R (u)}{u}) - 1 (\frac{R (u)}{u}) = (\frac{R (u)}{N}) - (\frac{R (u)}{u})$
183	171 175 182	3eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\frac{R (u)}{u}) = (\frac{R (u)}{N}) - (\frac{R (u)}{u})$
184	183	negeqd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to - (\frac{u - N}{N}) (\frac{R (u)}{u}) = - ((\frac{R (u)}{N}) - (\frac{R (u)}{u}))$
185	87 82	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (u)}{N} \in ℝ$
186	185	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (u)}{N} \in ℂ$
187	186 89	negsubdi2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to - ((\frac{R (u)}{N}) - (\frac{R (u)}{u})) = (\frac{R (u)}{u}) - (\frac{R (u)}{N})$
188	184 187	eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to - (\frac{u - N}{N}) (\frac{R (u)}{u}) = (\frac{R (u)}{u}) - (\frac{R (u)}{N})$
189	152	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (N) \in ℂ$
190	178 189 165 166	divsubdird	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{R (u) - R (N)}{N} = (\frac{R (u)}{N}) - (\frac{R (N)}{N})$
191	188 190	oveq12d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to - (\frac{u - N}{N}) (\frac{R (u)}{u}) + (\frac{R (u) - R (N)}{N}) = ((\frac{R (u)}{u}) - (\frac{R (u)}{N})) + (\frac{R (u)}{N}) - (\frac{R (N)}{N})$
192	89 186 95	npncand	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ((\frac{R (u)}{u}) - (\frac{R (u)}{N})) + (\frac{R (u)}{N}) - (\frac{R (N)}{N}) = (\frac{R (u)}{u}) - (\frac{R (N)}{N})$
193	191 192	eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to - (\frac{u - N}{N}) (\frac{R (u)}{u}) + (\frac{R (u) - R (N)}{N}) = (\frac{R (u)}{u}) - (\frac{R (N)}{N})$
194	193	fveq2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|- (\frac{u - N}{N}) (\frac{R (u)}{u}) + (\frac{R (u) - R (N)}{N})\| = \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\|$
195	158	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\frac{R (u)}{u}) \in ℂ$
196	195	absnegd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|- (\frac{u - N}{N}) (\frac{R (u)}{u})\| = \|(\frac{u - N}{N}) (\frac{R (u)}{u})\|$
197	107	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u - N}{N} \in ℂ$
198	197 89	absmuld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{u - N}{N}) (\frac{R (u)}{u})\| = \|\frac{u - N}{N}\| \|\frac{R (u)}{u}\|$
199	81 105	subge0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (0 \leq u - N \leftrightarrow N \leq u)$
200	83 199	mpbird	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 0 \leq u - N$
201	106 82 200	divge0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 0 \leq \frac{u - N}{N}$
202	107 201	absidd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{u - N}{N}\| = \frac{u - N}{N}$
203	202	oveq1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{u - N}{N}\| \|\frac{R (u)}{u}\| = (\frac{u - N}{N}) \|\frac{R (u)}{u}\|$
204	196 198 203	3eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|- (\frac{u - N}{N}) (\frac{R (u)}{u})\| = (\frac{u - N}{N}) \|\frac{R (u)}{u}\|$
205	154 165 166	absdivd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u) - R (N)}{N}\| = \frac{\|R (u) - R (N)\|}{\|N\|}$
206	82	rprege0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (N \in ℝ \land 0 \leq N)$
207		absid	$⊢ (N \in ℝ \land 0 \leq N) \to \|N\| = N$
208	206 207	syl	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|N\| = N$
209	208	oveq2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{\|R (u) - R (N)\|}{\|N\|} = \frac{\|R (u) - R (N)\|}{N}$
210	205 209	eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u) - R (N)}{N}\| = \frac{\|R (u) - R (N)\|}{N}$
211	204 210	oveq12d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|- (\frac{u - N}{N}) (\frac{R (u)}{u})\| + \|\frac{R (u) - R (N)}{N}\| = (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{\|R (u) - R (N)\|}{N})$
212	163 194 211	3brtr3d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| \leq (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{\|R (u) - R (N)\|}{N})$
213	106 148	readdcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (u - N) + ψ (u) - ψ (N) \in ℝ$
214	213 82	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{(u - N) + ψ (u) - ψ (N)}{N} \in ℝ$
215	148	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (u) - ψ (N) \in ℂ$
216	165 164	subcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to N - u \in ℂ$
217	215 216	abstrid	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(ψ (u) - ψ (N)) + N - u\| \leq \|ψ (u) - ψ (N)\| + \|N - u\|$
218	1	pntrval	$⊢ u \in ℝ^{+} \to R (u) = ψ (u) - u$
219	84 218	syl	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (u) = ψ (u) - u$
220	1	pntrval	$⊢ N \in ℝ^{+} \to R (N) = ψ (N) - N$
221	82 220	syl	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (N) = ψ (N) - N$
222	219 221	oveq12d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to R (u) - R (N) = ψ (u) - u - (ψ (N) - N)$
223	145	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (u) \in ℂ$
224	147	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (N) \in ℂ$
225		subadd4	$⊢ ((ψ (u) \in ℂ \land ψ (N) \in ℂ) \land (u \in ℂ \land N \in ℂ)) \to ψ (u) - ψ (N) - (u - N) = ψ (u) + N - (ψ (N) + u)$
226		sub4	$⊢ ((ψ (u) \in ℂ \land ψ (N) \in ℂ) \land (u \in ℂ \land N \in ℂ)) \to ψ (u) - ψ (N) - (u - N) = ψ (u) - u - (ψ (N) - N)$
227		addsub4	$⊢ ((ψ (u) \in ℂ \land N \in ℂ) \land (ψ (N) \in ℂ \land u \in ℂ)) \to ψ (u) + N - (ψ (N) + u) = (ψ (u) - ψ (N)) + N - u$
228	227	an42s	$⊢ ((ψ (u) \in ℂ \land ψ (N) \in ℂ) \land (u \in ℂ \land N \in ℂ)) \to ψ (u) + N - (ψ (N) + u) = (ψ (u) - ψ (N)) + N - u$
229	225 226 228	3eqtr3d	$⊢ ((ψ (u) \in ℂ \land ψ (N) \in ℂ) \land (u \in ℂ \land N \in ℂ)) \to ψ (u) - u - (ψ (N) - N) = (ψ (u) - ψ (N)) + N - u$
230	223 224 164 165 229	syl22anc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (u) - u - (ψ (N) - N) = (ψ (u) - ψ (N)) + N - u$
231	222 230	eqtr2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (ψ (u) - ψ (N)) + N - u = R (u) - R (N)$
232	231	fveq2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(ψ (u) - ψ (N)) + N - u\| = \|R (u) - R (N)\|$
233	106	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to u - N \in ℂ$
234		chpwordi	$⊢ (N \in ℝ \land u \in ℝ \land N \leq u) \to ψ (N) \leq ψ (u)$
235	105 81 83 234	syl3anc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (N) \leq ψ (u)$
236	147 145 235	abssubge0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|ψ (u) - ψ (N)\| = ψ (u) - ψ (N)$
237	105 81 83	abssuble0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|N - u\| = u - N$
238	236 237	oveq12d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|ψ (u) - ψ (N)\| + \|N - u\| = (ψ (u) - ψ (N)) + u - N$
239	215 233 238	comraddd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|ψ (u) - ψ (N)\| + \|N - u\| = (u - N) + ψ (u) - ψ (N)$
240	217 232 239	3brtr3d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|R (u) - R (N)\| \leq (u - N) + ψ (u) - ψ (N)$
241	155 213 82 240	lediv1dd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{\|R (u) - R (N)\|}{N} \leq \frac{(u - N) + ψ (u) - ψ (N)}{N}$
242	156 214 151 241	leadd2dd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{\|R (u) - R (N)\|}{N}) \leq (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{(u - N) + ψ (u) - ψ (N)}{N})$
243	151	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \|\frac{R (u)}{u}\| \in ℂ$
244	149	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{ψ (u) - ψ (N)}{N} \in ℂ$
245	243 197 244	addassd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{u - N}{N}) + (\frac{ψ (u) - ψ (N)}{N}) = (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{u - N}{N}) + (\frac{ψ (u) - ψ (N)}{N})$
246	90	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| \in ℂ$
247	197 246 174	adddid	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) = (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{u - N}{N}) \cdot 1$
248	197	mulridd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \cdot 1 = \frac{u - N}{N}$
249	248	oveq2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{u - N}{N}) \cdot 1 = (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{u - N}{N})$
250	247 249	eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) = (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{u - N}{N})$
251	250	oveq1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{ψ (u) - ψ (N)}{N}) = (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{u - N}{N}) + (\frac{ψ (u) - ψ (N)}{N})$
252	233 215 165 166	divdird	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{(u - N) + ψ (u) - ψ (N)}{N} = (\frac{u - N}{N}) + (\frac{ψ (u) - ψ (N)}{N})$
253	252	oveq2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{(u - N) + ψ (u) - ψ (N)}{N}) = (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{u - N}{N}) + (\frac{ψ (u) - ψ (N)}{N})$
254	245 251 253	3eqtr4d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{ψ (u) - ψ (N)}{N}) = (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{(u - N) + ψ (u) - ψ (N)}{N})$
255	242 254	breqtrrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) \|\frac{R (u)}{u}\| + (\frac{\|R (u) - R (N)\|}{N}) \leq (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{ψ (u) - ψ (N)}{N})$
256	97 157 150 212 255	letrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| \leq (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{ψ (u) - ψ (N)}{N})$
257		remulcl	$⊢ (2 \in ℝ \land \frac{u - N}{N} \in ℝ) \to 2 (\frac{u - N}{N}) \in ℝ$
258	29 107 257	sylancr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 (\frac{u - N}{N}) \in ℝ$
259	258 139	readdcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 (\frac{u - N}{N}) + (\frac{T}{\log N}) \in ℝ$
260		remulcl	$⊢ (2 \in ℝ \land u - N \in ℝ) \to 2 (u - N) \in ℝ$
261	29 106 260	sylancr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 (u - N) \in ℝ$
262	105 138	rerpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{N}{\log N} \in ℝ$
263	113 262	remulcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to T (\frac{N}{\log N}) \in ℝ$
264	261 263	readdcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 (u - N) + T (\frac{N}{\log N}) \in ℝ$
265		fveq2	$⊢ y = u \to ψ (y) = ψ (u)$
266	265	oveq1d	$⊢ y = u \to ψ (y) - ψ (N) = ψ (u) - ψ (N)$
267		oveq1	$⊢ y = u \to y - N = u - N$
268	267	oveq2d	$⊢ y = u \to 2 (y - N) = 2 (u - N)$
269	268	oveq1d	$⊢ y = u \to 2 (y - N) + T (\frac{N}{\log N}) = 2 (u - N) + T (\frac{N}{\log N})$
270	266 269	breq12d	$⊢ y = u \to (ψ (y) - ψ (N) \leq 2 (y - N) + T (\frac{N}{\log N}) \leftrightarrow ψ (u) - ψ (N) \leq 2 (u - N) + T (\frac{N}{\log N}))$
271		id	$⊢ x = N \to x = N$
272		oveq2	$⊢ x = N \to 2 x = 2 \cdot N$
273	271 272	oveq12d	$⊢ x = N \to [x, 2 x] = [N, 2 \cdot N]$
274		fveq2	$⊢ x = N \to ψ (x) = ψ (N)$
275	274	oveq2d	$⊢ x = N \to ψ (y) - ψ (x) = ψ (y) - ψ (N)$
276		oveq2	$⊢ x = N \to y - x = y - N$
277	276	oveq2d	$⊢ x = N \to 2 (y - x) = 2 (y - N)$
278		fveq2	$⊢ x = N \to \log x = \log N$
279	271 278	oveq12d	$⊢ x = N \to \frac{x}{\log x} = \frac{N}{\log N}$
280	279	oveq2d	$⊢ x = N \to T (\frac{x}{\log x}) = T (\frac{N}{\log N})$
281	277 280	oveq12d	$⊢ x = N \to 2 (y - x) + T (\frac{x}{\log x}) = 2 (y - N) + T (\frac{N}{\log N})$
282	275 281	breq12d	$⊢ x = N \to (ψ (y) - ψ (x) \leq 2 (y - x) + T (\frac{x}{\log x}) \leftrightarrow ψ (y) - ψ (N) \leq 2 (y - N) + T (\frac{N}{\log N}))$
283	273 282	raleqbidv	$⊢ x = N \to (\forall y \in [x, 2 x] ψ (y) - ψ (x) \leq 2 (y - x) + T (\frac{x}{\log x}) \leftrightarrow \forall y \in [N, 2 \cdot N] ψ (y) - ψ (N) \leq 2 (y - N) + T (\frac{N}{\log N}))$
284	12	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \forall x \in (1, +∞) \forall y \in [x, 2 x] ψ (y) - ψ (x) \leq 2 (y - x) + T (\frac{x}{\log x})$
285		1xr	$⊢ 1 \in ℝ^{*}$
286		elioopnf	$⊢ 1 \in ℝ^{*} \to (N \in (1, +∞) \leftrightarrow (N \in ℝ \land 1 < N))$
287	285 286	ax-mp	$⊢ N \in (1, +∞) \leftrightarrow (N \in ℝ \land 1 < N)$
288	105 137 287	sylanbrc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to N \in (1, +∞)$
289	283 284 288	rspcdva	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \forall y \in [N, 2 \cdot N] ψ (y) - ψ (N) \leq 2 (y - N) + T (\frac{N}{\log N})$
290	28	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (1 + L E) \cdot N \in ℝ$
291	31	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 \cdot N \in ℝ$
292	80	simp3d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to u \leq (1 + L E) \cdot N$
293		ltle	$⊢ (1 + L E \in ℝ \land 2 \in ℝ) \to (1 + L E < 2 \to 1 + L E \leq 2)$
294	26 29 293	sylancl	$⊢ φ \to (1 + L E < 2 \to 1 + L E \leq 2)$
295	67 294	mpd	$⊢ φ \to 1 + L E \leq 2$
296	295	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 1 + L E \leq 2$
297	26	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 1 + L E \in ℝ$
298	29	a1i	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 \in ℝ$
299	297 298 82	lemul1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (1 + L E \leq 2 \leftrightarrow (1 + L E) \cdot N \leq 2 \cdot N)$
300	296 299	mpbid	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (1 + L E) \cdot N \leq 2 \cdot N$
301	81 290 291 292 300	letrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to u \leq 2 \cdot N$
302		elicc2	$⊢ (N \in ℝ \land 2 \cdot N \in ℝ) \to (u \in [N, 2 \cdot N] \leftrightarrow (u \in ℝ \land N \leq u \land u \leq 2 \cdot N))$
303	105 291 302	syl2anc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (u \in [N, 2 \cdot N] \leftrightarrow (u \in ℝ \land N \leq u \land u \leq 2 \cdot N))$
304	81 83 301 303	mpbir3and	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to u \in [N, 2 \cdot N]$
305	270 289 304	rspcdva	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ψ (u) - ψ (N) \leq 2 (u - N) + T (\frac{N}{\log N})$
306	148 264 82 305	lediv1dd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{ψ (u) - ψ (N)}{N} \leq \frac{2 (u - N) + T (\frac{N}{\log N})}{N}$
307	261	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 (u - N) \in ℂ$
308	11	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to T \in ℝ^{+}$
309	308	rpred	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to T \in ℝ$
310	309 262	remulcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to T (\frac{N}{\log N}) \in ℝ$
311	310	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to T (\frac{N}{\log N}) \in ℂ$
312		divdir	$⊢ (2 (u - N) \in ℂ \land T (\frac{N}{\log N}) \in ℂ \land (N \in ℂ \land N \neq 0)) \to \frac{2 (u - N) + T (\frac{N}{\log N})}{N} = (\frac{2 (u - N)}{N}) + (\frac{T (\frac{N}{\log N})}{N})$
313	307 311 177 312	syl3anc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{2 (u - N) + T (\frac{N}{\log N})}{N} = (\frac{2 (u - N)}{N}) + (\frac{T (\frac{N}{\log N})}{N})$
314		2cnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 \in ℂ$
315	314 233 165 166	divassd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{2 (u - N)}{N} = 2 (\frac{u - N}{N})$
316	113	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to T \in ℂ$
317	138	rpcnne0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\log N \in ℂ \land \log N \neq 0)$
318		div12	$⊢ (T \in ℂ \land N \in ℂ \land (\log N \in ℂ \land \log N \neq 0)) \to T (\frac{N}{\log N}) = N (\frac{T}{\log N})$
319	316 165 317 318	syl3anc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to T (\frac{N}{\log N}) = N (\frac{T}{\log N})$
320	319	oveq1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T (\frac{N}{\log N})}{N} = \frac{N (\frac{T}{\log N})}{N}$
321	308 138	rpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\log N} \in ℝ^{+}$
322	321	rpcnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\log N} \in ℂ$
323	322 165 166	divcan3d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{N (\frac{T}{\log N})}{N} = \frac{T}{\log N}$
324	320 323	eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T (\frac{N}{\log N})}{N} = \frac{T}{\log N}$
325	315 324	oveq12d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{2 (u - N)}{N}) + (\frac{T (\frac{N}{\log N})}{N}) = 2 (\frac{u - N}{N}) + (\frac{T}{\log N})$
326	313 325	eqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{2 (u - N) + T (\frac{N}{\log N})}{N} = 2 (\frac{u - N}{N}) + (\frac{T}{\log N})$
327	306 326	breqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{ψ (u) - ψ (N)}{N} \leq 2 (\frac{u - N}{N}) + (\frac{T}{\log N})$
328	149 259 143 327	leadd2dd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{ψ (u) - ψ (N)}{N}) \leq (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + 2 (\frac{u - N}{N}) + (\frac{T}{\log N})$
329	143	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) \in ℂ$
330	258	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 (\frac{u - N}{N}) \in ℂ$
331	139	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\log N} \in ℂ$
332	329 330 331	addassd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + 2 (\frac{u - N}{N}) + (\frac{T}{\log N}) = (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + 2 (\frac{u - N}{N}) + (\frac{T}{\log N})$
333		2cn	$⊢ 2 \in ℂ$
334		mulcom	$⊢ (2 \in ℂ \land \frac{u - N}{N} \in ℂ) \to 2 (\frac{u - N}{N}) = (\frac{u - N}{N}) \cdot 2$
335	333 197 334	sylancr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 (\frac{u - N}{N}) = (\frac{u - N}{N}) \cdot 2$
336	335	oveq2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + 2 (\frac{u - N}{N}) = (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{u - N}{N}) \cdot 2$
337	142	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| + 1 \in ℂ$
338	197 337 314	adddid	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1 + 2) = (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{u - N}{N}) \cdot 2$
339	246 174 314	addassd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| + 1 + 2 = \|\frac{R (u)}{u}\| + 1 + 2$
340		1p2e3	$⊢ 1 + 2 = 3$
341	340	oveq2i	$⊢ \|\frac{R (u)}{u}\| + 1 + 2 = \|\frac{R (u)}{u}\| + 3$
342	339 341	eqtrdi	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| + 1 + 2 = \|\frac{R (u)}{u}\| + 3$
343	342	oveq2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1 + 2) = (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3)$
344	336 338 343	3eqtr2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + 2 (\frac{u - N}{N}) = (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3)$
345	344	oveq1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + 2 (\frac{u - N}{N}) + (\frac{T}{\log N}) = (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) + (\frac{T}{\log N})$
346	332 345	eqtr3d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + 2 (\frac{u - N}{N}) + (\frac{T}{\log N}) = (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) + (\frac{T}{\log N})$
347	328 346	breqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 1) + (\frac{ψ (u) - ψ (N)}{N}) \leq (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) + (\frac{T}{\log N})$
348	97 150 140 256 347	letrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| \leq (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) + (\frac{T}{\log N})$
349	104	rehalfcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{\frac{E}{2}}{2} \in ℝ$
350	81 297 82	ledivmul2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u}{N} \leq 1 + L E \leftrightarrow u \leq (1 + L E) \cdot N)$
351	292 350	mpbird	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u}{N} \leq 1 + L E$
352		ax-1cn	$⊢ 1 \in ℂ$
353	25	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to L E \in ℝ$
354	353	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to L E \in ℂ$
355		addcom	$⊢ (1 \in ℂ \land L E \in ℂ) \to 1 + L E = L E + 1$
356	352 354 355	sylancr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 1 + L E = L E + 1$
357	351 356	breqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u}{N} \leq L E + 1$
358	172 114 353	lesubaddd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ((\frac{u}{N}) - 1 \leq L E \leftrightarrow \frac{u}{N} \leq L E + 1)$
359	357 358	mpbird	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u}{N}) - 1 \leq L E$
360	170 359	eqbrtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{u - N}{N} \leq L E$
361	2	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to A \in ℝ^{+}$
362	361	rpred	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to A \in ℝ$
363		fveq2	$⊢ x = u \to R (x) = R (u)$
364		id	$⊢ x = u \to x = u$
365	363 364	oveq12d	$⊢ x = u \to \frac{R (x)}{x} = \frac{R (u)}{u}$
366	365	fveq2d	$⊢ x = u \to \|\frac{R (x)}{x}\| = \|\frac{R (u)}{u}\|$
367	366	breq1d	$⊢ x = u \to (\|\frac{R (x)}{x}\| \leq A \leftrightarrow \|\frac{R (u)}{u}\| \leq A)$
368	4	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
369	367 368 84	rspcdva	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| \leq A$
370	90 362 109 369	leadd1dd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| + 3 \leq A + 3$
371	107 201	jca	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N} \in ℝ \land 0 \leq \frac{u - N}{N})$
372		3rp	$⊢ 3 \in ℝ^{+}$
373		rpaddcl	$⊢ (A \in ℝ^{+} \land 3 \in ℝ^{+}) \to A + 3 \in ℝ^{+}$
374	361 372 373	sylancl	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to A + 3 \in ℝ^{+}$
375	374	rprege0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (A + 3 \in ℝ \land 0 \leq A + 3)$
376		lemul12b	$⊢ (((\frac{u - N}{N} \in ℝ \land 0 \leq \frac{u - N}{N}) \land L E \in ℝ) \land (\|\frac{R (u)}{u}\| + 3 \in ℝ \land (A + 3 \in ℝ \land 0 \leq A + 3))) \to ((\frac{u - N}{N} \leq L E \land \|\frac{R (u)}{u}\| + 3 \leq A + 3) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) \leq L E (A + 3))$
377	371 353 110 375 376	syl22anc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to ((\frac{u - N}{N} \leq L E \land \|\frac{R (u)}{u}\| + 3 \leq A + 3) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) \leq L E (A + 3))$
378	360 370 377	mp2and	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) \leq L E (A + 3)$
379	43	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to E \in ℝ^{+}$
380	115 116	mp1i	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 4 \in ℝ^{+}$
381	379 380	rpdivcld	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{E}{4} \in ℝ^{+}$
382	381	rpcnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{E}{4} \in ℂ$
383	374	rpcnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to A + 3 \in ℂ$
384	374	rpne0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to A + 3 \neq 0$
385	382 383 384	divcan1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{\frac{E}{4}}{A + 3}) (A + 3) = \frac{E}{4}$
386	24	recnd	$⊢ φ \to E \in ℂ$
387	386	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to E \in ℂ$
388	380	rpcnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 4 \in ℂ$
389	380	rpne0d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 4 \neq 0$
390	387 388 389	divrec2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{E}{4} = (\frac{1}{4}) E$
391	390	oveq1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{\frac{E}{4}}{A + 3} = \frac{(\frac{1}{4}) E}{A + 3}$
392		4cn	$⊢ 4 \in ℂ$
393		4ne0	$⊢ 4 \neq 0$
394	392 393	reccli	$⊢ \frac{1}{4} \in ℂ$
395	394	a1i	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{1}{4} \in ℂ$
396	395 387 383 384	div23d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{(\frac{1}{4}) E}{A + 3} = (\frac{\frac{1}{4}}{A + 3}) E$
397	3	oveq1i	$⊢ L E = (\frac{\frac{1}{4}}{A + 3}) E$
398	396 397	eqtr4di	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{(\frac{1}{4}) E}{A + 3} = L E$
399	391 398	eqtr2d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to L E = \frac{\frac{E}{4}}{A + 3}$
400	399	oveq1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to L E (A + 3) = (\frac{\frac{E}{4}}{A + 3}) (A + 3)$
401		2ne0	$⊢ 2 \neq 0$
402	401	a1i	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to 2 \neq 0$
403	387 314 314 402 402	divdiv1d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{\frac{E}{2}}{2} = \frac{E}{2 \cdot 2}$
404		2t2e4	$⊢ 2 \cdot 2 = 4$
405	404	oveq2i	$⊢ \frac{E}{2 \cdot 2} = \frac{E}{4}$
406	403 405	eqtrdi	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{\frac{E}{2}}{2} = \frac{E}{4}$
407	385 400 406	3eqtr4d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to L E (A + 3) = \frac{\frac{E}{2}}{2}$
408	378 407	breqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) \leq \frac{\frac{E}{2}}{2}$
409	120	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\frac{E}{4}} \in ℝ$
410	138	rpred	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \log N \in ℝ$
411	82	reeflogd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to e^{\log N} = N$
412	136 411	breqtrrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to e^{\frac{T}{\frac{E}{4}}} < e^{\log N}$
413		eflt	$⊢ (\frac{T}{\frac{E}{4}} \in ℝ \land \log N \in ℝ) \to (\frac{T}{\frac{E}{4}} < \log N \leftrightarrow e^{\frac{T}{\frac{E}{4}}} < e^{\log N})$
414	409 410 413	syl2anc	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{T}{\frac{E}{4}} < \log N \leftrightarrow e^{\frac{T}{\frac{E}{4}}} < e^{\log N})$
415	412 414	mpbird	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\frac{E}{4}} < \log N$
416	409 410 415	ltled	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\frac{E}{4}} \leq \log N$
417	113 381 138 416	lediv23d	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\log N} \leq \frac{E}{4}$
418	417 406	breqtrrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{T}{\log N} \leq \frac{\frac{E}{2}}{2}$
419	111 139 349 349 408 418	le2addd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) + (\frac{T}{\log N}) \leq (\frac{\frac{E}{2}}{2}) + (\frac{\frac{E}{2}}{2})$
420	104	recnd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \frac{E}{2} \in ℂ$
421	420	2halvesd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{\frac{E}{2}}{2}) + (\frac{\frac{E}{2}}{2}) = \frac{E}{2}$
422	419 421	breqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{u - N}{N}) (\|\frac{R (u)}{u}\| + 3) + (\frac{T}{\log N}) \leq \frac{E}{2}$
423	97 140 104 348 422	letrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| \leq \frac{E}{2}$
424	16	simprd	$⊢ φ \to \|\frac{R (N)}{N}\| \leq \frac{E}{2}$
425	424	adantr	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (N)}{N}\| \leq \frac{E}{2}$
426	97 98 104 104 423 425	le2addd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| + \|\frac{R (N)}{N}\| \leq (\frac{E}{2}) + (\frac{E}{2})$
427	387	2halvesd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to (\frac{E}{2}) + (\frac{E}{2}) = E$
428	426 427	breqtrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|(\frac{R (u)}{u}) - (\frac{R (N)}{N})\| + \|\frac{R (N)}{N}\| \leq E$
429	90 99 100 103 428	letrd	$⊢ (φ \land u \in [N, (1 + L E) \cdot N]) \to \|\frac{R (u)}{u}\| \leq E$
430	429	ralrimiva	$⊢ φ \to \forall u \in [N, (1 + L E) \cdot N] \|\frac{R (u)}{u}\| \leq E$
431	19 79 430	jca31	$⊢ φ \to ((Y < N \land (1 + L E) \cdot N < M Y) \land \forall u \in [N, (1 + L E) \cdot N] \|\frac{R (u)}{u}\| \leq E)$
432		breq2	$⊢ z = N \to (Y < z \leftrightarrow Y < N)$
433		oveq2	$⊢ z = N \to (1 + L E) z = (1 + L E) \cdot N$
434	433	breq1d	$⊢ z = N \to ((1 + L E) z < M Y \leftrightarrow (1 + L E) \cdot N < M Y)$
435	432 434	anbi12d	$⊢ z = N \to ((Y < z \land (1 + L E) z < M Y) \leftrightarrow (Y < N \land (1 + L E) \cdot N < M Y))$
436		id	$⊢ z = N \to z = N$
437	436 433	oveq12d	$⊢ z = N \to [z, (1 + L E) z] = [N, (1 + L E) \cdot N]$
438	437	raleqdv	$⊢ z = N \to (\forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E \leftrightarrow \forall u \in [N, (1 + L E) \cdot N] \|\frac{R (u)}{u}\| \leq E)$
439	435 438	anbi12d	$⊢ z = N \to (((Y < z \land (1 + L E) z < M Y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E) \leftrightarrow ((Y < N \land (1 + L E) \cdot N < M Y) \land \forall u \in [N, (1 + L E) \cdot N] \|\frac{R (u)}{u}\| \leq E))$
440	439	rspcev	$⊢ (N \in ℝ^{+} \land ((Y < N \land (1 + L E) \cdot N < M Y) \land \forall u \in [N, (1 + L E) \cdot N] \|\frac{R (u)}{u}\| \leq E)) \to \exists z \in ℝ^{+} ((Y < z \land (1 + L E) z < M Y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
441	17 431 440	syl2anc	$⊢ φ \to \exists z \in ℝ^{+} ((Y < z \land (1 + L E) z < M Y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$

Metamath Proof Explorer

Theorem pntibndlem2

Proof