Step | Hyp | Ref
| Expression |
1 | | eldmg 5319 |
. . 3
|
2 | 1 | ibi 256 |
. 2
|
3 | | simpl2 1065 |
. . . . . 6
|
4 | 3 | ffvelrnda 6359 |
. . . . . . . . 9
|
5 | | dvcnp.k |
. . . . . . . . . . . . . . 15
ℂfld |
6 | 5 | cnfldtop 22587 |
. . . . . . . . . . . . . 14
|
7 | | simpl1 1064 |
. . . . . . . . . . . . . . 15
|
8 | | cnex 10017 |
. . . . . . . . . . . . . . 15
|
9 | | ssexg 4804 |
. . . . . . . . . . . . . . 15
|
10 | 7, 8, 9 | sylancl 694 |
. . . . . . . . . . . . . 14
|
11 | | resttop 20964 |
. . . . . . . . . . . . . 14
↾t |
12 | 6, 10, 11 | sylancr 695 |
. . . . . . . . . . . . 13
↾t |
13 | | simpl3 1066 |
. . . . . . . . . . . . . 14
|
14 | 5 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . 16
TopOn |
15 | | resttopon 20965 |
. . . . . . . . . . . . . . . 16
TopOn
↾t TopOn |
16 | 14, 7, 15 | sylancr 695 |
. . . . . . . . . . . . . . 15
↾t TopOn |
17 | | toponuni 20719 |
. . . . . . . . . . . . . . 15
↾t TopOn ↾t |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . 14
↾t |
19 | 13, 18 | sseqtrd 3641 |
. . . . . . . . . . . . 13
↾t |
20 | | eqid 2622 |
. . . . . . . . . . . . . 14
↾t
↾t |
21 | 20 | ntrss2 20861 |
. . . . . . . . . . . . 13
↾t
↾t ↾t |
22 | 12, 19, 21 | syl2anc 693 |
. . . . . . . . . . . 12
↾t |
23 | | eqid 2622 |
. . . . . . . . . . . . . 14
↾t ↾t |
24 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
25 | | simp1 1061 |
. . . . . . . . . . . . . 14
|
26 | | simp2 1062 |
. . . . . . . . . . . . . 14
|
27 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
28 | 23, 5, 24, 25, 26, 27 | eldv 23662 |
. . . . . . . . . . . . 13
↾t lim |
29 | 28 | simprbda 653 |
. . . . . . . . . . . 12
↾t |
30 | 22, 29 | sseldd 3604 |
. . . . . . . . . . 11
|
31 | 3, 30 | ffvelrnd 6360 |
. . . . . . . . . 10
|
32 | 31 | adantr 481 |
. . . . . . . . 9
|
33 | 4, 32 | subcld 10392 |
. . . . . . . 8
|
34 | | ssid 3624 |
. . . . . . . . 9
|
35 | 34 | a1i 11 |
. . . . . . . 8
|
36 | | txtopon 21394 |
. . . . . . . . . . 11
TopOn
TopOn
TopOn |
37 | 14, 14, 36 | mp2an 708 |
. . . . . . . . . 10
TopOn |
38 | 37 | toponunii 20721 |
. . . . . . . . . . 11
|
39 | 38 | restid 16094 |
. . . . . . . . . 10
TopOn ↾t |
40 | 37, 39 | ax-mp 5 |
. . . . . . . . 9
↾t |
41 | 40 | eqcomi 2631 |
. . . . . . . 8
↾t |
42 | 13, 7 | sstrd 3613 |
. . . . . . . . . . . 12
|
43 | 3, 42, 30 | dvlem 23660 |
. . . . . . . . . . 11
|
44 | 42 | ssdifssd 3748 |
. . . . . . . . . . . . 13
|
45 | 44 | sselda 3603 |
. . . . . . . . . . . 12
|
46 | 42, 30 | sseldd 3604 |
. . . . . . . . . . . . 13
|
47 | 46 | adantr 481 |
. . . . . . . . . . . 12
|
48 | 45, 47 | subcld 10392 |
. . . . . . . . . . 11
|
49 | 28 | simplbda 654 |
. . . . . . . . . . 11
lim |
50 | | limcresi 23649 |
. . . . . . . . . . . . 13
lim
lim |
51 | | difss 3737 |
. . . . . . . . . . . . . . 15
|
52 | | resmpt 5449 |
. . . . . . . . . . . . . . 15
|
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
54 | 53 | oveq1i 6660 |
. . . . . . . . . . . . 13
lim lim |
55 | 50, 54 | sseqtri 3637 |
. . . . . . . . . . . 12
lim lim |
56 | 46 | subidd 10380 |
. . . . . . . . . . . . 13
|
57 | 5 | subcn 22669 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . 15
|
59 | | cncfmptid 22715 |
. . . . . . . . . . . . . . . 16
|
60 | 42, 34, 59 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
61 | | cncfmptc 22714 |
. . . . . . . . . . . . . . . 16
|
62 | 46, 42, 35, 61 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
63 | 5, 58, 60, 62 | cncfmpt2f 22717 |
. . . . . . . . . . . . . 14
|
64 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
65 | 63, 30, 64 | cnmptlimc 23654 |
. . . . . . . . . . . . 13
lim |
66 | 56, 65 | eqeltrrd 2702 |
. . . . . . . . . . . 12
lim |
67 | 55, 66 | sseldi 3601 |
. . . . . . . . . . 11
lim |
68 | 5 | mulcn 22670 |
. . . . . . . . . . . 12
|
69 | 25, 26, 27 | dvcl 23663 |
. . . . . . . . . . . . 13
|
70 | | 0cn 10032 |
. . . . . . . . . . . . 13
|
71 | | opelxpi 5148 |
. . . . . . . . . . . . 13
|
72 | 69, 70, 71 | sylancl 694 |
. . . . . . . . . . . 12
|
73 | 38 | cncnpi 21082 |
. . . . . . . . . . . 12
|
74 | 68, 72, 73 | sylancr 695 |
. . . . . . . . . . 11
|
75 | 43, 48, 35, 35, 5, 41, 49, 67, 74 | limccnp2 23656 |
. . . . . . . . . 10
lim |
76 | 69 | mul01d 10235 |
. . . . . . . . . 10
|
77 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
|
78 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
79 | 51, 78 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
80 | 77, 79 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
81 | 31 | adantr 481 |
. . . . . . . . . . . . . 14
|
82 | 80, 81 | subcld 10392 |
. . . . . . . . . . . . 13
|
83 | | eldifsni 4320 |
. . . . . . . . . . . . . . 15
|
84 | 83 | adantl 482 |
. . . . . . . . . . . . . 14
|
85 | 45, 47, 84 | subne0d 10401 |
. . . . . . . . . . . . 13
|
86 | 82, 48, 85 | divcan1d 10802 |
. . . . . . . . . . . 12
|
87 | 86 | mpteq2dva 4744 |
. . . . . . . . . . 11
|
88 | 87 | oveq1d 6665 |
. . . . . . . . . 10
lim lim |
89 | 75, 76, 88 | 3eltr3d 2715 |
. . . . . . . . 9
lim |
90 | | eqid 2622 |
. . . . . . . . . . . 12
|
91 | 33, 90 | fmptd 6385 |
. . . . . . . . . . 11
|
92 | 91 | limcdif 23640 |
. . . . . . . . . 10
lim lim |
93 | | resmpt 5449 |
. . . . . . . . . . . 12
|
94 | 51, 93 | ax-mp 5 |
. . . . . . . . . . 11
|
95 | 94 | oveq1i 6660 |
. . . . . . . . . 10
lim lim |
96 | 92, 95 | syl6eq 2672 |
. . . . . . . . 9
lim lim |
97 | 89, 96 | eleqtrrd 2704 |
. . . . . . . 8
lim |
98 | | cncfmptc 22714 |
. . . . . . . . . 10
|
99 | 31, 42, 35, 98 | syl3anc 1326 |
. . . . . . . . 9
|
100 | | eqidd 2623 |
. . . . . . . . 9
|
101 | 99, 30, 100 | cnmptlimc 23654 |
. . . . . . . 8
lim |
102 | 5 | addcn 22668 |
. . . . . . . . 9
|
103 | | opelxpi 5148 |
. . . . . . . . . 10
|
104 | 70, 31, 103 | sylancr 695 |
. . . . . . . . 9
|
105 | 38 | cncnpi 21082 |
. . . . . . . . 9
|
106 | 102, 104,
105 | sylancr 695 |
. . . . . . . 8
|
107 | 33, 32, 35, 35, 5, 41, 97, 101, 106 | limccnp2 23656 |
. . . . . . 7
lim |
108 | 31 | addid2d 10237 |
. . . . . . 7
|
109 | 4, 32 | npcand 10396 |
. . . . . . . . . 10
|
110 | 109 | mpteq2dva 4744 |
. . . . . . . . 9
|
111 | 3 | feqmptd 6249 |
. . . . . . . . 9
|
112 | 110, 111 | eqtr4d 2659 |
. . . . . . . 8
|
113 | 112 | oveq1d 6665 |
. . . . . . 7
lim lim |
114 | 107, 108,
113 | 3eltr3d 2715 |
. . . . . 6
lim |
115 | | dvcnp.j |
. . . . . . . 8
↾t |
116 | 5, 115 | cnplimc 23651 |
. . . . . . 7
lim |
117 | 42, 30, 116 | syl2anc 693 |
. . . . . 6
lim |
118 | 3, 114, 117 | mpbir2and 957 |
. . . . 5
|
119 | 118 | ex 450 |
. . . 4
|
120 | 119 | exlimdv 1861 |
. . 3
|
121 | 120 | imp 445 |
. 2
|
122 | 2, 121 | sylan2 491 |
1
|