rlimcnp2

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	rlimcnp2.a	$⊢ φ \to A \subseteq [0, +∞)$
	rlimcnp2.0	$⊢ φ \to 0 \in A$
	rlimcnp2.b	$⊢ φ \to B \subseteq ℝ$
	rlimcnp2.c	$⊢ φ \to C \in ℂ$
	rlimcnp2.r	$⊢ (φ \land y \in B) \to S \in ℂ$
	rlimcnp2.d	$⊢ (φ \land y \in ℝ^{+}) \to (y \in B \leftrightarrow \frac{1}{y} \in A)$
	rlimcnp2.s	$⊢ y = \frac{1}{x} \to S = R$
	rlimcnp2.j	$⊢ J = TopOpen (ℂ_{fld})$
	rlimcnp2.k	$⊢ K = J ↾_{𝑡} A$
Assertion	rlimcnp2	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ if (x = 0, C, R)) \in (K CnP J) (0))$

Proof

Step	Hyp	Ref	Expression
1		rlimcnp2.a	$⊢ φ \to A \subseteq [0, +∞)$
2		rlimcnp2.0	$⊢ φ \to 0 \in A$
3		rlimcnp2.b	$⊢ φ \to B \subseteq ℝ$
4		rlimcnp2.c	$⊢ φ \to C \in ℂ$
5		rlimcnp2.r	$⊢ (φ \land y \in B) \to S \in ℂ$
6		rlimcnp2.d	$⊢ (φ \land y \in ℝ^{+}) \to (y \in B \leftrightarrow \frac{1}{y} \in A)$
7		rlimcnp2.s	$⊢ y = \frac{1}{x} \to S = R$
8		rlimcnp2.j	$⊢ J = TopOpen (ℂ_{fld})$
9		rlimcnp2.k	$⊢ K = J ↾_{𝑡} A$
10		inss1	$⊢ B \cap [1, +∞) \subseteq B$
11		resmpt	$⊢ B \cap [1, +∞) \subseteq B \to {(y \in B ⟼ S) ↾}_{(B \cap [1, +∞))} = (y \in (B \cap [1, +∞)) ⟼ S)$
12	10 11	mp1i	$⊢ φ \to {(y \in B ⟼ S) ↾}_{(B \cap [1, +∞))} = (y \in (B \cap [1, +∞)) ⟼ S)$
13		0xr	$⊢ 0 \in ℝ^{*}$
14		0lt1	$⊢ 0 < 1$
15		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
16		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
17		xrltletr	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land w \in ℝ^{*}) \to ((0 < 1 \land 1 \leq w) \to 0 < w)$
18	15 16 17	ixxss1	$⊢ (0 \in ℝ^{*} \land 0 < 1) \to [1, +∞) \subseteq (0, +∞)$
19	13 14 18	mp2an	$⊢ [1, +∞) \subseteq (0, +∞)$
20		ioorp	$⊢ (0, +∞) = ℝ^{+}$
21	19 20	sseqtri	$⊢ [1, +∞) \subseteq ℝ^{+}$
22		sslin	$⊢ [1, +∞) \subseteq ℝ^{+} \to B \cap [1, +∞) \subseteq B \cap ℝ^{+}$
23	21 22	ax-mp	$⊢ B \cap [1, +∞) \subseteq B \cap ℝ^{+}$
24		resmpt	$⊢ B \cap [1, +∞) \subseteq B \cap ℝ^{+} \to {(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{(B \cap [1, +∞))} = (y \in (B \cap [1, +∞)) ⟼ S)$
25	23 24	mp1i	$⊢ φ \to {(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{(B \cap [1, +∞))} = (y \in (B \cap [1, +∞)) ⟼ S)$
26	12 25	eqtr4d	$⊢ φ \to {(y \in B ⟼ S) ↾}_{(B \cap [1, +∞))} = {(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{(B \cap [1, +∞))}$
27		resres	$⊢ {({(y \in B ⟼ S) ↾}_{B}) ↾}_{[1, +∞)} = {(y \in B ⟼ S) ↾}_{(B \cap [1, +∞))}$
28		resres	$⊢ {({(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{B}) ↾}_{[1, +∞)} = {(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{(B \cap [1, +∞))}$
29	26 27 28	3eqtr4g	$⊢ φ \to {({(y \in B ⟼ S) ↾}_{B}) ↾}_{[1, +∞)} = {({(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{B}) ↾}_{[1, +∞)}$
30	5	fmpttd	$⊢ φ \to (y \in B ⟼ S) : B ⟶ ℂ$
31	30	ffnd	$⊢ φ \to (y \in B ⟼ S) Fn B$
32		fnresdm	$⊢ (y \in B ⟼ S) Fn B \to {(y \in B ⟼ S) ↾}_{B} = (y \in B ⟼ S)$
33	31 32	syl	$⊢ φ \to {(y \in B ⟼ S) ↾}_{B} = (y \in B ⟼ S)$
34	33	reseq1d	$⊢ φ \to {({(y \in B ⟼ S) ↾}_{B}) ↾}_{[1, +∞)} = {(y \in B ⟼ S) ↾}_{[1, +∞)}$
35		elinel1	$⊢ y \in (B \cap ℝ^{+}) \to y \in B$
36	35 5	sylan2	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to S \in ℂ$
37	36	fmpttd	$⊢ φ \to (y \in (B \cap ℝ^{+}) ⟼ S) : B \cap ℝ^{+} ⟶ ℂ$
38		frel	$⊢ (y \in (B \cap ℝ^{+}) ⟼ S) : B \cap ℝ^{+} ⟶ ℂ \to Rel (y \in (B \cap ℝ^{+}) ⟼ S)$
39	37 38	syl	$⊢ φ \to Rel (y \in (B \cap ℝ^{+}) ⟼ S)$
40		eqid	$⊢ (y \in (B \cap ℝ^{+}) ⟼ S) = (y \in (B \cap ℝ^{+}) ⟼ S)$
41	40 36	dmmptd	$⊢ φ \to dom (y \in (B \cap ℝ^{+}) ⟼ S) = B \cap ℝ^{+}$
42		inss1	$⊢ B \cap ℝ^{+} \subseteq B$
43	41 42	eqsstrdi	$⊢ φ \to dom (y \in (B \cap ℝ^{+}) ⟼ S) \subseteq B$
44		relssres	$⊢ (Rel (y \in (B \cap ℝ^{+}) ⟼ S) \land dom (y \in (B \cap ℝ^{+}) ⟼ S) \subseteq B) \to {(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{B} = (y \in (B \cap ℝ^{+}) ⟼ S)$
45	39 43 44	syl2anc	$⊢ φ \to {(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{B} = (y \in (B \cap ℝ^{+}) ⟼ S)$
46	45	reseq1d	$⊢ φ \to {({(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{B}) ↾}_{[1, +∞)} = {(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{[1, +∞)}$
47	29 34 46	3eqtr3d	$⊢ φ \to {(y \in B ⟼ S) ↾}_{[1, +∞)} = {(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{[1, +∞)}$
48	47	breq1d	$⊢ φ \to (({(y \in B ⟼ S) ↾}_{[1, +∞)}) \underset{ℝ}{⇝} C \leftrightarrow ({(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{[1, +∞)}) \underset{ℝ}{⇝} C)$
49		1red	$⊢ φ \to 1 \in ℝ$
50	30 3 49	rlimresb	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow ({(y \in B ⟼ S) ↾}_{[1, +∞)}) \underset{ℝ}{⇝} C)$
51	42 3	sstrid	$⊢ φ \to B \cap ℝ^{+} \subseteq ℝ$
52	37 51 49	rlimresb	$⊢ φ \to ((y \in (B \cap ℝ^{+}) ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow ({(y \in (B \cap ℝ^{+}) ⟼ S) ↾}_{[1, +∞)}) \underset{ℝ}{⇝} C)$
53	48 50 52	3bitr4d	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow (y \in (B \cap ℝ^{+}) ⟼ S) \underset{ℝ}{⇝} C)$
54		inss2	$⊢ B \cap ℝ^{+} \subseteq ℝ^{+}$
55	54	a1i	$⊢ φ \to B \cap ℝ^{+} \subseteq ℝ^{+}$
56	55	sselda	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to y \in ℝ^{+}$
57	56	rpreccld	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to \frac{1}{y} \in ℝ^{+}$
58	57	rpne0d	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to \frac{1}{y} \neq 0$
59	58	neneqd	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to \neg \frac{1}{y} = 0$
60	59	iffalsed	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to if (\frac{1}{y} = 0, C, ⦋ (\frac{1}{y}) / x ⦌ R) = ⦋ (\frac{1}{y}) / x ⦌ R$
61		oveq2	$⊢ x = \frac{1}{y} \to \frac{1}{x} = \frac{1}{\frac{1}{y}}$
62		rpcnne0	$⊢ y \in ℝ^{+} \to (y \in ℂ \land y \neq 0)$
63		recrec	$⊢ (y \in ℂ \land y \neq 0) \to \frac{1}{\frac{1}{y}} = y$
64	56 62 63	3syl	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to \frac{1}{\frac{1}{y}} = y$
65	61 64	sylan9eqr	$⊢ ((φ \land y \in (B \cap ℝ^{+})) \land x = \frac{1}{y}) \to \frac{1}{x} = y$
66	65	eqcomd	$⊢ ((φ \land y \in (B \cap ℝ^{+})) \land x = \frac{1}{y}) \to y = \frac{1}{x}$
67	66 7	syl	$⊢ ((φ \land y \in (B \cap ℝ^{+})) \land x = \frac{1}{y}) \to S = R$
68	67	eqcomd	$⊢ ((φ \land y \in (B \cap ℝ^{+})) \land x = \frac{1}{y}) \to R = S$
69	57 68	csbied	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to ⦋ (\frac{1}{y}) / x ⦌ R = S$
70	60 69	eqtrd	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to if (\frac{1}{y} = 0, C, ⦋ (\frac{1}{y}) / x ⦌ R) = S$
71	70	mpteq2dva	$⊢ φ \to (y \in (B \cap ℝ^{+}) ⟼ if (\frac{1}{y} = 0, C, ⦋ (\frac{1}{y}) / x ⦌ R)) = (y \in (B \cap ℝ^{+}) ⟼ S)$
72	71	breq1d	$⊢ φ \to ((y \in (B \cap ℝ^{+}) ⟼ if (\frac{1}{y} = 0, C, ⦋ (\frac{1}{y}) / x ⦌ R)) \underset{ℝ}{⇝} C \leftrightarrow (y \in (B \cap ℝ^{+}) ⟼ S) \underset{ℝ}{⇝} C)$
73	4	ad2antrr	$⊢ ((φ \land w \in A) \land w = 0) \to C \in ℂ$
74	1	sselda	$⊢ (φ \land w \in A) \to w \in [0, +∞)$
75		0re	$⊢ 0 \in ℝ$
76		pnfxr	$⊢ +∞ \in ℝ^{*}$
77		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (w \in [0, +∞) \leftrightarrow (w \in ℝ \land 0 \leq w \land w < +∞))$
78	75 76 77	mp2an	$⊢ w \in [0, +∞) \leftrightarrow (w \in ℝ \land 0 \leq w \land w < +∞)$
79	74 78	sylib	$⊢ (φ \land w \in A) \to (w \in ℝ \land 0 \leq w \land w < +∞)$
80	79	simp1d	$⊢ (φ \land w \in A) \to w \in ℝ$
81	80	adantr	$⊢ ((φ \land w \in A) \land \neg w = 0) \to w \in ℝ$
82	79	simp2d	$⊢ (φ \land w \in A) \to 0 \leq w$
83		leloe	$⊢ (0 \in ℝ \land w \in ℝ) \to (0 \leq w \leftrightarrow (0 < w \lor 0 = w))$
84	75 80 83	sylancr	$⊢ (φ \land w \in A) \to (0 \leq w \leftrightarrow (0 < w \lor 0 = w))$
85	82 84	mpbid	$⊢ (φ \land w \in A) \to (0 < w \lor 0 = w)$
86	85	ord	$⊢ (φ \land w \in A) \to (\neg 0 < w \to 0 = w)$
87		eqcom	$⊢ 0 = w \leftrightarrow w = 0$
88	86 87	imbitrdi	$⊢ (φ \land w \in A) \to (\neg 0 < w \to w = 0)$
89	88	con1d	$⊢ (φ \land w \in A) \to (\neg w = 0 \to 0 < w)$
90	89	imp	$⊢ ((φ \land w \in A) \land \neg w = 0) \to 0 < w$
91	81 90	elrpd	$⊢ ((φ \land w \in A) \land \neg w = 0) \to w \in ℝ^{+}$
92		rpcnne0	$⊢ w \in ℝ^{+} \to (w \in ℂ \land w \neq 0)$
93		recrec	$⊢ (w \in ℂ \land w \neq 0) \to \frac{1}{\frac{1}{w}} = w$
94	92 93	syl	$⊢ w \in ℝ^{+} \to \frac{1}{\frac{1}{w}} = w$
95	91 94	syl	$⊢ ((φ \land w \in A) \land \neg w = 0) \to \frac{1}{\frac{1}{w}} = w$
96	95	csbeq1d	$⊢ ((φ \land w \in A) \land \neg w = 0) \to ⦋ (\frac{1}{\frac{1}{w}}) / x ⦌ R = ⦋ w / x ⦌ R$
97		oveq2	$⊢ y = \frac{1}{w} \to \frac{1}{y} = \frac{1}{\frac{1}{w}}$
98	97	csbeq1d	$⊢ y = \frac{1}{w} \to ⦋ (\frac{1}{y}) / x ⦌ R = ⦋ (\frac{1}{\frac{1}{w}}) / x ⦌ R$
99	98	eleq1d	$⊢ y = \frac{1}{w} \to (⦋ (\frac{1}{y}) / x ⦌ R \in ℂ \leftrightarrow ⦋ (\frac{1}{\frac{1}{w}}) / x ⦌ R \in ℂ)$
100	69 36	eqeltrd	$⊢ (φ \land y \in (B \cap ℝ^{+})) \to ⦋ (\frac{1}{y}) / x ⦌ R \in ℂ$
101	100	ralrimiva	$⊢ φ \to \forall y \in (B \cap ℝ^{+}) ⦋ (\frac{1}{y}) / x ⦌ R \in ℂ$
102	101	ad2antrr	$⊢ ((φ \land w \in A) \land \neg w = 0) \to \forall y \in (B \cap ℝ^{+}) ⦋ (\frac{1}{y}) / x ⦌ R \in ℂ$
103		simplr	$⊢ ((φ \land w \in A) \land \neg w = 0) \to w \in A$
104		simpll	$⊢ ((φ \land w \in A) \land \neg w = 0) \to φ$
105		eleq1	$⊢ y = \frac{1}{w} \to (y \in B \leftrightarrow \frac{1}{w} \in B)$
106	97	eleq1d	$⊢ y = \frac{1}{w} \to (\frac{1}{y} \in A \leftrightarrow \frac{1}{\frac{1}{w}} \in A)$
107	105 106	bibi12d	$⊢ y = \frac{1}{w} \to ((y \in B \leftrightarrow \frac{1}{y} \in A) \leftrightarrow (\frac{1}{w} \in B \leftrightarrow \frac{1}{\frac{1}{w}} \in A))$
108	6	ralrimiva	$⊢ φ \to \forall y \in ℝ^{+} (y \in B \leftrightarrow \frac{1}{y} \in A)$
109	108	adantr	$⊢ (φ \land w \in ℝ^{+}) \to \forall y \in ℝ^{+} (y \in B \leftrightarrow \frac{1}{y} \in A)$
110		rpreccl	$⊢ w \in ℝ^{+} \to \frac{1}{w} \in ℝ^{+}$
111	110	adantl	$⊢ (φ \land w \in ℝ^{+}) \to \frac{1}{w} \in ℝ^{+}$
112	107 109 111	rspcdva	$⊢ (φ \land w \in ℝ^{+}) \to (\frac{1}{w} \in B \leftrightarrow \frac{1}{\frac{1}{w}} \in A)$
113	94	adantl	$⊢ (φ \land w \in ℝ^{+}) \to \frac{1}{\frac{1}{w}} = w$
114	113	eleq1d	$⊢ (φ \land w \in ℝ^{+}) \to (\frac{1}{\frac{1}{w}} \in A \leftrightarrow w \in A)$
115	112 114	bitr2d	$⊢ (φ \land w \in ℝ^{+}) \to (w \in A \leftrightarrow \frac{1}{w} \in B)$
116	104 91 115	syl2anc	$⊢ ((φ \land w \in A) \land \neg w = 0) \to (w \in A \leftrightarrow \frac{1}{w} \in B)$
117	103 116	mpbid	$⊢ ((φ \land w \in A) \land \neg w = 0) \to \frac{1}{w} \in B$
118	91	rpreccld	$⊢ ((φ \land w \in A) \land \neg w = 0) \to \frac{1}{w} \in ℝ^{+}$
119	117 118	elind	$⊢ ((φ \land w \in A) \land \neg w = 0) \to \frac{1}{w} \in (B \cap ℝ^{+})$
120	99 102 119	rspcdva	$⊢ ((φ \land w \in A) \land \neg w = 0) \to ⦋ (\frac{1}{\frac{1}{w}}) / x ⦌ R \in ℂ$
121	96 120	eqeltrrd	$⊢ ((φ \land w \in A) \land \neg w = 0) \to ⦋ w / x ⦌ R \in ℂ$
122	73 121	ifclda	$⊢ (φ \land w \in A) \to if (w = 0, C, ⦋ w / x ⦌ R) \in ℂ$
123	111	biantrud	$⊢ (φ \land w \in ℝ^{+}) \to (\frac{1}{w} \in B \leftrightarrow (\frac{1}{w} \in B \land \frac{1}{w} \in ℝ^{+}))$
124	115 123	bitrd	$⊢ (φ \land w \in ℝ^{+}) \to (w \in A \leftrightarrow (\frac{1}{w} \in B \land \frac{1}{w} \in ℝ^{+}))$
125		elin	$⊢ \frac{1}{w} \in (B \cap ℝ^{+}) \leftrightarrow (\frac{1}{w} \in B \land \frac{1}{w} \in ℝ^{+})$
126	124 125	bitr4di	$⊢ (φ \land w \in ℝ^{+}) \to (w \in A \leftrightarrow \frac{1}{w} \in (B \cap ℝ^{+}))$
127		iftrue	$⊢ w = 0 \to if (w = 0, C, ⦋ w / x ⦌ R) = C$
128		eqeq1	$⊢ w = \frac{1}{y} \to (w = 0 \leftrightarrow \frac{1}{y} = 0)$
129		csbeq1	$⊢ w = \frac{1}{y} \to ⦋ w / x ⦌ R = ⦋ (\frac{1}{y}) / x ⦌ R$
130	128 129	ifbieq2d	$⊢ w = \frac{1}{y} \to if (w = 0, C, ⦋ w / x ⦌ R) = if (\frac{1}{y} = 0, C, ⦋ (\frac{1}{y}) / x ⦌ R)$
131	1 2 55 122 126 127 130 8 9	rlimcnp	$⊢ φ \to ((y \in (B \cap ℝ^{+}) ⟼ if (\frac{1}{y} = 0, C, ⦋ (\frac{1}{y}) / x ⦌ R)) \underset{ℝ}{⇝} C \leftrightarrow (w \in A ⟼ if (w = 0, C, ⦋ w / x ⦌ R)) \in (K CnP J) (0))$
132		nfcv	$⊢ \underline{Ⅎ} w if (x = 0, C, R)$
133		nfv	$⊢ Ⅎ x w = 0$
134		nfcv	$⊢ \underline{Ⅎ} x C$
135		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ w / x ⦌ R$
136	133 134 135	nfif	$⊢ \underline{Ⅎ} x if (w = 0, C, ⦋ w / x ⦌ R)$
137		eqeq1	$⊢ x = w \to (x = 0 \leftrightarrow w = 0)$
138		csbeq1a	$⊢ x = w \to R = ⦋ w / x ⦌ R$
139	137 138	ifbieq2d	$⊢ x = w \to if (x = 0, C, R) = if (w = 0, C, ⦋ w / x ⦌ R)$
140	132 136 139	cbvmpt	$⊢ (x \in A ⟼ if (x = 0, C, R)) = (w \in A ⟼ if (w = 0, C, ⦋ w / x ⦌ R))$
141	140	eleq1i	$⊢ (x \in A ⟼ if (x = 0, C, R)) \in (K CnP J) (0) \leftrightarrow (w \in A ⟼ if (w = 0, C, ⦋ w / x ⦌ R)) \in (K CnP J) (0)$
142	131 141	bitr4di	$⊢ φ \to ((y \in (B \cap ℝ^{+}) ⟼ if (\frac{1}{y} = 0, C, ⦋ (\frac{1}{y}) / x ⦌ R)) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ if (x = 0, C, R)) \in (K CnP J) (0))$
143	53 72 142	3bitr2d	$⊢ φ \to ((y \in B ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ if (x = 0, C, R)) \in (K CnP J) (0))$

Metamath Proof Explorer

Theorem rlimcnp2

Proof