pntlem3

Description: Lemma for pnt . Equation 10.6.35 in Shapiro, p. 436. (Contributed by Mario Carneiro, 8-Apr-2016) (Proof shortened by AV, 27-Sep-2020)

	Ref	Expression
Hypotheses	pntlem3.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntlem3.a	$⊢ φ \to A \in ℝ^{+}$
	pntlem3.A	$⊢ φ \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
	pntlem3.1	$⊢ T = \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}$
	pntlem3.2	$⊢ φ \to C \in ℝ^{+}$
	pntlem3.3	$⊢ (φ \land u \in T) \to u - C u^{3} \in T$
Assertion	pntlem3	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$

Proof

Step	Hyp	Ref	Expression
1		pntlem3.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		pntlem3.a	$⊢ φ \to A \in ℝ^{+}$
3		pntlem3.A	$⊢ φ \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
4		pntlem3.1	$⊢ T = \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}$
5		pntlem3.2	$⊢ φ \to C \in ℝ^{+}$
6		pntlem3.3	$⊢ (φ \land u \in T) \to u - C u^{3} \in T$
7		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
8		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
9	8	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
10	9	a1i	$⊢ (φ \land 0 < inf (T ℝ <)) \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
11		ssid	$⊢ ℂ \subseteq ℂ$
12		cncfmptid	$⊢ (ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (p \in ℂ ⟼ p) : ℂ \underset{cn}{⟶} ℂ$
13	11 11 12	mp2an	$⊢ (p \in ℂ ⟼ p) : ℂ \underset{cn}{⟶} ℂ$
14	13	a1i	$⊢ (φ \land 0 < inf (T ℝ <)) \to (p \in ℂ ⟼ p) : ℂ \underset{cn}{⟶} ℂ$
15	5	adantr	$⊢ (φ \land 0 < inf (T ℝ <)) \to C \in ℝ^{+}$
16	15	rpcnd	$⊢ (φ \land 0 < inf (T ℝ <)) \to C \in ℂ$
17	11	a1i	$⊢ (φ \land 0 < inf (T ℝ <)) \to ℂ \subseteq ℂ$
18		cncfmptc	$⊢ (C \in ℂ \land ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (p \in ℂ ⟼ C) : ℂ \underset{cn}{⟶} ℂ$
19	16 17 17 18	syl3anc	$⊢ (φ \land 0 < inf (T ℝ <)) \to (p \in ℂ ⟼ C) : ℂ \underset{cn}{⟶} ℂ$
20		3nn0	$⊢ 3 \in ℕ_{0}$
21	8	expcn	$⊢ 3 \in ℕ_{0} \to (p \in ℂ ⟼ p^{3}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
22	20 21	mp1i	$⊢ (φ \land 0 < inf (T ℝ <)) \to (p \in ℂ ⟼ p^{3}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
23	8	cncfcn1	$⊢ ℂ \underset{cn}{⟶} ℂ = TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld})$
24	22 23	eleqtrrdi	$⊢ (φ \land 0 < inf (T ℝ <)) \to (p \in ℂ ⟼ p^{3}) : ℂ \underset{cn}{⟶} ℂ$
25	19 24	mulcncf	$⊢ (φ \land 0 < inf (T ℝ <)) \to (p \in ℂ ⟼ C p^{3}) : ℂ \underset{cn}{⟶} ℂ$
26	8 10 14 25	cncfmpt2f	$⊢ (φ \land 0 < inf (T ℝ <)) \to (p \in ℂ ⟼ p - C p^{3}) : ℂ \underset{cn}{⟶} ℂ$
27	4	ssrab3	$⊢ T \subseteq [0, A]$
28		0re	$⊢ 0 \in ℝ$
29	2	rpred	$⊢ φ \to A \in ℝ$
30		iccssre	$⊢ (0 \in ℝ \land A \in ℝ) \to [0, A] \subseteq ℝ$
31	28 29 30	sylancr	$⊢ φ \to [0, A] \subseteq ℝ$
32	27 31	sstrid	$⊢ φ \to T \subseteq ℝ$
33		0xr	$⊢ 0 \in ℝ^{*}$
34	2	rpxrd	$⊢ φ \to A \in ℝ^{*}$
35	2	rpge0d	$⊢ φ \to 0 \leq A$
36		ubicc2	$⊢ (0 \in ℝ^{} \land A \in ℝ^{} \land 0 \leq A) \to A \in [0, A]$
37	33 34 35 36	mp3an2i	$⊢ φ \to A \in [0, A]$
38		1rp	$⊢ 1 \in ℝ^{+}$
39		fveq2	$⊢ x = z \to R (x) = R (z)$
40		id	$⊢ x = z \to x = z$
41	39 40	oveq12d	$⊢ x = z \to \frac{R (x)}{x} = \frac{R (z)}{z}$
42	41	fveq2d	$⊢ x = z \to \|\frac{R (x)}{x}\| = \|\frac{R (z)}{z}\|$
43	42	breq1d	$⊢ x = z \to (\|\frac{R (x)}{x}\| \leq A \leftrightarrow \|\frac{R (z)}{z}\| \leq A)$
44	3	adantr	$⊢ (φ \land z \in [1, +∞)) \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
45		1re	$⊢ 1 \in ℝ$
46		elicopnf	$⊢ 1 \in ℝ \to (z \in [1, +∞) \leftrightarrow (z \in ℝ \land 1 \leq z))$
47	45 46	mp1i	$⊢ φ \to (z \in [1, +∞) \leftrightarrow (z \in ℝ \land 1 \leq z))$
48	47	simprbda	$⊢ (φ \land z \in [1, +∞)) \to z \in ℝ$
49		0red	$⊢ (φ \land z \in [1, +∞)) \to 0 \in ℝ$
50	45	a1i	$⊢ (φ \land z \in [1, +∞)) \to 1 \in ℝ$
51		0lt1	$⊢ 0 < 1$
52	51	a1i	$⊢ (φ \land z \in [1, +∞)) \to 0 < 1$
53	47	simplbda	$⊢ (φ \land z \in [1, +∞)) \to 1 \leq z$
54	49 50 48 52 53	ltletrd	$⊢ (φ \land z \in [1, +∞)) \to 0 < z$
55	48 54	elrpd	$⊢ (φ \land z \in [1, +∞)) \to z \in ℝ^{+}$
56	43 44 55	rspcdva	$⊢ (φ \land z \in [1, +∞)) \to \|\frac{R (z)}{z}\| \leq A$
57	56	ralrimiva	$⊢ φ \to \forall z \in [1, +∞) \|\frac{R (z)}{z}\| \leq A$
58		oveq1	$⊢ y = 1 \to [y, +∞) = [1, +∞)$
59	58	raleqdv	$⊢ y = 1 \to (\forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq A \leftrightarrow \forall z \in [1, +∞) \|\frac{R (z)}{z}\| \leq A)$
60	59	rspcev	$⊢ (1 \in ℝ^{+} \land \forall z \in [1, +∞) \|\frac{R (z)}{z}\| \leq A) \to \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq A$
61	38 57 60	sylancr	$⊢ φ \to \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq A$
62		breq2	$⊢ t = A \to (\|\frac{R (z)}{z}\| \leq t \leftrightarrow \|\frac{R (z)}{z}\| \leq A)$
63	62	rexralbidv	$⊢ t = A \to (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \leftrightarrow \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq A)$
64	63 4	elrab2	$⊢ A \in T \leftrightarrow (A \in [0, A] \land \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq A)$
65	37 61 64	sylanbrc	$⊢ φ \to A \in T$
66	65	ne0d	$⊢ φ \to T \neq \emptyset$
67		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (t \in [0, A] \leftrightarrow (t \in ℝ \land 0 \leq t \land t \leq A))$
68	28 29 67	sylancr	$⊢ φ \to (t \in [0, A] \leftrightarrow (t \in ℝ \land 0 \leq t \land t \leq A))$
69	68	biimpa	$⊢ (φ \land t \in [0, A]) \to (t \in ℝ \land 0 \leq t \land t \leq A)$
70	69	simp2d	$⊢ (φ \land t \in [0, A]) \to 0 \leq t$
71	70	a1d	$⊢ (φ \land t \in [0, A]) \to (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to 0 \leq t)$
72	71	ralrimiva	$⊢ φ \to \forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to 0 \leq t)$
73	4	raleqi	$⊢ \forall w \in T 0 \leq w \leftrightarrow \forall w \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\} 0 \leq w$
74		breq2	$⊢ w = t \to (0 \leq w \leftrightarrow 0 \leq t)$
75	74	ralrab2	$⊢ \forall w \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\} 0 \leq w \leftrightarrow \forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to 0 \leq t)$
76	73 75	bitri	$⊢ \forall w \in T 0 \leq w \leftrightarrow \forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to 0 \leq t)$
77	72 76	sylibr	$⊢ φ \to \forall w \in T 0 \leq w$
78		breq1	$⊢ x = 0 \to (x \leq w \leftrightarrow 0 \leq w)$
79	78	ralbidv	$⊢ x = 0 \to (\forall w \in T x \leq w \leftrightarrow \forall w \in T 0 \leq w)$
80	79	rspcev	$⊢ (0 \in ℝ \land \forall w \in T 0 \leq w) \to \exists x \in ℝ \forall w \in T x \leq w$
81	28 77 80	sylancr	$⊢ φ \to \exists x \in ℝ \forall w \in T x \leq w$
82		infrecl	$⊢ (T \subseteq ℝ \land T \neq \emptyset \land \exists x \in ℝ \forall w \in T x \leq w) \to inf (T ℝ <) \in ℝ$
83	32 66 81 82	syl3anc	$⊢ φ \to inf (T ℝ <) \in ℝ$
84	83	recnd	$⊢ φ \to inf (T ℝ <) \in ℂ$
85	84	adantr	$⊢ (φ \land 0 < inf (T ℝ <)) \to inf (T ℝ <) \in ℂ$
86		elrp	$⊢ inf (T ℝ <) \in ℝ^{+} \leftrightarrow (inf (T ℝ <) \in ℝ \land 0 < inf (T ℝ <))$
87	86	biimpri	$⊢ (inf (T ℝ <) \in ℝ \land 0 < inf (T ℝ <)) \to inf (T ℝ <) \in ℝ^{+}$
88	83 87	sylan	$⊢ (φ \land 0 < inf (T ℝ <)) \to inf (T ℝ <) \in ℝ^{+}$
89		3z	$⊢ 3 \in ℤ$
90		rpexpcl	$⊢ (inf (T ℝ <) \in ℝ^{+} \land 3 \in ℤ) \to {inf (T ℝ <)}^{3} \in ℝ^{+}$
91	88 89 90	sylancl	$⊢ (φ \land 0 < inf (T ℝ <)) \to {inf (T ℝ <)}^{3} \in ℝ^{+}$
92	15 91	rpmulcld	$⊢ (φ \land 0 < inf (T ℝ <)) \to C {inf (T ℝ <)}^{3} \in ℝ^{+}$
93		cncfi	$⊢ ((p \in ℂ ⟼ p - C p^{3}) : ℂ \underset{cn}{⟶} ℂ \land inf (T ℝ <) \in ℂ \land C {inf (T ℝ <)}^{3} \in ℝ^{+}) \to \exists s \in ℝ^{+} \forall u \in ℂ (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3})$
94	26 85 92 93	syl3anc	$⊢ (φ \land 0 < inf (T ℝ <)) \to \exists s \in ℝ^{+} \forall u \in ℂ (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3})$
95	83	ad2antrr	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to inf (T ℝ <) \in ℝ$
96		rphalfcl	$⊢ s \in ℝ^{+} \to \frac{s}{2} \in ℝ^{+}$
97	96	adantl	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to \frac{s}{2} \in ℝ^{+}$
98	95 97	ltaddrpd	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to inf (T ℝ <) < inf (T ℝ <) + (\frac{s}{2})$
99	97	rpred	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to \frac{s}{2} \in ℝ$
100	95 99	readdcld	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to inf (T ℝ <) + (\frac{s}{2}) \in ℝ$
101	95 100	ltnled	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to (inf (T ℝ <) < inf (T ℝ <) + (\frac{s}{2}) \leftrightarrow \neg inf (T ℝ <) + (\frac{s}{2}) \leq inf (T ℝ <))$
102	98 101	mpbid	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to \neg inf (T ℝ <) + (\frac{s}{2}) \leq inf (T ℝ <)$
103		ax-resscn	$⊢ ℝ \subseteq ℂ$
104	32 103	sstrdi	$⊢ φ \to T \subseteq ℂ$
105	104	ad2antrr	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to T \subseteq ℂ$
106		ssralv	$⊢ T \subseteq ℂ \to (\forall u \in ℂ (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3}) \to \forall u \in T (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3}))$
107	105 106	syl	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to (\forall u \in ℂ (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3}) \to \forall u \in T (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3}))$
108	32	ad2antrr	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to T \subseteq ℝ$
109	108	sselda	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to u \in ℝ$
110	100	adantr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) + (\frac{s}{2}) \in ℝ$
111	109 110	ltnled	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (u < inf (T ℝ <) + (\frac{s}{2}) \leftrightarrow \neg inf (T ℝ <) + (\frac{s}{2}) \leq u)$
112	83	ad3antrrr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) \in ℝ$
113	99	adantr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to \frac{s}{2} \in ℝ$
114	112 113	resubcld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) - (\frac{s}{2}) \in ℝ$
115	95 97	ltsubrpd	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to inf (T ℝ <) - (\frac{s}{2}) < inf (T ℝ <)$
116	115	adantr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) - (\frac{s}{2}) < inf (T ℝ <)$
117	32	ad3antrrr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to T \subseteq ℝ$
118	81	ad3antrrr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to \exists x \in ℝ \forall w \in T x \leq w$
119		simpr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to u \in T$
120		infrelb	$⊢ (T \subseteq ℝ \land \exists x \in ℝ \forall w \in T x \leq w \land u \in T) \to inf (T ℝ <) \leq u$
121	117 118 119 120	syl3anc	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) \leq u$
122	114 112 109 116 121	ltletrd	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) - (\frac{s}{2}) < u$
123	109 112 113	absdifltd	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (\|u - inf (T ℝ <)\| < \frac{s}{2} \leftrightarrow (inf (T ℝ <) - (\frac{s}{2}) < u \land u < inf (T ℝ <) + (\frac{s}{2})))$
124	123	biimprd	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to ((inf (T ℝ <) - (\frac{s}{2}) < u \land u < inf (T ℝ <) + (\frac{s}{2})) \to \|u - inf (T ℝ <)\| < \frac{s}{2})$
125	122 124	mpand	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (u < inf (T ℝ <) + (\frac{s}{2}) \to \|u - inf (T ℝ <)\| < \frac{s}{2})$
126		rphalflt	$⊢ s \in ℝ^{+} \to \frac{s}{2} < s$
127	126	ad2antlr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to \frac{s}{2} < s$
128	109 112	resubcld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to u - inf (T ℝ <) \in ℝ$
129	128	recnd	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to u - inf (T ℝ <) \in ℂ$
130	129	abscld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to \|u - inf (T ℝ <)\| \in ℝ$
131		rpre	$⊢ s \in ℝ^{+} \to s \in ℝ$
132	131	ad2antlr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to s \in ℝ$
133		lttr	$⊢ (\|u - inf (T ℝ <)\| \in ℝ \land \frac{s}{2} \in ℝ \land s \in ℝ) \to ((\|u - inf (T ℝ <)\| < \frac{s}{2} \land \frac{s}{2} < s) \to \|u - inf (T ℝ <)\| < s)$
134	130 113 132 133	syl3anc	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to ((\|u - inf (T ℝ <)\| < \frac{s}{2} \land \frac{s}{2} < s) \to \|u - inf (T ℝ <)\| < s)$
135	127 134	mpan2d	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (\|u - inf (T ℝ <)\| < \frac{s}{2} \to \|u - inf (T ℝ <)\| < s)$
136	125 135	syld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (u < inf (T ℝ <) + (\frac{s}{2}) \to \|u - inf (T ℝ <)\| < s)$
137	111 136	sylbird	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (\neg inf (T ℝ <) + (\frac{s}{2}) \leq u \to \|u - inf (T ℝ <)\| < s)$
138	137	con1d	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (\neg \|u - inf (T ℝ <)\| < s \to inf (T ℝ <) + (\frac{s}{2}) \leq u)$
139	109	recnd	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to u \in ℂ$
140		id	$⊢ p = u \to p = u$
141		oveq1	$⊢ p = u \to p^{3} = u^{3}$
142	141	oveq2d	$⊢ p = u \to C p^{3} = C u^{3}$
143	140 142	oveq12d	$⊢ p = u \to p - C p^{3} = u - C u^{3}$
144		eqid	$⊢ (p \in ℂ ⟼ p - C p^{3}) = (p \in ℂ ⟼ p - C p^{3})$
145		ovex	$⊢ u - C u^{3} \in V$
146	143 144 145	fvmpt	$⊢ u \in ℂ \to (p \in ℂ ⟼ p - C p^{3}) (u) = u - C u^{3}$
147	139 146	syl	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (p \in ℂ ⟼ p - C p^{3}) (u) = u - C u^{3}$
148	85	ad2antrr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) \in ℂ$
149		id	$⊢ p = inf (T ℝ <) \to p = inf (T ℝ <)$
150		oveq1	$⊢ p = inf (T ℝ <) \to p^{3} = {inf (T ℝ <)}^{3}$
151	150	oveq2d	$⊢ p = inf (T ℝ <) \to C p^{3} = C {inf (T ℝ <)}^{3}$
152	149 151	oveq12d	$⊢ p = inf (T ℝ <) \to p - C p^{3} = inf (T ℝ <) - C {inf (T ℝ <)}^{3}$
153		ovex	$⊢ inf (T ℝ <) - C {inf (T ℝ <)}^{3} \in V$
154	152 144 153	fvmpt	$⊢ inf (T ℝ <) \in ℂ \to (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <)) = inf (T ℝ <) - C {inf (T ℝ <)}^{3}$
155	148 154	syl	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <)) = inf (T ℝ <) - C {inf (T ℝ <)}^{3}$
156	147 155	oveq12d	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <)) = u - C u^{3} - (inf (T ℝ <) - C {inf (T ℝ <)}^{3})$
157	156	fveq2d	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| = \|u - C u^{3} - (inf (T ℝ <) - C {inf (T ℝ <)}^{3})\|$
158	157	breq1d	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (\|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3} \leftrightarrow \|u - C u^{3} - (inf (T ℝ <) - C {inf (T ℝ <)}^{3})\| < C {inf (T ℝ <)}^{3})$
159	5	rpred	$⊢ φ \to C \in ℝ$
160	159	ad3antrrr	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to C \in ℝ$
161		reexpcl	$⊢ (u \in ℝ \land 3 \in ℕ_{0}) \to u^{3} \in ℝ$
162	109 20 161	sylancl	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to u^{3} \in ℝ$
163	160 162	remulcld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to C u^{3} \in ℝ$
164	109 163	resubcld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to u - C u^{3} \in ℝ$
165	20	a1i	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to 3 \in ℕ_{0}$
166	112 165	reexpcld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to {inf (T ℝ <)}^{3} \in ℝ$
167	160 166	remulcld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to C {inf (T ℝ <)}^{3} \in ℝ$
168	112 167	resubcld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) - C {inf (T ℝ <)}^{3} \in ℝ$
169	164 168 167	absdifltd	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (\|u - C u^{3} - (inf (T ℝ <) - C {inf (T ℝ <)}^{3})\| < C {inf (T ℝ <)}^{3} \leftrightarrow (inf (T ℝ <) - C {inf (T ℝ <)}^{3} - C {inf (T ℝ <)}^{3} < u - C u^{3} \land u - C u^{3} < inf (T ℝ <) - C {inf (T ℝ <)}^{3} + C {inf (T ℝ <)}^{3}))$
170	167	recnd	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to C {inf (T ℝ <)}^{3} \in ℂ$
171	148 170	npcand	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) - C {inf (T ℝ <)}^{3} + C {inf (T ℝ <)}^{3} = inf (T ℝ <)$
172	171	breq2d	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (u - C u^{3} < inf (T ℝ <) - C {inf (T ℝ <)}^{3} + C {inf (T ℝ <)}^{3} \leftrightarrow u - C u^{3} < inf (T ℝ <))$
173	6	ad4ant14	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to u - C u^{3} \in T$
174		infrelb	$⊢ (T \subseteq ℝ \land \exists x \in ℝ \forall w \in T x \leq w \land u - C u^{3} \in T) \to inf (T ℝ <) \leq u - C u^{3}$
175	117 118 173 174	syl3anc	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to inf (T ℝ <) \leq u - C u^{3}$
176	112 164 175	lensymd	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to \neg u - C u^{3} < inf (T ℝ <)$
177	176	pm2.21d	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (u - C u^{3} < inf (T ℝ <) \to inf (T ℝ <) + (\frac{s}{2}) \leq u)$
178	172 177	sylbid	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (u - C u^{3} < inf (T ℝ <) - C {inf (T ℝ <)}^{3} + C {inf (T ℝ <)}^{3} \to inf (T ℝ <) + (\frac{s}{2}) \leq u)$
179	178	adantld	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to ((inf (T ℝ <) - C {inf (T ℝ <)}^{3} - C {inf (T ℝ <)}^{3} < u - C u^{3} \land u - C u^{3} < inf (T ℝ <) - C {inf (T ℝ <)}^{3} + C {inf (T ℝ <)}^{3}) \to inf (T ℝ <) + (\frac{s}{2}) \leq u)$
180	169 179	sylbid	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (\|u - C u^{3} - (inf (T ℝ <) - C {inf (T ℝ <)}^{3})\| < C {inf (T ℝ <)}^{3} \to inf (T ℝ <) + (\frac{s}{2}) \leq u)$
181	158 180	sylbid	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to (\|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3} \to inf (T ℝ <) + (\frac{s}{2}) \leq u)$
182	138 181	jad	$⊢ (((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \land u \in T) \to ((\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3}) \to inf (T ℝ <) + (\frac{s}{2}) \leq u)$
183	182	ralimdva	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to (\forall u \in T (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3}) \to \forall u \in T inf (T ℝ <) + (\frac{s}{2}) \leq u)$
184	66	ad2antrr	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to T \neq \emptyset$
185	81	ad2antrr	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to \exists x \in ℝ \forall w \in T x \leq w$
186		infregelb	$⊢ ((T \subseteq ℝ \land T \neq \emptyset \land \exists x \in ℝ \forall w \in T x \leq w) \land inf (T ℝ <) + (\frac{s}{2}) \in ℝ) \to (inf (T ℝ <) + (\frac{s}{2}) \leq inf (T ℝ <) \leftrightarrow \forall u \in T inf (T ℝ <) + (\frac{s}{2}) \leq u)$
187	108 184 185 100 186	syl31anc	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to (inf (T ℝ <) + (\frac{s}{2}) \leq inf (T ℝ <) \leftrightarrow \forall u \in T inf (T ℝ <) + (\frac{s}{2}) \leq u)$
188	183 187	sylibrd	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to (\forall u \in T (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3}) \to inf (T ℝ <) + (\frac{s}{2}) \leq inf (T ℝ <))$
189	107 188	syld	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to (\forall u \in ℂ (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3}) \to inf (T ℝ <) + (\frac{s}{2}) \leq inf (T ℝ <))$
190	102 189	mtod	$⊢ ((φ \land 0 < inf (T ℝ <)) \land s \in ℝ^{+}) \to \neg \forall u \in ℂ (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3})$
191	190	nrexdv	$⊢ (φ \land 0 < inf (T ℝ <)) \to \neg \exists s \in ℝ^{+} \forall u \in ℂ (\|u - inf (T ℝ <)\| < s \to \|(p \in ℂ ⟼ p - C p^{3}) (u) - (p \in ℂ ⟼ p - C p^{3}) (inf (T ℝ <))\| < C {inf (T ℝ <)}^{3})$
192	94 191	pm2.65da	$⊢ φ \to \neg 0 < inf (T ℝ <)$
193	192	adantr	$⊢ (φ \land s \in ℝ^{+}) \to \neg 0 < inf (T ℝ <)$
194	32	adantr	$⊢ (φ \land s \in ℝ^{+}) \to T \subseteq ℝ$
195	66	adantr	$⊢ (φ \land s \in ℝ^{+}) \to T \neq \emptyset$
196	81	adantr	$⊢ (φ \land s \in ℝ^{+}) \to \exists x \in ℝ \forall w \in T x \leq w$
197	131	adantl	$⊢ (φ \land s \in ℝ^{+}) \to s \in ℝ$
198		infregelb	$⊢ ((T \subseteq ℝ \land T \neq \emptyset \land \exists x \in ℝ \forall w \in T x \leq w) \land s \in ℝ) \to (s \leq inf (T ℝ <) \leftrightarrow \forall w \in T s \leq w)$
199	194 195 196 197 198	syl31anc	$⊢ (φ \land s \in ℝ^{+}) \to (s \leq inf (T ℝ <) \leftrightarrow \forall w \in T s \leq w)$
200	4	raleqi	$⊢ \forall w \in T s \leq w \leftrightarrow \forall w \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\} s \leq w$
201		breq2	$⊢ w = t \to (s \leq w \leftrightarrow s \leq t)$
202	201	ralrab2	$⊢ \forall w \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\} s \leq w \leftrightarrow \forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to s \leq t)$
203	200 202	bitri	$⊢ \forall w \in T s \leq w \leftrightarrow \forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to s \leq t)$
204	199 203	bitrdi	$⊢ (φ \land s \in ℝ^{+}) \to (s \leq inf (T ℝ <) \leftrightarrow \forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to s \leq t))$
205		rpgt0	$⊢ s \in ℝ^{+} \to 0 < s$
206	205	adantl	$⊢ (φ \land s \in ℝ^{+}) \to 0 < s$
207	83	adantr	$⊢ (φ \land s \in ℝ^{+}) \to inf (T ℝ <) \in ℝ$
208		ltletr	$⊢ (0 \in ℝ \land s \in ℝ \land inf (T ℝ <) \in ℝ) \to ((0 < s \land s \leq inf (T ℝ <)) \to 0 < inf (T ℝ <))$
209	28 197 207 208	mp3an2i	$⊢ (φ \land s \in ℝ^{+}) \to ((0 < s \land s \leq inf (T ℝ <)) \to 0 < inf (T ℝ <))$
210	206 209	mpand	$⊢ (φ \land s \in ℝ^{+}) \to (s \leq inf (T ℝ <) \to 0 < inf (T ℝ <))$
211	204 210	sylbird	$⊢ (φ \land s \in ℝ^{+}) \to (\forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to s \leq t) \to 0 < inf (T ℝ <))$
212	193 211	mtod	$⊢ (φ \land s \in ℝ^{+}) \to \neg \forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to s \leq t)$
213		rexanali	$⊢ \exists t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \land \neg s \leq t) \leftrightarrow \neg \forall t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to s \leq t)$
214	212 213	sylibr	$⊢ (φ \land s \in ℝ^{+}) \to \exists t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \land \neg s \leq t)$
215		fveq2	$⊢ z = x \to R (z) = R (x)$
216		id	$⊢ z = x \to z = x$
217	215 216	oveq12d	$⊢ z = x \to \frac{R (z)}{z} = \frac{R (x)}{x}$
218	217	fveq2d	$⊢ z = x \to \|\frac{R (z)}{z}\| = \|\frac{R (x)}{x}\|$
219	218	breq1d	$⊢ z = x \to (\|\frac{R (z)}{z}\| \leq t \leftrightarrow \|\frac{R (x)}{x}\| \leq t)$
220	219	cbvralvw	$⊢ \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \leftrightarrow \forall x \in [y, +∞) \|\frac{R (x)}{x}\| \leq t$
221		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
222	221	ad2antll	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to x \in ℝ$
223		simprl	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to y \leq x$
224		simplr	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to y \in ℝ^{+}$
225	224	rpred	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to y \in ℝ$
226		elicopnf	$⊢ y \in ℝ \to (x \in [y, +∞) \leftrightarrow (x \in ℝ \land y \leq x))$
227	225 226	syl	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (x \in [y, +∞) \leftrightarrow (x \in ℝ \land y \leq x))$
228	222 223 227	mpbir2and	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to x \in [y, +∞)$
229	1	pntrval	$⊢ x \in ℝ^{+} \to R (x) = ψ (x) - x$
230	229	ad2antll	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to R (x) = ψ (x) - x$
231	230	oveq1d	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to \frac{R (x)}{x} = \frac{ψ (x) - x}{x}$
232		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
233	222 232	syl	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to ψ (x) \in ℝ$
234	233	recnd	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to ψ (x) \in ℂ$
235		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
236	235	ad2antll	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to x \in ℂ$
237		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
238	237	ad2antll	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to x \neq 0$
239	234 236 236 238	divsubdird	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to \frac{ψ (x) - x}{x} = (\frac{ψ (x)}{x}) - (\frac{x}{x})$
240	236 238	dividd	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to \frac{x}{x} = 1$
241	240	oveq2d	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (\frac{ψ (x)}{x}) - (\frac{x}{x}) = (\frac{ψ (x)}{x}) - 1$
242	231 239 241	3eqtrrd	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (\frac{ψ (x)}{x}) - 1 = \frac{R (x)}{x}$
243	242	fveq2d	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to \|(\frac{ψ (x)}{x}) - 1\| = \|\frac{R (x)}{x}\|$
244	243	breq1d	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (\|(\frac{ψ (x)}{x}) - 1\| \leq t \leftrightarrow \|\frac{R (x)}{x}\| \leq t)$
245		simprr	$⊢ ((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \to \neg s \leq t$
246	245	ad2antrr	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to \neg s \leq t$
247	31	ad2antrr	$⊢ ((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \to [0, A] \subseteq ℝ$
248	247	ad2antrr	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to [0, A] \subseteq ℝ$
249		simplrl	$⊢ (((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \to t \in [0, A]$
250	249	adantr	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to t \in [0, A]$
251	248 250	sseldd	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to t \in ℝ$
252		simp-4r	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to s \in ℝ^{+}$
253	252	rpred	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to s \in ℝ$
254	251 253	ltnled	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (t < s \leftrightarrow \neg s \leq t)$
255	246 254	mpbird	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to t < s$
256	221 232	syl	$⊢ x \in ℝ^{+} \to ψ (x) \in ℝ$
257		rerpdivcl	$⊢ (ψ (x) \in ℝ \land x \in ℝ^{+}) \to \frac{ψ (x)}{x} \in ℝ$
258	256 257	mpancom	$⊢ x \in ℝ^{+} \to \frac{ψ (x)}{x} \in ℝ$
259	258	ad2antll	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to \frac{ψ (x)}{x} \in ℝ$
260		resubcl	$⊢ (\frac{ψ (x)}{x} \in ℝ \land 1 \in ℝ) \to (\frac{ψ (x)}{x}) - 1 \in ℝ$
261	259 45 260	sylancl	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (\frac{ψ (x)}{x}) - 1 \in ℝ$
262	261	recnd	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (\frac{ψ (x)}{x}) - 1 \in ℂ$
263	262	abscld	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to \|(\frac{ψ (x)}{x}) - 1\| \in ℝ$
264		lelttr	$⊢ (\|(\frac{ψ (x)}{x}) - 1\| \in ℝ \land t \in ℝ \land s \in ℝ) \to ((\|(\frac{ψ (x)}{x}) - 1\| \leq t \land t < s) \to \|(\frac{ψ (x)}{x}) - 1\| < s)$
265	263 251 253 264	syl3anc	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to ((\|(\frac{ψ (x)}{x}) - 1\| \leq t \land t < s) \to \|(\frac{ψ (x)}{x}) - 1\| < s)$
266	255 265	mpan2d	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (\|(\frac{ψ (x)}{x}) - 1\| \leq t \to \|(\frac{ψ (x)}{x}) - 1\| < s)$
267	244 266	sylbird	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to (\|\frac{R (x)}{x}\| \leq t \to \|(\frac{ψ (x)}{x}) - 1\| < s)$
268	228 267	embantd	$⊢ ((((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \land (y \leq x \land x \in ℝ^{+})) \to ((x \in [y, +∞) \to \|\frac{R (x)}{x}\| \leq t) \to \|(\frac{ψ (x)}{x}) - 1\| < s)$
269	268	exp32	$⊢ (((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \to (y \leq x \to (x \in ℝ^{+} \to ((x \in [y, +∞) \to \|\frac{R (x)}{x}\| \leq t) \to \|(\frac{ψ (x)}{x}) - 1\| < s)))$
270	269	com24	$⊢ (((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \to ((x \in [y, +∞) \to \|\frac{R (x)}{x}\| \leq t) \to (x \in ℝ^{+} \to (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s)))$
271	270	ralimdv2	$⊢ (((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \to (\forall x \in [y, +∞) \|\frac{R (x)}{x}\| \leq t \to \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
272	220 271	biimtrid	$⊢ (((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \land y \in ℝ^{+}) \to (\forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
273	272	reximdva	$⊢ ((φ \land s \in ℝ^{+}) \land (t \in [0, A] \land \neg s \leq t)) \to (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to \exists y \in ℝ^{+} \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
274	273	anassrs	$⊢ (((φ \land s \in ℝ^{+}) \land t \in [0, A]) \land \neg s \leq t) \to (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \to \exists y \in ℝ^{+} \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
275	274	impancom	$⊢ (((φ \land s \in ℝ^{+}) \land t \in [0, A]) \land \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t) \to (\neg s \leq t \to \exists y \in ℝ^{+} \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
276	275	expimpd	$⊢ ((φ \land s \in ℝ^{+}) \land t \in [0, A]) \to ((\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \land \neg s \leq t) \to \exists y \in ℝ^{+} \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
277	276	rexlimdva	$⊢ (φ \land s \in ℝ^{+}) \to (\exists t \in [0, A] (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \land \neg s \leq t) \to \exists y \in ℝ^{+} \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
278	214 277	mpd	$⊢ (φ \land s \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s)$
279		ssrexv	$⊢ ℝ^{+} \subseteq ℝ \to (\exists y \in ℝ^{+} \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s) \to \exists y \in ℝ \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
280	7 278 279	mpsyl	$⊢ (φ \land s \in ℝ^{+}) \to \exists y \in ℝ \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s)$
281	280	ralrimiva	$⊢ φ \to \forall s \in ℝ^{+} \exists y \in ℝ \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s)$
282	258	recnd	$⊢ x \in ℝ^{+} \to \frac{ψ (x)}{x} \in ℂ$
283	282	rgen	$⊢ \forall x \in ℝ^{+} \frac{ψ (x)}{x} \in ℂ$
284	283	a1i	$⊢ φ \to \forall x \in ℝ^{+} \frac{ψ (x)}{x} \in ℂ$
285	7	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
286		1cnd	$⊢ φ \to 1 \in ℂ$
287	284 285 286	rlim2	$⊢ φ \to ((x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1 \leftrightarrow \forall s \in ℝ^{+} \exists y \in ℝ \forall x \in ℝ^{+} (y \leq x \to \|(\frac{ψ (x)}{x}) - 1\| < s))$
288	281 287	mpbird	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$

Metamath Proof Explorer

Theorem pntlem3

Proof