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 | |
|
lmclim.3 | |
||
Assertion | lmclim | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmclim.2 | |
|
2 | lmclim.3 | |
|
3 | 3anass | |
|
4 | 2 | uztrn2 | |
5 | 3anass | |
|
6 | simplr | |
|
7 | 6 | sselda | |
8 | 7 | biantrurd | |
9 | eqid | |
|
10 | 9 | cnmetdval | |
11 | 10 | ancoms | |
12 | 11 | breq1d | |
13 | 12 | pm5.32da | |
14 | 13 | ad2antlr | |
15 | 8 14 | bitr3d | |
16 | 5 15 | syl5bb | |
17 | 4 16 | sylan2 | |
18 | 17 | anassrs | |
19 | 18 | ralbidva | |
20 | 19 | rexbidva | |
21 | 20 | ralbidv | |
22 | 21 | pm5.32da | |
23 | 22 | anbi2d | |
24 | 3 23 | syl5bb | |
25 | 1 | cnfldtopn | |
26 | cnxmet | |
|
27 | 26 | a1i | |
28 | simpl | |
|
29 | 25 27 2 28 | lmmbr3 | |
30 | simpll | |
|
31 | simpr | |
|
32 | eqidd | |
|
33 | 2 30 31 32 | clim2 | |
34 | 33 | pm5.32da | |
35 | 24 29 34 | 3bitr4d | |