Theorem rlimi

Description: Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015)

	Ref	Expression
Hypotheses	rlimi.1	$$⊢\phi \to \forall z\in AB\in V$$
	rlimi.2	$$⊢\phi \to R\in {ℝ}^{+}$$
	rlimi.3	$$⊢\phi \to \left(z\in A⟼B\right)\underset{ℝ}{⇝}C$$
Assertion	rlimi	$$⊢\phi \to \exists y\in ℝ\forall z\in A\left(y\le z\to \left|B-C\right|<R\right)$$

Proof

Step	Hyp	Ref	Expression
1		rlimi.1	$$⊢\phi \to \forall z\in AB\in V$$
2		rlimi.2	$$⊢\phi \to R\in {ℝ}^{+}$$
3		rlimi.3	$$⊢\phi \to \left(z\in A⟼B\right)\underset{ℝ}{⇝}C$$
4		breq2	$$⊢x=R\to \left(\left|B-C\right|<x\leftrightarrow \left|B-C\right|<R\right)$$
5	4	imbi2d	$$⊢x=R\to \left(\left(y\le z\to \left|B-C\right|<x\right)\leftrightarrow \left(y\le z\to \left|B-C\right|<R\right)\right)$$
6	5	rexralbidv	$$⊢x=R\to \left(\exists y\in ℝ\forall z\in A\left(y\le z\to \left|B-C\right|<x\right)\leftrightarrow \exists y\in ℝ\forall z\in A\left(y\le z\to \left|B-C\right|<R\right)\right)$$
7		rlimf	$$⊢\left(z\in A⟼B\right)\underset{ℝ}{⇝}C\to \left(z\in A⟼B\right):\mathrm{dom}\left(z\in A⟼B\right)⟶ℂ$$
8	3 7	syl	$$⊢\phi \to \left(z\in A⟼B\right):\mathrm{dom}\left(z\in A⟼B\right)⟶ℂ$$
9		eqid	$$⊢\left(z\in A⟼B\right)=\left(z\in A⟼B\right)$$
10	9	fmpt	$$⊢\forall z\in AB\in V\leftrightarrow \left(z\in A⟼B\right):A⟶V$$
11	1 10	sylib	$$⊢\phi \to \left(z\in A⟼B\right):A⟶V$$
12	11	fdmd	$$⊢\phi \to \mathrm{dom}\left(z\in A⟼B\right)=A$$
13	12	feq2d	$$⊢\phi \to \left(\left(z\in A⟼B\right):\mathrm{dom}\left(z\in A⟼B\right)⟶ℂ\leftrightarrow \left(z\in A⟼B\right):A⟶ℂ\right)$$
14	8 13	mpbid	$$⊢\phi \to \left(z\in A⟼B\right):A⟶ℂ$$
15	9	fmpt	$$⊢\forall z\in AB\in ℂ\leftrightarrow \left(z\in A⟼B\right):A⟶ℂ$$
16	14 15	sylibr	$$⊢\phi \to \forall z\in AB\in ℂ$$
17		rlimss	$$⊢\left(z\in A⟼B\right)\underset{ℝ}{⇝}C\to \mathrm{dom}\left(z\in A⟼B\right)\subseteq ℝ$$
18	3 17	syl	$$⊢\phi \to \mathrm{dom}\left(z\in A⟼B\right)\subseteq ℝ$$
19	12 18	eqsstrrd	$$⊢\phi \to A\subseteq ℝ$$
20		rlimcl	$$⊢\left(z\in A⟼B\right)\underset{ℝ}{⇝}C\to C\in ℂ$$
21	3 20	syl	$$⊢\phi \to C\in ℂ$$
22	16 19 21	rlim2	$$⊢\phi \to \left(\left(z\in A⟼B\right)\underset{ℝ}{⇝}C\leftrightarrow \forall x\in {ℝ}^{+}\exists y\in ℝ\forall z\in A\left(y\le z\to \left|B-C\right|<x\right)\right)$$
23	3 22	mpbid	$$⊢\phi \to \forall x\in {ℝ}^{+}\exists y\in ℝ\forall z\in A\left(y\le z\to \left|B-C\right|<x\right)$$
24	6 23 2	rspcdva	$$⊢\phi \to \exists y\in ℝ\forall z\in A\left(y\le z\to \left|B-C\right|<R\right)$$