Metamath Proof Explorer

Theorem lmclim

Description: Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 9-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmclim.2 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
lmclim.3 ${⊢}{Z}={ℤ}_{\ge {M}}$
Assertion lmclim

Proof

Step Hyp Ref Expression
1 lmclim.2 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 lmclim.3 ${⊢}{Z}={ℤ}_{\ge {M}}$
3 3anass ${⊢}\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)\right)↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge \left({P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)\right)\right)$
4 2 uztrn2 ${⊢}\left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
5 3anass ${⊢}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\left({k}\in \mathrm{dom}{F}\wedge \left({F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)\right)$
6 simplr ${⊢}\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\to {Z}\subseteq \mathrm{dom}{F}$
7 6 sselda ${⊢}\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\wedge {k}\in {Z}\right)\to {k}\in \mathrm{dom}{F}$
8 7 biantrurd ${⊢}\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\wedge {k}\in {Z}\right)\to \left(\left({F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\left({k}\in \mathrm{dom}{F}\wedge \left({F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)\right)\right)$
9 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
10 9 cnmetdval ${⊢}\left({F}\left({k}\right)\in ℂ\wedge {P}\in ℂ\right)\to {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}=\left|{F}\left({k}\right)-{P}\right|$
11 10 ancoms ${⊢}\left({P}\in ℂ\wedge {F}\left({k}\right)\in ℂ\right)\to {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}=\left|{F}\left({k}\right)-{P}\right|$
12 11 breq1d ${⊢}\left({P}\in ℂ\wedge {F}\left({k}\right)\in ℂ\right)\to \left({F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}↔\left|{F}\left({k}\right)-{P}\right|<{x}\right)$
13 12 pm5.32da ${⊢}{P}\in ℂ\to \left(\left({F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
14 13 ad2antlr ${⊢}\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\wedge {k}\in {Z}\right)\to \left(\left({F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
15 8 14 bitr3d ${⊢}\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\wedge {k}\in {Z}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge \left({F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)\right)↔\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
16 5 15 syl5bb ${⊢}\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\wedge {k}\in {Z}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
17 4 16 sylan2 ${⊢}\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\wedge \left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
18 17 anassrs ${⊢}\left(\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
19 18 ralbidva ${⊢}\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
20 19 rexbidva ${⊢}\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
21 20 ralbidv ${⊢}\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {P}\in ℂ\right)\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)$
22 21 pm5.32da ${⊢}\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\to \left(\left({P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)\right)↔\left({P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)\right)$
23 22 anbi2d ${⊢}\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\to \left(\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge \left({P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)\right)\right)↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge \left({P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)\right)\right)$
24 3 23 syl5bb ${⊢}\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\to \left(\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\wedge {F}\left({k}\right)\left(\mathrm{abs}\circ -\right){P}<{x}\right)\right)↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge \left({P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)\right)\right)$
25 1 cnfldtopn ${⊢}{J}=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$
26 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
27 26 a1i ${⊢}\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\to \mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
28 simpl ${⊢}\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\to {M}\in ℤ$
29 25 27 2 28 lmmbr3
30 simpll ${⊢}\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\right)\to {M}\in ℤ$
31 simpr ${⊢}\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)$
32 eqidd ${⊢}\left(\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\right)\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={F}\left({k}\right)$
33 2 30 31 32 clim2 ${⊢}\left(\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\right)\to \left({F}⇝{P}↔\left({P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)\right)$
34 33 pm5.32da ${⊢}\left({M}\in ℤ\wedge {Z}\subseteq \mathrm{dom}{F}\right)\to \left(\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge {F}⇝{P}\right)↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge \left({P}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{P}\right|<{x}\right)\right)\right)\right)$
35 24 29 34 3bitr4d