# Metamath Proof Explorer

## Theorem rlim

Description: Express the predicate: The limit of complex number function F is C , or F converges to C , in the real sense. This means that for any real x , no matter how small, there always exists a number y such that the absolute difference of any number in the function beyond y and the limit is less than x . (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypotheses rlim.1 ${⊢}{\phi }\to {F}:{A}⟶ℂ$
rlim.2 ${⊢}{\phi }\to {A}\subseteq ℝ$
rlim.4 ${⊢}\left({\phi }\wedge {z}\in {A}\right)\to {F}\left({z}\right)={B}$
Assertion rlim

### Proof

Step Hyp Ref Expression
1 rlim.1 ${⊢}{\phi }\to {F}:{A}⟶ℂ$
2 rlim.2 ${⊢}{\phi }\to {A}\subseteq ℝ$
3 rlim.4 ${⊢}\left({\phi }\wedge {z}\in {A}\right)\to {F}\left({z}\right)={B}$
4 rlimrel
5 4 brrelex2i
6 5 a1i
7 elex ${⊢}{C}\in ℂ\to {C}\in \mathrm{V}$
8 7 ad2antrl ${⊢}\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge \left({C}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)\right)\to {C}\in \mathrm{V}$
9 8 a1i ${⊢}{\phi }\to \left(\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge \left({C}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)\right)\to {C}\in \mathrm{V}\right)$
10 cnex ${⊢}ℂ\in \mathrm{V}$
11 reex ${⊢}ℝ\in \mathrm{V}$
12 elpm2r ${⊢}\left(\left(ℂ\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\wedge \left({F}:{A}⟶ℂ\wedge {A}\subseteq ℝ\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
13 10 11 12 mpanl12 ${⊢}\left({F}:{A}⟶ℂ\wedge {A}\subseteq ℝ\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
14 1 2 13 syl2anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
15 eleq1 ${⊢}{f}={F}\to \left({f}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)↔{F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\right)$
16 eleq1 ${⊢}{w}={C}\to \left({w}\in ℂ↔{C}\in ℂ\right)$
17 15 16 bi2anan9 ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \left(\left({f}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge {w}\in ℂ\right)↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge {C}\in ℂ\right)\right)$
18 simpl ${⊢}\left({f}={F}\wedge {w}={C}\right)\to {f}={F}$
19 18 dmeqd ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \mathrm{dom}{f}=\mathrm{dom}{F}$
20 fveq1 ${⊢}{f}={F}\to {f}\left({z}\right)={F}\left({z}\right)$
21 oveq12 ${⊢}\left({f}\left({z}\right)={F}\left({z}\right)\wedge {w}={C}\right)\to {f}\left({z}\right)-{w}={F}\left({z}\right)-{C}$
22 20 21 sylan ${⊢}\left({f}={F}\wedge {w}={C}\right)\to {f}\left({z}\right)-{w}={F}\left({z}\right)-{C}$
23 22 fveq2d ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \left|{f}\left({z}\right)-{w}\right|=\left|{F}\left({z}\right)-{C}\right|$
24 23 breq1d ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \left(\left|{f}\left({z}\right)-{w}\right|<{x}↔\left|{F}\left({z}\right)-{C}\right|<{x}\right)$
25 24 imbi2d ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \left(\left({y}\le {z}\to \left|{f}\left({z}\right)-{w}\right|<{x}\right)↔\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)$
26 19 25 raleqbidv ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \left(\forall {z}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{f}\left({z}\right)-{w}\right|<{x}\right)↔\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)$
27 26 rexbidv ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{f}\left({z}\right)-{w}\right|<{x}\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)$
28 27 ralbidv ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{f}\left({z}\right)-{w}\right|<{x}\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)$
29 17 28 anbi12d ${⊢}\left({f}={F}\wedge {w}={C}\right)\to \left(\left(\left({f}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge {w}\in ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{f}\left({z}\right)-{w}\right|<{x}\right)\right)↔\left(\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge {C}\in ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)\right)$
30 df-rlim
31 29 30 brabga
32 anass ${⊢}\left(\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge {C}\in ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge \left({C}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)\right)$
33 31 32 syl6bb
34 33 ex
35 14 34 syl
36 6 9 35 pm5.21ndd
37 14 biantrurd ${⊢}{\phi }\to \left(\left({C}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge \left({C}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)\right)\right)$
38 1 fdmd ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
39 38 raleqdv ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)$
40 3 fvoveq1d ${⊢}\left({\phi }\wedge {z}\in {A}\right)\to \left|{F}\left({z}\right)-{C}\right|=\left|{B}-{C}\right|$
41 40 breq1d ${⊢}\left({\phi }\wedge {z}\in {A}\right)\to \left(\left|{F}\left({z}\right)-{C}\right|<{x}↔\left|{B}-{C}\right|<{x}\right)$
42 41 imbi2d ${⊢}\left({\phi }\wedge {z}\in {A}\right)\to \left(\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)↔\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
43 42 ralbidva ${⊢}{\phi }\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
44 39 43 bitrd ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
45 44 rexbidv ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
46 45 ralbidv ${⊢}{\phi }\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)$
47 46 anbi2d ${⊢}{\phi }\to \left(\left({C}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{F}\left({z}\right)-{C}\right|<{x}\right)\right)↔\left({C}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left|{B}-{C}\right|<{x}\right)\right)\right)$
48 36 37 47 3bitr2d