rlimcnp

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypotheses	rlimcnp.a	$⊢ φ \to A \subseteq [0, +∞)$
	rlimcnp.0	$⊢ φ \to 0 \in A$
	rlimcnp.b	$⊢ φ \to B \subseteq ℝ^{+}$
	rlimcnp.r	$⊢ (φ \land x \in A) \to R \in ℂ$
	rlimcnp.d	$⊢ (φ \land x \in ℝ^{+}) \to (x \in A \leftrightarrow \frac{1}{x} \in B)$
	rlimcnp.c	$⊢ x = 0 \to R = C$
	rlimcnp.s	$⊢ x = \frac{1}{y} \to R = S$
	rlimcnp.j	$⊢ J = TopOpen (ℂ_{fld})$
	rlimcnp.k	$⊢ K = J ↾_{𝑡} A$
Assertion	rlimcnp	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ R) \in (K CnP J) (0))$

Proof

Step	Hyp	Ref	Expression
1		rlimcnp.a	$⊢ φ \to A \subseteq [0, +∞)$
2		rlimcnp.0	$⊢ φ \to 0 \in A$
3		rlimcnp.b	$⊢ φ \to B \subseteq ℝ^{+}$
4		rlimcnp.r	$⊢ (φ \land x \in A) \to R \in ℂ$
5		rlimcnp.d	$⊢ (φ \land x \in ℝ^{+}) \to (x \in A \leftrightarrow \frac{1}{x} \in B)$
6		rlimcnp.c	$⊢ x = 0 \to R = C$
7		rlimcnp.s	$⊢ x = \frac{1}{y} \to R = S$
8		rlimcnp.j	$⊢ J = TopOpen (ℂ_{fld})$
9		rlimcnp.k	$⊢ K = J ↾_{𝑡} A$
10		rpreccl	$⊢ r \in ℝ^{+} \to \frac{1}{r} \in ℝ^{+}$
11	10	adantl	$⊢ (φ \land r \in ℝ^{+}) \to \frac{1}{r} \in ℝ^{+}$
12		rpreccl	$⊢ t \in ℝ^{+} \to \frac{1}{t} \in ℝ^{+}$
13		rpcnne0	$⊢ t \in ℝ^{+} \to (t \in ℂ \land t \neq 0)$
14	13	adantl	$⊢ (φ \land t \in ℝ^{+}) \to (t \in ℂ \land t \neq 0)$
15		recrec	$⊢ (t \in ℂ \land t \neq 0) \to \frac{1}{\frac{1}{t}} = t$
16	14 15	syl	$⊢ (φ \land t \in ℝ^{+}) \to \frac{1}{\frac{1}{t}} = t$
17	16	eqcomd	$⊢ (φ \land t \in ℝ^{+}) \to t = \frac{1}{\frac{1}{t}}$
18		oveq2	$⊢ r = \frac{1}{t} \to \frac{1}{r} = \frac{1}{\frac{1}{t}}$
19	18	rspceeqv	$⊢ (\frac{1}{t} \in ℝ^{+} \land t = \frac{1}{\frac{1}{t}}) \to \exists r \in ℝ^{+} t = \frac{1}{r}$
20	12 17 19	syl2an2	$⊢ (φ \land t \in ℝ^{+}) \to \exists r \in ℝ^{+} t = \frac{1}{r}$
21		simpr	$⊢ (φ \land t = \frac{1}{r}) \to t = \frac{1}{r}$
22	21	breq1d	$⊢ (φ \land t = \frac{1}{r}) \to (t < y \leftrightarrow \frac{1}{r} < y)$
23	22	imbi1d	$⊢ (φ \land t = \frac{1}{r}) \to ((t < y \to \|S - C\| < z) \leftrightarrow (\frac{1}{r} < y \to \|S - C\| < z))$
24	23	ralbidv	$⊢ (φ \land t = \frac{1}{r}) \to (\forall y \in B (t < y \to \|S - C\| < z) \leftrightarrow \forall y \in B (\frac{1}{r} < y \to \|S - C\| < z))$
25	11 20 24	rexxfrd	$⊢ φ \to (\exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \leftrightarrow \exists r \in ℝ^{+} \forall y \in B (\frac{1}{r} < y \to \|S - C\| < z))$
26	25	adantr	$⊢ (φ \land z \in ℝ^{+}) \to (\exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \leftrightarrow \exists r \in ℝ^{+} \forall y \in B (\frac{1}{r} < y \to \|S - C\| < z))$
27		simplr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in B) \to r \in ℝ^{+}$
28	3	sselda	$⊢ (φ \land y \in B) \to y \in ℝ^{+}$
29	28	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in B) \to y \in ℝ^{+}$
30		elrp	$⊢ r \in ℝ^{+} \leftrightarrow (r \in ℝ \land 0 < r)$
31		elrp	$⊢ y \in ℝ^{+} \leftrightarrow (y \in ℝ \land 0 < y)$
32		ltrec1	$⊢ ((r \in ℝ \land 0 < r) \land (y \in ℝ \land 0 < y)) \to (\frac{1}{r} < y \leftrightarrow \frac{1}{y} < r)$
33	30 31 32	syl2anb	$⊢ (r \in ℝ^{+} \land y \in ℝ^{+}) \to (\frac{1}{r} < y \leftrightarrow \frac{1}{y} < r)$
34	27 29 33	syl2anc	$⊢ ((φ \land r \in ℝ^{+}) \land y \in B) \to (\frac{1}{r} < y \leftrightarrow \frac{1}{y} < r)$
35	34	imbi1d	$⊢ ((φ \land r \in ℝ^{+}) \land y \in B) \to ((\frac{1}{r} < y \to \|S - C\| < z) \leftrightarrow (\frac{1}{y} < r \to \|S - C\| < z))$
36	35	ralbidva	$⊢ (φ \land r \in ℝ^{+}) \to (\forall y \in B (\frac{1}{r} < y \to \|S - C\| < z) \leftrightarrow \forall y \in B (\frac{1}{y} < r \to \|S - C\| < z))$
37	36	adantlr	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to (\forall y \in B (\frac{1}{r} < y \to \|S - C\| < z) \leftrightarrow \forall y \in B (\frac{1}{y} < r \to \|S - C\| < z))$
38		rpcn	$⊢ y \in ℝ^{+} \to y \in ℂ$
39		rpne0	$⊢ y \in ℝ^{+} \to y \neq 0$
40	38 39	recrecd	$⊢ y \in ℝ^{+} \to \frac{1}{\frac{1}{y}} = y$
41	28 40	syl	$⊢ (φ \land y \in B) \to \frac{1}{\frac{1}{y}} = y$
42		simpr	$⊢ (φ \land y \in B) \to y \in B$
43	41 42	eqeltrd	$⊢ (φ \land y \in B) \to \frac{1}{\frac{1}{y}} \in B$
44		eleq1	$⊢ x = \frac{1}{y} \to (x \in A \leftrightarrow \frac{1}{y} \in A)$
45		oveq2	$⊢ x = \frac{1}{y} \to \frac{1}{x} = \frac{1}{\frac{1}{y}}$
46	45	eleq1d	$⊢ x = \frac{1}{y} \to (\frac{1}{x} \in B \leftrightarrow \frac{1}{\frac{1}{y}} \in B)$
47	44 46	bibi12d	$⊢ x = \frac{1}{y} \to ((x \in A \leftrightarrow \frac{1}{x} \in B) \leftrightarrow (\frac{1}{y} \in A \leftrightarrow \frac{1}{\frac{1}{y}} \in B))$
48	5	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} (x \in A \leftrightarrow \frac{1}{x} \in B)$
49	48	adantr	$⊢ (φ \land y \in B) \to \forall x \in ℝ^{+} (x \in A \leftrightarrow \frac{1}{x} \in B)$
50	28	rpreccld	$⊢ (φ \land y \in B) \to \frac{1}{y} \in ℝ^{+}$
51	47 49 50	rspcdva	$⊢ (φ \land y \in B) \to (\frac{1}{y} \in A \leftrightarrow \frac{1}{\frac{1}{y}} \in B)$
52	43 51	mpbird	$⊢ (φ \land y \in B) \to \frac{1}{y} \in A$
53	50	rpne0d	$⊢ (φ \land y \in B) \to \frac{1}{y} \neq 0$
54		eldifsn	$⊢ \frac{1}{y} \in (A ∖ \{0\}) \leftrightarrow (\frac{1}{y} \in A \land \frac{1}{y} \neq 0)$
55	52 53 54	sylanbrc	$⊢ (φ \land y \in B) \to \frac{1}{y} \in (A ∖ \{0\})$
56		eldifi	$⊢ x \in (A ∖ \{0\}) \to x \in A$
57	56	adantl	$⊢ (φ \land x \in (A ∖ \{0\})) \to x \in A$
58		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
59	1	ssdifssd	$⊢ φ \to A ∖ \{0\} \subseteq [0, +∞)$
60	59	sselda	$⊢ (φ \land x \in (A ∖ \{0\})) \to x \in [0, +∞)$
61	58 60	sseldi	$⊢ (φ \land x \in (A ∖ \{0\})) \to x \in ℝ$
62		0re	$⊢ 0 \in ℝ$
63		pnfxr	$⊢ +∞ \in ℝ^{*}$
64		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (x \in [0, +∞) \leftrightarrow (x \in ℝ \land 0 \leq x \land x < +∞))$
65	62 63 64	mp2an	$⊢ x \in [0, +∞) \leftrightarrow (x \in ℝ \land 0 \leq x \land x < +∞)$
66	65	simp2bi	$⊢ x \in [0, +∞) \to 0 \leq x$
67	60 66	syl	$⊢ (φ \land x \in (A ∖ \{0\})) \to 0 \leq x$
68		eldifsni	$⊢ x \in (A ∖ \{0\}) \to x \neq 0$
69	68	adantl	$⊢ (φ \land x \in (A ∖ \{0\})) \to x \neq 0$
70	61 67 69	ne0gt0d	$⊢ (φ \land x \in (A ∖ \{0\})) \to 0 < x$
71	61 70	elrpd	$⊢ (φ \land x \in (A ∖ \{0\})) \to x \in ℝ^{+}$
72	71 5	syldan	$⊢ (φ \land x \in (A ∖ \{0\})) \to (x \in A \leftrightarrow \frac{1}{x} \in B)$
73	57 72	mpbid	$⊢ (φ \land x \in (A ∖ \{0\})) \to \frac{1}{x} \in B$
74		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
75		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
76	74 75	recrecd	$⊢ x \in ℝ^{+} \to \frac{1}{\frac{1}{x}} = x$
77	71 76	syl	$⊢ (φ \land x \in (A ∖ \{0\})) \to \frac{1}{\frac{1}{x}} = x$
78	77	eqcomd	$⊢ (φ \land x \in (A ∖ \{0\})) \to x = \frac{1}{\frac{1}{x}}$
79		oveq2	$⊢ y = \frac{1}{x} \to \frac{1}{y} = \frac{1}{\frac{1}{x}}$
80	79	rspceeqv	$⊢ (\frac{1}{x} \in B \land x = \frac{1}{\frac{1}{x}}) \to \exists y \in B x = \frac{1}{y}$
81	73 78 80	syl2anc	$⊢ (φ \land x \in (A ∖ \{0\})) \to \exists y \in B x = \frac{1}{y}$
82		breq1	$⊢ x = \frac{1}{y} \to (x < r \leftrightarrow \frac{1}{y} < r)$
83	7	fvoveq1d	$⊢ x = \frac{1}{y} \to \|R - C\| = \|S - C\|$
84	83	breq1d	$⊢ x = \frac{1}{y} \to (\|R - C\| < z \leftrightarrow \|S - C\| < z)$
85	82 84	imbi12d	$⊢ x = \frac{1}{y} \to ((x < r \to \|R - C\| < z) \leftrightarrow (\frac{1}{y} < r \to \|S - C\| < z))$
86	85	adantl	$⊢ (φ \land x = \frac{1}{y}) \to ((x < r \to \|R - C\| < z) \leftrightarrow (\frac{1}{y} < r \to \|S - C\| < z))$
87	55 81 86	ralxfrd	$⊢ φ \to (\forall x \in (A ∖ \{0\}) (x < r \to \|R - C\| < z) \leftrightarrow \forall y \in B (\frac{1}{y} < r \to \|S - C\| < z))$
88	87	ad2antrr	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to (\forall x \in (A ∖ \{0\}) (x < r \to \|R - C\| < z) \leftrightarrow \forall y \in B (\frac{1}{y} < r \to \|S - C\| < z))$
89	37 88	bitr4d	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to (\forall y \in B (\frac{1}{r} < y \to \|S - C\| < z) \leftrightarrow \forall x \in (A ∖ \{0\}) (x < r \to \|R - C\| < z))$
90		elsni	$⊢ x \in \{0\} \to x = 0$
91	90	adantl	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to x = 0$
92	91 6	syl	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to R = C$
93	92	oveq1d	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to R - C = C - C$
94	6	eleq1d	$⊢ x = 0 \to (R \in ℂ \leftrightarrow C \in ℂ)$
95	4	ralrimiva	$⊢ φ \to \forall x \in A R \in ℂ$
96	94 95 2	rspcdva	$⊢ φ \to C \in ℂ$
97	96	subidd	$⊢ φ \to C - C = 0$
98	97	ad2antrr	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to C - C = 0$
99	93 98	eqtrd	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to R - C = 0$
100	99	abs00bd	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to \|R - C\| = 0$
101		rpgt0	$⊢ z \in ℝ^{+} \to 0 < z$
102	101	ad2antlr	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to 0 < z$
103	100 102	eqbrtrd	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to \|R - C\| < z$
104	103	a1d	$⊢ ((φ \land z \in ℝ^{+}) \land x \in \{0\}) \to (x < r \to \|R - C\| < z)$
105	104	ralrimiva	$⊢ (φ \land z \in ℝ^{+}) \to \forall x \in \{0\} (x < r \to \|R - C\| < z)$
106	105	adantr	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to \forall x \in \{0\} (x < r \to \|R - C\| < z)$
107	106	biantrud	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to (\forall x \in (A ∖ \{0\}) (x < r \to \|R - C\| < z) \leftrightarrow (\forall x \in (A ∖ \{0\}) (x < r \to \|R - C\| < z) \land \forall x \in \{0\} (x < r \to \|R - C\| < z)))$
108		ralunb	$⊢ \forall x \in ((A ∖ \{0\}) \cup \{0\}) (x < r \to \|R - C\| < z) \leftrightarrow (\forall x \in (A ∖ \{0\}) (x < r \to \|R - C\| < z) \land \forall x \in \{0\} (x < r \to \|R - C\| < z))$
109	107 108	bitr4di	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to (\forall x \in (A ∖ \{0\}) (x < r \to \|R - C\| < z) \leftrightarrow \forall x \in ((A ∖ \{0\}) \cup \{0\}) (x < r \to \|R - C\| < z))$
110		undif1	$⊢ (A ∖ \{0\}) \cup \{0\} = A \cup \{0\}$
111	2	ad2antrr	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to 0 \in A$
112	111	snssd	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to \{0\} \subseteq A$
113		ssequn2	$⊢ \{0\} \subseteq A \leftrightarrow A \cup \{0\} = A$
114	112 113	sylib	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to A \cup \{0\} = A$
115	110 114	syl5eq	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to (A ∖ \{0\}) \cup \{0\} = A$
116	115	raleqdv	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to (\forall x \in ((A ∖ \{0\}) \cup \{0\}) (x < r \to \|R - C\| < z) \leftrightarrow \forall x \in A (x < r \to \|R - C\| < z))$
117	89 109 116	3bitrd	$⊢ ((φ \land z \in ℝ^{+}) \land r \in ℝ^{+}) \to (\forall y \in B (\frac{1}{r} < y \to \|S - C\| < z) \leftrightarrow \forall x \in A (x < r \to \|R - C\| < z))$
118	117	rexbidva	$⊢ (φ \land z \in ℝ^{+}) \to (\exists r \in ℝ^{+} \forall y \in B (\frac{1}{r} < y \to \|S - C\| < z) \leftrightarrow \exists r \in ℝ^{+} \forall x \in A (x < r \to \|R - C\| < z))$
119	26 118	bitrd	$⊢ (φ \land z \in ℝ^{+}) \to (\exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \leftrightarrow \exists r \in ℝ^{+} \forall x \in A (x < r \to \|R - C\| < z))$
120	119	ralbidva	$⊢ φ \to (\forall z \in ℝ^{+} \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \leftrightarrow \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall x \in A (x < r \to \|R - C\| < z))$
121		nfv	$⊢ Ⅎ x w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r$
122		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ R) (w)$
123		nfcv	$⊢ \underline{Ⅎ} x (abs \circ -)$
124		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ R) (0)$
125	122 123 124	nfov	$⊢ \underline{Ⅎ} x ((x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0))$
126		nfcv	$⊢ \underline{Ⅎ} x <$
127		nfcv	$⊢ \underline{Ⅎ} x z$
128	125 126 127	nfbr	$⊢ Ⅎ x (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z$
129	121 128	nfim	$⊢ Ⅎ x (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z)$
130		nfv	$⊢ Ⅎ w (x ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) < z)$
131		oveq1	$⊢ w = x \to w ({(abs \circ -) ↾}_{(A \times A)}) 0 = x ({(abs \circ -) ↾}_{(A \times A)}) 0$
132	131	breq1d	$⊢ w = x \to (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \leftrightarrow x ({(abs \circ -) ↾}_{(A \times A)}) 0 < r)$
133		fveq2	$⊢ w = x \to (x \in A ⟼ R) (w) = (x \in A ⟼ R) (x)$
134	133	oveq1d	$⊢ w = x \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) = (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0)$
135	134	breq1d	$⊢ w = x \to ((x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z \leftrightarrow (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) < z)$
136	132 135	imbi12d	$⊢ w = x \to ((w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z) \leftrightarrow (x ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) < z))$
137	129 130 136	cbvralw	$⊢ \forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z) \leftrightarrow \forall x \in A (x ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) < z)$
138		simpr	$⊢ (φ \land x \in A) \to x \in A$
139	2	adantr	$⊢ (φ \land x \in A) \to 0 \in A$
140	138 139	ovresd	$⊢ (φ \land x \in A) \to x ({(abs \circ -) ↾}_{(A \times A)}) 0 = x (abs \circ -) 0$
141	1 58	sstrdi	$⊢ φ \to A \subseteq ℝ$
142		ax-resscn	$⊢ ℝ \subseteq ℂ$
143	141 142	sstrdi	$⊢ φ \to A \subseteq ℂ$
144	143	sselda	$⊢ (φ \land x \in A) \to x \in ℂ$
145		0cnd	$⊢ (φ \land x \in A) \to 0 \in ℂ$
146		eqid	$⊢ abs \circ - = abs \circ -$
147	146	cnmetdval	$⊢ (x \in ℂ \land 0 \in ℂ) \to x (abs \circ -) 0 = \|x - 0\|$
148	144 145 147	syl2anc	$⊢ (φ \land x \in A) \to x (abs \circ -) 0 = \|x - 0\|$
149	144	subid1d	$⊢ (φ \land x \in A) \to x - 0 = x$
150	149	fveq2d	$⊢ (φ \land x \in A) \to \|x - 0\| = \|x\|$
151	140 148 150	3eqtrd	$⊢ (φ \land x \in A) \to x ({(abs \circ -) ↾}_{(A \times A)}) 0 = \|x\|$
152	141	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
153	1	sselda	$⊢ (φ \land x \in A) \to x \in [0, +∞)$
154	153 66	syl	$⊢ (φ \land x \in A) \to 0 \leq x$
155	152 154	absidd	$⊢ (φ \land x \in A) \to \|x\| = x$
156	151 155	eqtrd	$⊢ (φ \land x \in A) \to x ({(abs \circ -) ↾}_{(A \times A)}) 0 = x$
157	156	breq1d	$⊢ (φ \land x \in A) \to (x ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \leftrightarrow x < r)$
158		eqid	$⊢ (x \in A ⟼ R) = (x \in A ⟼ R)$
159	158	fvmpt2	$⊢ (x \in A \land R \in ℂ) \to (x \in A ⟼ R) (x) = R$
160	138 4 159	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ R) (x) = R$
161	96	adantr	$⊢ (φ \land x \in A) \to C \in ℂ$
162	158 6 139 161	fvmptd3	$⊢ (φ \land x \in A) \to (x \in A ⟼ R) (0) = C$
163	160 162	oveq12d	$⊢ (φ \land x \in A) \to (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) = R (abs \circ -) C$
164	146	cnmetdval	$⊢ (R \in ℂ \land C \in ℂ) \to R (abs \circ -) C = \|R - C\|$
165	4 161 164	syl2anc	$⊢ (φ \land x \in A) \to R (abs \circ -) C = \|R - C\|$
166	163 165	eqtrd	$⊢ (φ \land x \in A) \to (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) = \|R - C\|$
167	166	breq1d	$⊢ (φ \land x \in A) \to ((x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) < z \leftrightarrow \|R - C\| < z)$
168	157 167	imbi12d	$⊢ (φ \land x \in A) \to ((x ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) < z) \leftrightarrow (x < r \to \|R - C\| < z))$
169	168	ralbidva	$⊢ φ \to (\forall x \in A (x ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (x) (abs \circ -) (x \in A ⟼ R) (0) < z) \leftrightarrow \forall x \in A (x < r \to \|R - C\| < z))$
170	137 169	syl5bb	$⊢ φ \to (\forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z) \leftrightarrow \forall x \in A (x < r \to \|R - C\| < z))$
171	170	rexbidv	$⊢ φ \to (\exists r \in ℝ^{+} \forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z) \leftrightarrow \exists r \in ℝ^{+} \forall x \in A (x < r \to \|R - C\| < z))$
172	171	ralbidv	$⊢ φ \to (\forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z) \leftrightarrow \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall x \in A (x < r \to \|R - C\| < z))$
173	4	fmpttd	$⊢ φ \to (x \in A ⟼ R) : A ⟶ ℂ$
174	173	biantrurd	$⊢ φ \to (\forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z) \leftrightarrow ((x \in A ⟼ R) : A ⟶ ℂ \land \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z)))$
175	120 172 174	3bitr2d	$⊢ φ \to (\forall z \in ℝ^{+} \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \leftrightarrow ((x \in A ⟼ R) : A ⟶ ℂ \land \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z)))$
176	7	eleq1d	$⊢ x = \frac{1}{y} \to (R \in ℂ \leftrightarrow S \in ℂ)$
177	95	adantr	$⊢ (φ \land y \in B) \to \forall x \in A R \in ℂ$
178	176 177 52	rspcdva	$⊢ (φ \land y \in B) \to S \in ℂ$
179	178	ralrimiva	$⊢ φ \to \forall y \in B S \in ℂ$
180		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
181	3 180	sstrdi	$⊢ φ \to B \subseteq ℝ$
182		1red	$⊢ φ \to 1 \in ℝ$
183	179 181 96 182	rlim3	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow \forall z \in ℝ^{+} \exists t \in [1, +∞) \forall y \in B (t \leq y \to \|S - C\| < z))$
184		0xr	$⊢ 0 \in ℝ^{*}$
185		0lt1	$⊢ 0 < 1$
186		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
187		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
188		xrltletr	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land w \in ℝ^{*}) \to ((0 < 1 \land 1 \leq w) \to 0 < w)$
189	186 187 188	ixxss1	$⊢ (0 \in ℝ^{*} \land 0 < 1) \to [1, +∞) \subseteq (0, +∞)$
190	184 185 189	mp2an	$⊢ [1, +∞) \subseteq (0, +∞)$
191		ioorp	$⊢ (0, +∞) = ℝ^{+}$
192	190 191	sseqtri	$⊢ [1, +∞) \subseteq ℝ^{+}$
193		ssrexv	$⊢ [1, +∞) \subseteq ℝ^{+} \to (\exists t \in [1, +∞) \forall y \in B (t \leq y \to \|S - C\| < z) \to \exists t \in ℝ^{+} \forall y \in B (t \leq y \to \|S - C\| < z))$
194	192 193	ax-mp	$⊢ \exists t \in [1, +∞) \forall y \in B (t \leq y \to \|S - C\| < z) \to \exists t \in ℝ^{+} \forall y \in B (t \leq y \to \|S - C\| < z)$
195		simplr	$⊢ ((φ \land t \in ℝ^{+}) \land y \in B) \to t \in ℝ^{+}$
196	180 195	sseldi	$⊢ ((φ \land t \in ℝ^{+}) \land y \in B) \to t \in ℝ$
197	181	adantr	$⊢ (φ \land t \in ℝ^{+}) \to B \subseteq ℝ$
198	197	sselda	$⊢ ((φ \land t \in ℝ^{+}) \land y \in B) \to y \in ℝ$
199		ltle	$⊢ (t \in ℝ \land y \in ℝ) \to (t < y \to t \leq y)$
200	196 198 199	syl2anc	$⊢ ((φ \land t \in ℝ^{+}) \land y \in B) \to (t < y \to t \leq y)$
201	200	imim1d	$⊢ ((φ \land t \in ℝ^{+}) \land y \in B) \to ((t \leq y \to \|S - C\| < z) \to (t < y \to \|S - C\| < z))$
202	201	ralimdva	$⊢ (φ \land t \in ℝ^{+}) \to (\forall y \in B (t \leq y \to \|S - C\| < z) \to \forall y \in B (t < y \to \|S - C\| < z))$
203	202	reximdva	$⊢ φ \to (\exists t \in ℝ^{+} \forall y \in B (t \leq y \to \|S - C\| < z) \to \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z))$
204	194 203	syl5	$⊢ φ \to (\exists t \in [1, +∞) \forall y \in B (t \leq y \to \|S - C\| < z) \to \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z))$
205	204	ralimdv	$⊢ φ \to (\forall z \in ℝ^{+} \exists t \in [1, +∞) \forall y \in B (t \leq y \to \|S - C\| < z) \to \forall z \in ℝ^{+} \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z))$
206	183 205	sylbid	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \to \forall z \in ℝ^{+} \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z))$
207		ssrexv	$⊢ ℝ^{+} \subseteq ℝ \to (\exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \to \exists t \in ℝ \forall y \in B (t < y \to \|S - C\| < z))$
208	180 207	ax-mp	$⊢ \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \to \exists t \in ℝ \forall y \in B (t < y \to \|S - C\| < z)$
209	208	ralimi	$⊢ \forall z \in ℝ^{+} \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \to \forall z \in ℝ^{+} \exists t \in ℝ \forall y \in B (t < y \to \|S - C\| < z)$
210	179 181 96	rlim2lt	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow \forall z \in ℝ^{+} \exists t \in ℝ \forall y \in B (t < y \to \|S - C\| < z))$
211	209 210	syl5ibr	$⊢ φ \to (\forall z \in ℝ^{+} \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z) \to (y \in B ⟼ S) \underset{ℝ}{⇝} C)$
212	206 211	impbid	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow \forall z \in ℝ^{+} \exists t \in ℝ^{+} \forall y \in B (t < y \to \|S - C\| < z))$
213		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
214		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land A \subseteq ℂ) \to {(abs \circ -) ↾}_{(A \times A)} \in ∞Met (A)$
215	213 143 214	sylancr	$⊢ φ \to {(abs \circ -) ↾}_{(A \times A)} \in ∞Met (A)$
216	213	a1i	$⊢ φ \to abs \circ - \in ∞Met (ℂ)$
217		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{(A \times A)}) = MetOpen ({(abs \circ -) ↾}_{(A \times A)})$
218	8	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
219	217 218	metcnp2	$⊢ ({(abs \circ -) ↾}_{(A \times A)} \in ∞Met (A) \land abs \circ - \in ∞Met (ℂ) \land 0 \in A) \to ((x \in A ⟼ R) \in (MetOpen ({(abs \circ -) ↾}_{(A \times A)}) CnP J) (0) \leftrightarrow ((x \in A ⟼ R) : A ⟶ ℂ \land \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z)))$
220	215 216 2 219	syl3anc	$⊢ φ \to ((x \in A ⟼ R) \in (MetOpen ({(abs \circ -) ↾}_{(A \times A)}) CnP J) (0) \leftrightarrow ((x \in A ⟼ R) : A ⟶ ℂ \land \forall z \in ℝ^{+} \exists r \in ℝ^{+} \forall w \in A (w ({(abs \circ -) ↾}_{(A \times A)}) 0 < r \to (x \in A ⟼ R) (w) (abs \circ -) (x \in A ⟼ R) (0) < z)))$
221	175 212 220	3bitr4d	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ R) \in (MetOpen ({(abs \circ -) ↾}_{(A \times A)}) CnP J) (0))$
222		eqid	$⊢ {(abs \circ -) ↾}_{(A \times A)} = {(abs \circ -) ↾}_{(A \times A)}$
223	222 218 217	metrest	$⊢ (abs \circ - \in ∞Met (ℂ) \land A \subseteq ℂ) \to J ↾_{𝑡} A = MetOpen ({(abs \circ -) ↾}_{(A \times A)})$
224	213 143 223	sylancr	$⊢ φ \to J ↾_{𝑡} A = MetOpen ({(abs \circ -) ↾}_{(A \times A)})$
225	9 224	syl5eq	$⊢ φ \to K = MetOpen ({(abs \circ -) ↾}_{(A \times A)})$
226	225	oveq1d	$⊢ φ \to K CnP J = MetOpen ({(abs \circ -) ↾}_{(A \times A)}) CnP J$
227	226	fveq1d	$⊢ φ \to (K CnP J) (0) = (MetOpen ({(abs \circ -) ↾}_{(A \times A)}) CnP J) (0)$
228	227	eleq2d	$⊢ φ \to ((x \in A ⟼ R) \in (K CnP J) (0) \leftrightarrow (x \in A ⟼ R) \in (MetOpen ({(abs \circ -) ↾}_{(A \times A)}) CnP J) (0))$
229	221 228	bitr4d	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ R) \in (K CnP J) (0))$

Metamath Proof Explorer

Theorem rlimcnp

Proof