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=TopOpenfld
lmclim.3 Z=M
Assertion lmclim MZdomFFtJPF𝑝𝑚FP

Proof

Step Hyp Ref Expression
1 lmclim.2 J=TopOpenfld
2 lmclim.3 Z=M
3 3anass F𝑝𝑚Px+jZkjkdomFFkFkabsP<xF𝑝𝑚Px+jZkjkdomFFkFkabsP<x
4 2 uztrn2 jZkjkZ
5 3anass kdomFFkFkabsP<xkdomFFkFkabsP<x
6 simplr MZdomFPZdomF
7 6 sselda MZdomFPkZkdomF
8 7 biantrurd MZdomFPkZFkFkabsP<xkdomFFkFkabsP<x
9 eqid abs=abs
10 9 cnmetdval FkPFkabsP=FkP
11 10 ancoms PFkFkabsP=FkP
12 11 breq1d PFkFkabsP<xFkP<x
13 12 pm5.32da PFkFkabsP<xFkFkP<x
14 13 ad2antlr MZdomFPkZFkFkabsP<xFkFkP<x
15 8 14 bitr3d MZdomFPkZkdomFFkFkabsP<xFkFkP<x
16 5 15 syl5bb MZdomFPkZkdomFFkFkabsP<xFkFkP<x
17 4 16 sylan2 MZdomFPjZkjkdomFFkFkabsP<xFkFkP<x
18 17 anassrs MZdomFPjZkjkdomFFkFkabsP<xFkFkP<x
19 18 ralbidva MZdomFPjZkjkdomFFkFkabsP<xkjFkFkP<x
20 19 rexbidva MZdomFPjZkjkdomFFkFkabsP<xjZkjFkFkP<x
21 20 ralbidv MZdomFPx+jZkjkdomFFkFkabsP<xx+jZkjFkFkP<x
22 21 pm5.32da MZdomFPx+jZkjkdomFFkFkabsP<xPx+jZkjFkFkP<x
23 22 anbi2d MZdomFF𝑝𝑚Px+jZkjkdomFFkFkabsP<xF𝑝𝑚Px+jZkjFkFkP<x
24 3 23 syl5bb MZdomFF𝑝𝑚Px+jZkjkdomFFkFkabsP<xF𝑝𝑚Px+jZkjFkFkP<x
25 1 cnfldtopn J=MetOpenabs
26 cnxmet abs∞Met
27 26 a1i MZdomFabs∞Met
28 simpl MZdomFM
29 25 27 2 28 lmmbr3 MZdomFFtJPF𝑝𝑚Px+jZkjkdomFFkFkabsP<x
30 simpll MZdomFF𝑝𝑚M
31 simpr MZdomFF𝑝𝑚F𝑝𝑚
32 eqidd MZdomFF𝑝𝑚kZFk=Fk
33 2 30 31 32 clim2 MZdomFF𝑝𝑚FPPx+jZkjFkFkP<x
34 33 pm5.32da MZdomFF𝑝𝑚FPF𝑝𝑚Px+jZkjFkFkP<x
35 24 29 34 3bitr4d MZdomFFtJPF𝑝𝑚FP