pntibnd

Description: Lemma for pnt . Establish smallness of R on an interval. Lemma 10.6.2 in Shapiro, p. 436. (Contributed by Mario Carneiro, 10-Apr-2016)

		Ref	Expression
	Hypothesis	pntlem1.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	pntibnd	$⊢ \exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \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		pntlem1.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2	1	pntrmax	$⊢ \exists d \in ℝ^{+} \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d$
3	1	pntpbnd	$⊢ \exists b \in ℝ^{+} \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f)$
4		reeanv	$⊢ \exists d \in ℝ^{+} \exists b \in ℝ^{+} (\forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f)) \leftrightarrow (\exists d \in ℝ^{+} \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \exists b \in ℝ^{+} \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f))$
5		2rp	$⊢ 2 \in ℝ^{+}$
6		rpmulcl	$⊢ (2 \in ℝ^{+} \land b \in ℝ^{+}) \to 2 b \in ℝ^{+}$
7	5 6	mpan	$⊢ b \in ℝ^{+} \to 2 b \in ℝ^{+}$
8		2re	$⊢ 2 \in ℝ$
9		1lt2	$⊢ 1 < 2$
10		rplogcl	$⊢ (2 \in ℝ \land 1 < 2) \to \log 2 \in ℝ^{+}$
11	8 9 10	mp2an	$⊢ \log 2 \in ℝ^{+}$
12		rpaddcl	$⊢ (2 b \in ℝ^{+} \land \log 2 \in ℝ^{+}) \to 2 b + \log 2 \in ℝ^{+}$
13	7 11 12	sylancl	$⊢ b \in ℝ^{+} \to 2 b + \log 2 \in ℝ^{+}$
14	13	ad2antlr	$⊢ ((d \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f))) \to 2 b + \log 2 \in ℝ^{+}$
15		id	$⊢ d \in ℝ^{+} \to d \in ℝ^{+}$
16		eqid	$⊢ \frac{\frac{1}{4}}{d + 3} = \frac{\frac{1}{4}}{d + 3}$
17	1 15 16	pntibndlem1	$⊢ d \in ℝ^{+} \to \frac{\frac{1}{4}}{d + 3} \in (0, 1)$
18	17	ad2antrr	$⊢ ((d \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f))) \to \frac{\frac{1}{4}}{d + 3} \in (0, 1)$
19		elioore	$⊢ e \in (0, 1) \to e \in ℝ$
20		eliooord	$⊢ e \in (0, 1) \to (0 < e \land e < 1)$
21	20	simpld	$⊢ e \in (0, 1) \to 0 < e$
22	19 21	elrpd	$⊢ e \in (0, 1) \to e \in ℝ^{+}$
23	22	rphalfcld	$⊢ e \in (0, 1) \to \frac{e}{2} \in ℝ^{+}$
24	23	rpred	$⊢ e \in (0, 1) \to \frac{e}{2} \in ℝ$
25	23	rpgt0d	$⊢ e \in (0, 1) \to 0 < \frac{e}{2}$
26		1red	$⊢ e \in (0, 1) \to 1 \in ℝ$
27		rphalflt	$⊢ e \in ℝ^{+} \to \frac{e}{2} < e$
28	22 27	syl	$⊢ e \in (0, 1) \to \frac{e}{2} < e$
29	20	simprd	$⊢ e \in (0, 1) \to e < 1$
30	24 19 26 28 29	lttrd	$⊢ e \in (0, 1) \to \frac{e}{2} < 1$
31		0xr	$⊢ 0 \in ℝ^{*}$
32		1xr	$⊢ 1 \in ℝ^{*}$
33		elioo2	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (\frac{e}{2} \in (0, 1) \leftrightarrow (\frac{e}{2} \in ℝ \land 0 < \frac{e}{2} \land \frac{e}{2} < 1))$
34	31 32 33	mp2an	$⊢ \frac{e}{2} \in (0, 1) \leftrightarrow (\frac{e}{2} \in ℝ \land 0 < \frac{e}{2} \land \frac{e}{2} < 1)$
35	24 25 30 34	syl3anbrc	$⊢ e \in (0, 1) \to \frac{e}{2} \in (0, 1)$
36	35	adantl	$⊢ (((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \to \frac{e}{2} \in (0, 1)$
37		oveq2	$⊢ f = \frac{e}{2} \to \frac{b}{f} = \frac{b}{\frac{e}{2}}$
38	37	fveq2d	$⊢ f = \frac{e}{2} \to e^{\frac{b}{f}} = e^{\frac{b}{\frac{e}{2}}}$
39	38	oveq1d	$⊢ f = \frac{e}{2} \to [e^{\frac{b}{f}}, +∞) = [e^{\frac{b}{\frac{e}{2}}}, +∞)$
40		breq2	$⊢ f = \frac{e}{2} \to (\|\frac{R (n)}{n}\| \leq f \leftrightarrow \|\frac{R (n)}{n}\| \leq \frac{e}{2})$
41	40	anbi2d	$⊢ f = \frac{e}{2} \to (((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \leftrightarrow ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))$
42	41	rexbidv	$⊢ f = \frac{e}{2} \to (\exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \leftrightarrow \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))$
43	42	ralbidv	$⊢ f = \frac{e}{2} \to (\forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \leftrightarrow \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))$
44	39 43	raleqbidv	$⊢ f = \frac{e}{2} \to (\forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \leftrightarrow \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))$
45	44	rexbidv	$⊢ f = \frac{e}{2} \to (\exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \leftrightarrow \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))$
46	45	rspcv	$⊢ \frac{e}{2} \in (0, 1) \to (\forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \to \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))$
47	36 46	syl	$⊢ (((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \to (\forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \to \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))$
48		simp-4l	$⊢ ((((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \land (g \in ℝ^{+} \land \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))) \to d \in ℝ^{+}$
49		simpllr	$⊢ ((((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \land (g \in ℝ^{+} \land \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))) \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d$
50		simplr	$⊢ ((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \to b \in ℝ^{+}$
51	50	ad2antrr	$⊢ ((((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \land (g \in ℝ^{+} \land \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))) \to b \in ℝ^{+}$
52		eqid	$⊢ e^{\frac{b}{\frac{e}{2}}} = e^{\frac{b}{\frac{e}{2}}}$
53		eqid	$⊢ 2 b + \log 2 = 2 b + \log 2$
54		simplr	$⊢ ((((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \land (g \in ℝ^{+} \land \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))) \to e \in (0, 1)$
55		simprl	$⊢ ((((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \land (g \in ℝ^{+} \land \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))) \to g \in ℝ^{+}$
56		simprr	$⊢ ((((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \land (g \in ℝ^{+} \land \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))) \to \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2})$
57	1 48 16 49 51 52 53 54 55 56	pntibndlem3	$⊢ ((((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \land (g \in ℝ^{+} \land \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}))) \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{e}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e)$
58	57	rexlimdvaa	$⊢ (((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \to (\exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{\frac{e}{2}}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq \frac{e}{2}) \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{e}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e))$
59	47 58	syld	$⊢ (((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \land e \in (0, 1)) \to (\forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{e}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e))$
60	59	ralrimdva	$⊢ ((d \in ℝ^{+} \land b \in ℝ^{+}) \land \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d) \to (\forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f) \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{e}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e))$
61	60	impr	$⊢ ((d \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f))) \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{e}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e)$
62		fvoveq1	$⊢ c = 2 b + \log 2 \to e^{\frac{c}{e}} = e^{\frac{2 b + \log 2}{e}}$
63	62	oveq1d	$⊢ c = 2 b + \log 2 \to [e^{\frac{c}{e}}, +∞) = [e^{\frac{2 b + \log 2}{e}}, +∞)$
64	63	raleqdv	$⊢ c = 2 b + \log 2 \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{2 b + \log 2}{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))$
65	64	rexbidv	$⊢ c = 2 b + \log 2 \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) \leftrightarrow \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{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))$
66	65	ralbidv	$⊢ c = 2 b + \log 2 \to (\forall e \in (0, 1) \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) \leftrightarrow \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{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))$
67		oveq1	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to l e = (\frac{\frac{1}{4}}{d + 3}) e$
68	67	oveq2d	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to 1 + l e = 1 + (\frac{\frac{1}{4}}{d + 3}) e$
69	68	oveq1d	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to (1 + l e) z = (1 + (\frac{\frac{1}{4}}{d + 3}) e) z$
70	69	breq1d	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to ((1 + l e) z < k y \leftrightarrow (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y)$
71	70	anbi2d	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to ((y < z \land (1 + l e) z < k y) \leftrightarrow (y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y))$
72	69	oveq2d	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to [z, (1 + l e) z] = [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z]$
73	72	raleqdv	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to (\forall u \in [z, (1 + l e) z] \|\frac{R (u)}{u}\| \leq e \leftrightarrow \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e)$
74	71 73	anbi12d	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to (((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 ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e))$
75	74	rexbidv	$⊢ l = \frac{\frac{1}{4}}{d + 3} \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) \leftrightarrow \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e))$
76	75	ralbidv	$⊢ l = \frac{\frac{1}{4}}{d + 3} \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 (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e))$
77	76	rexralbidv	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to (\exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{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 \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{e}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e))$
78	77	ralbidv	$⊢ l = \frac{\frac{1}{4}}{d + 3} \to (\forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{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 e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{e}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e))$
79	66 78	rspc2ev	$⊢ (2 b + \log 2 \in ℝ^{+} \land \frac{\frac{1}{4}}{d + 3} \in (0, 1) \land \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{2 b + \log 2}{e}}, +∞) \forall y \in (x, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + (\frac{\frac{1}{4}}{d + 3}) e) z < k y) \land \forall u \in [z, (1 + (\frac{\frac{1}{4}}{d + 3}) e) z] \|\frac{R (u)}{u}\| \leq e)) \to \exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \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)$
80	14 18 61 79	syl3anc	$⊢ ((d \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f))) \to \exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \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)$
81	80	ex	$⊢ (d \in ℝ^{+} \land b \in ℝ^{+}) \to ((\forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f)) \to \exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \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))$
82	81	rexlimivv	$⊢ \exists d \in ℝ^{+} \exists b \in ℝ^{+} (\forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f)) \to \exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \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)$
83	4 82	sylbir	$⊢ (\exists d \in ℝ^{+} \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq d \land \exists b \in ℝ^{+} \forall f \in (0, 1) \exists g \in ℝ^{+} \forall m \in [e^{\frac{b}{f}}, +∞) \forall v \in (g, +∞) \exists n \in ℕ ((v < n \land n \leq m v) \land \|\frac{R (n)}{n}\| \leq f)) \to \exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \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)$
84	2 3 83	mp2an	$⊢ \exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \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 pntibnd

Proof