pntleml

Description: Lemma for pnt . Equation 10.6.35 in Shapiro, p. 436. (Contributed by Mario Carneiro, 14-Apr-2016)

	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$
	pntlemp.b	$⊢ φ \to B \in ℝ^{+}$
	pntlemp.l	$⊢ φ \to L \in (0, 1)$
	pntlemp.d	$⊢ D = A + 1$
	pntlemp.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
	pntlemp.K	$⊢ φ \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{B}{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)$
Assertion	pntleml	$⊢ φ \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		pntlemp.b	$⊢ φ \to B \in ℝ^{+}$
5		pntlemp.l	$⊢ φ \to L \in (0, 1)$
6		pntlemp.d	$⊢ D = A + 1$
7		pntlemp.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
8		pntlemp.K	$⊢ φ \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{B}{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)$
9		eqid	$⊢ \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\} = \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}$
10	1 2 4 5 6 7	pntlemd	$⊢ φ \to (L \in ℝ^{+} \land D \in ℝ^{+} \land F \in ℝ^{+})$
11	10	simp3d	$⊢ φ \to F \in ℝ^{+}$
12		0m0e0	$⊢ 0 - 0 = 0$
13		simpr	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to r = 0$
14	13	oveq1d	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to r^{3} = 0^{3}$
15		3nn	$⊢ 3 \in ℕ$
16		0exp	$⊢ 3 \in ℕ \to 0^{3} = 0$
17	15 16	ax-mp	$⊢ 0^{3} = 0$
18	14 17	eqtrdi	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to r^{3} = 0$
19	18	oveq2d	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to F r^{3} = F \cdot 0$
20	11	rpcnd	$⊢ φ \to F \in ℂ$
21	20	mul01d	$⊢ φ \to F \cdot 0 = 0$
22	21	ad2antrr	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to F \cdot 0 = 0$
23	19 22	eqtrd	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to F r^{3} = 0$
24	13 23	oveq12d	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to r - F r^{3} = 0 - 0$
25	12 24 13	3eqtr4a	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to r - F r^{3} = r$
26		simplr	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}$
27	25 26	eqeltrd	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r = 0) \to r - F r^{3} \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}$
28		oveq1	$⊢ y = s \to [y, +∞) = [s, +∞)$
29	28	raleqdv	$⊢ y = s \to (\forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r \leftrightarrow \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)$
30	29	cbvrexvw	$⊢ \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r \leftrightarrow \exists s \in ℝ^{+} \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r$
31		simplrr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r \in [0, A]$
32		0re	$⊢ 0 \in ℝ$
33	2	ad2antrr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to A \in ℝ^{+}$
34	33	rpred	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to A \in ℝ$
35		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (r \in [0, A] \leftrightarrow (r \in ℝ \land 0 \leq r \land r \leq A))$
36	32 34 35	sylancr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to (r \in [0, A] \leftrightarrow (r \in ℝ \land 0 \leq r \land r \leq A))$
37	31 36	mpbid	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to (r \in ℝ \land 0 \leq r \land r \leq A)$
38	37	simp1d	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r \in ℝ$
39	11	ad2antrr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to F \in ℝ^{+}$
40	37	simp2d	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to 0 \leq r$
41		simplrl	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r \neq 0$
42	38 40 41	ne0gt0d	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to 0 < r$
43	38 42	elrpd	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r \in ℝ^{+}$
44		3z	$⊢ 3 \in ℤ$
45		rpexpcl	$⊢ (r \in ℝ^{+} \land 3 \in ℤ) \to r^{3} \in ℝ^{+}$
46	43 44 45	sylancl	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r^{3} \in ℝ^{+}$
47	39 46	rpmulcld	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to F r^{3} \in ℝ^{+}$
48	47	rpred	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to F r^{3} \in ℝ$
49	38 48	resubcld	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r - F r^{3} \in ℝ$
50	3	ad2antrr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
51	4	ad2antrr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to B \in ℝ^{+}$
52	5	ad2antrr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to L \in (0, 1)$
53	8	ad2antrr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{B}{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)$
54	37	simp3d	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r \leq A$
55		eqid	$⊢ \frac{r}{D} = \frac{r}{D}$
56		eqid	$⊢ e^{\frac{B}{\frac{r}{D}}} = e^{\frac{B}{\frac{r}{D}}}$
57		simprl	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to s \in ℝ^{+}$
58		1rp	$⊢ 1 \in ℝ^{+}$
59		rpaddcl	$⊢ (s \in ℝ^{+} \land 1 \in ℝ^{+}) \to s + 1 \in ℝ^{+}$
60	57 58 59	sylancl	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to s + 1 \in ℝ^{+}$
61	57	rpge0d	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to 0 \leq s$
62		1re	$⊢ 1 \in ℝ$
63	57	rpred	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to s \in ℝ$
64		addge02	$⊢ (1 \in ℝ \land s \in ℝ) \to (0 \leq s \leftrightarrow 1 \leq s + 1)$
65	62 63 64	sylancr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to (0 \leq s \leftrightarrow 1 \leq s + 1)$
66	61 65	mpbid	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to 1 \leq s + 1$
67	60 66	jca	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to (s + 1 \in ℝ^{+} \land 1 \leq s + 1)$
68	57	rpxrd	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to s \in ℝ^{*}$
69	63	lep1d	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to s \leq s + 1$
70		df-ico	$⊢ [.) = (t \in ℝ^{}, r \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (t \leq w \land w < r)\})$
71		xrletr	$⊢ (s \in ℝ^{} \land s + 1 \in ℝ^{} \land v \in ℝ^{*}) \to ((s \leq s + 1 \land s + 1 \leq v) \to s \leq v)$
72	70 70 71	ixxss1	$⊢ (s \in ℝ^{*} \land s \leq s + 1) \to [s + 1, +∞) \subseteq [s, +∞)$
73	68 69 72	syl2anc	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to [s + 1, +∞) \subseteq [s, +∞)$
74		simprr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r$
75		ssralv	$⊢ [s + 1, +∞) \subseteq [s, +∞) \to (\forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r \to \forall z \in [s + 1, +∞) \|\frac{R (z)}{z}\| \leq r)$
76	73 74 75	sylc	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to \forall z \in [s + 1, +∞) \|\frac{R (z)}{z}\| \leq r$
77	1 33 50 51 52 6 7 53 43 54 55 56 67 76	pntlemp	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3}$
78		rpre	$⊢ w \in ℝ^{+} \to w \in ℝ$
79	78	adantl	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to w \in ℝ$
80	79	leidd	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to w \leq w$
81		elicopnf	$⊢ w \in ℝ \to (w \in [w, +∞) \leftrightarrow (w \in ℝ \land w \leq w))$
82	79 81	syl	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to (w \in [w, +∞) \leftrightarrow (w \in ℝ \land w \leq w))$
83	79 80 82	mpbir2and	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to w \in [w, +∞)$
84		fveq2	$⊢ v = w \to R (v) = R (w)$
85		id	$⊢ v = w \to v = w$
86	84 85	oveq12d	$⊢ v = w \to \frac{R (v)}{v} = \frac{R (w)}{w}$
87	86	fveq2d	$⊢ v = w \to \|\frac{R (v)}{v}\| = \|\frac{R (w)}{w}\|$
88	87	breq1d	$⊢ v = w \to (\|\frac{R (v)}{v}\| \leq r - F r^{3} \leftrightarrow \|\frac{R (w)}{w}\| \leq r - F r^{3})$
89	88	rspcv	$⊢ w \in [w, +∞) \to (\forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3} \to \|\frac{R (w)}{w}\| \leq r - F r^{3})$
90	83 89	syl	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to (\forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3} \to \|\frac{R (w)}{w}\| \leq r - F r^{3})$
91	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
92	91	ffvelcdmi	$⊢ w \in ℝ^{+} \to R (w) \in ℝ$
93		rerpdivcl	$⊢ (R (w) \in ℝ \land w \in ℝ^{+}) \to \frac{R (w)}{w} \in ℝ$
94	92 93	mpancom	$⊢ w \in ℝ^{+} \to \frac{R (w)}{w} \in ℝ$
95	94	adantl	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to \frac{R (w)}{w} \in ℝ$
96	95	recnd	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to \frac{R (w)}{w} \in ℂ$
97	96	absge0d	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to 0 \leq \|\frac{R (w)}{w}\|$
98	96	abscld	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to \|\frac{R (w)}{w}\| \in ℝ$
99	49	adantr	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to r - F r^{3} \in ℝ$
100		letr	$⊢ (0 \in ℝ \land \|\frac{R (w)}{w}\| \in ℝ \land r - F r^{3} \in ℝ) \to ((0 \leq \|\frac{R (w)}{w}\| \land \|\frac{R (w)}{w}\| \leq r - F r^{3}) \to 0 \leq r - F r^{3})$
101	32 98 99 100	mp3an2i	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to ((0 \leq \|\frac{R (w)}{w}\| \land \|\frac{R (w)}{w}\| \leq r - F r^{3}) \to 0 \leq r - F r^{3})$
102	97 101	mpand	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to (\|\frac{R (w)}{w}\| \leq r - F r^{3} \to 0 \leq r - F r^{3})$
103	90 102	syld	$⊢ (((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \land w \in ℝ^{+}) \to (\forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3} \to 0 \leq r - F r^{3})$
104	103	rexlimdva	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to (\exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3} \to 0 \leq r - F r^{3})$
105	77 104	mpd	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to 0 \leq r - F r^{3}$
106	47	rpge0d	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to 0 \leq F r^{3}$
107	38 48	subge02d	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to (0 \leq F r^{3} \leftrightarrow r - F r^{3} \leq r)$
108	106 107	mpbid	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r - F r^{3} \leq r$
109	49 38 34 108 54	letrd	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r - F r^{3} \leq A$
110		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (r - F r^{3} \in [0, A] \leftrightarrow (r - F r^{3} \in ℝ \land 0 \leq r - F r^{3} \land r - F r^{3} \leq A))$
111	32 34 110	sylancr	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to (r - F r^{3} \in [0, A] \leftrightarrow (r - F r^{3} \in ℝ \land 0 \leq r - F r^{3} \land r - F r^{3} \leq A))$
112	49 105 109 111	mpbir3and	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to r - F r^{3} \in [0, A]$
113	112 77	jca	$⊢ ((φ \land (r \neq 0 \land r \in [0, A])) \land (s \in ℝ^{+} \land \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r)) \to (r - F r^{3} \in [0, A] \land \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3})$
114	113	rexlimdvaa	$⊢ (φ \land (r \neq 0 \land r \in [0, A])) \to (\exists s \in ℝ^{+} \forall z \in [s, +∞) \|\frac{R (z)}{z}\| \leq r \to (r - F r^{3} \in [0, A] \land \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3}))$
115	30 114	biimtrid	$⊢ (φ \land (r \neq 0 \land r \in [0, A])) \to (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r \to (r - F r^{3} \in [0, A] \land \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3}))$
116	115	anassrs	$⊢ ((φ \land r \neq 0) \land r \in [0, A]) \to (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r \to (r - F r^{3} \in [0, A] \land \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3}))$
117	116	expimpd	$⊢ (φ \land r \neq 0) \to ((r \in [0, A] \land \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r) \to (r - F r^{3} \in [0, A] \land \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3}))$
118		breq2	$⊢ t = r \to (\|\frac{R (z)}{z}\| \leq t \leftrightarrow \|\frac{R (z)}{z}\| \leq r)$
119	118	rexralbidv	$⊢ t = r \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 r)$
120	119	elrab	$⊢ r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\} \leftrightarrow (r \in [0, A] \land \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r)$
121		breq2	$⊢ t = r - F r^{3} \to (\|\frac{R (z)}{z}\| \leq t \leftrightarrow \|\frac{R (z)}{z}\| \leq r - F r^{3})$
122	121	rexralbidv	$⊢ t = r - F r^{3} \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 r - F r^{3})$
123		fveq2	$⊢ v = z \to R (v) = R (z)$
124		id	$⊢ v = z \to v = z$
125	123 124	oveq12d	$⊢ v = z \to \frac{R (v)}{v} = \frac{R (z)}{z}$
126	125	fveq2d	$⊢ v = z \to \|\frac{R (v)}{v}\| = \|\frac{R (z)}{z}\|$
127	126	breq1d	$⊢ v = z \to (\|\frac{R (v)}{v}\| \leq r - F r^{3} \leftrightarrow \|\frac{R (z)}{z}\| \leq r - F r^{3})$
128	127	cbvralvw	$⊢ \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3} \leftrightarrow \forall z \in [w, +∞) \|\frac{R (z)}{z}\| \leq r - F r^{3}$
129		oveq1	$⊢ w = y \to [w, +∞) = [y, +∞)$
130	129	raleqdv	$⊢ w = y \to (\forall z \in [w, +∞) \|\frac{R (z)}{z}\| \leq r - F r^{3} \leftrightarrow \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r - F r^{3})$
131	128 130	bitrid	$⊢ w = y \to (\forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3} \leftrightarrow \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r - F r^{3})$
132	131	cbvrexvw	$⊢ \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3} \leftrightarrow \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq r - F r^{3}$
133	122 132	bitr4di	$⊢ t = r - F r^{3} \to (\exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t \leftrightarrow \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3})$
134	133	elrab	$⊢ r - F r^{3} \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\} \leftrightarrow (r - F r^{3} \in [0, A] \land \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq r - F r^{3})$
135	117 120 134	3imtr4g	$⊢ (φ \land r \neq 0) \to (r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\} \to r - F r^{3} \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\})$
136	135	imp	$⊢ ((φ \land r \neq 0) \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \to r - F r^{3} \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}$
137	136	an32s	$⊢ ((φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \land r \neq 0) \to r - F r^{3} \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}$
138	27 137	pm2.61dane	$⊢ (φ \land r \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}) \to r - F r^{3} \in \{t \in [0, A] \| \exists y \in ℝ^{+} \forall z \in [y, +∞) \|\frac{R (z)}{z}\| \leq t\}$
139	1 2 3 9 11 138	pntlem3	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$

Metamath Proof Explorer

Theorem pntleml

Proof