Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnheibor Structured version   Visualization version   Unicode version

Theorem cnheibor 22061
 Description: Heine-Borel theorem for complex numbers. A subset of is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.)
Hypotheses
Ref Expression
cnheibor.2 fld
cnheibor.3 t
Assertion
Ref Expression
cnheibor
Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem cnheibor
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnheibor.2 . . . . . 6 fld
21cnfldhaus 21883 . . . . 5
32a1i 11 . . . 4
4 simpl 464 . . . 4
5 cnheibor.3 . . . . 5 t
6 simpr 468 . . . . 5
75, 6syl5eqelr 2554 . . . 4 t
81cnfldtopon 21881 . . . . . 6 TopOn
98toponunii 20024 . . . . 5
109hauscmp 20499 . . . 4 t
113, 4, 7, 10syl3anc 1292 . . 3
121cnfldtop 21882 . . . . . . . . . . 11
139restuni 20255 . . . . . . . . . . 11 t
1412, 4, 13sylancr 676 . . . . . . . . . 10 t
155unieqi 4199 . . . . . . . . . 10 t
1614, 15syl6eqr 2523 . . . . . . . . 9
1716eleq2d 2534 . . . . . . . 8
1817biimpar 493 . . . . . . 7
1912a1i 11 . . . . . . . . . 10
20 cnex 9638 . . . . . . . . . . . 12
21 ssexg 4542 . . . . . . . . . . . 12
224, 20, 21sylancl 675 . . . . . . . . . . 11
2322adantr 472 . . . . . . . . . 10
24 cnxmet 21871 . . . . . . . . . . . 12
2524a1i 11 . . . . . . . . . . 11
26 0cnd 9654 . . . . . . . . . . 11
274sselda 3418 . . . . . . . . . . . . . 14
2827abscld 13575 . . . . . . . . . . . . 13
29 peano2re 9824 . . . . . . . . . . . . 13
3028, 29syl 17 . . . . . . . . . . . 12
3130rexrd 9708 . . . . . . . . . . 11
321cnfldtopn 21880 . . . . . . . . . . . 12
3332blopn 21593 . . . . . . . . . . 11
3425, 26, 31, 33syl3anc 1292 . . . . . . . . . 10
35 elrestr 15405 . . . . . . . . . 10 t
3619, 23, 34, 35syl3anc 1292 . . . . . . . . 9 t
3736, 5syl6eleqr 2560 . . . . . . . 8
38 0cn 9653 . . . . . . . . . . . . . 14
39 eqid 2471 . . . . . . . . . . . . . . 15
4039cnmetdval 21869 . . . . . . . . . . . . . 14
4138, 40mpan 684 . . . . . . . . . . . . 13
42 df-neg 9883 . . . . . . . . . . . . . . 15
4342fveq2i 5882 . . . . . . . . . . . . . 14
44 absneg 13417 . . . . . . . . . . . . . 14
4543, 44syl5eqr 2519 . . . . . . . . . . . . 13
4641, 45eqtrd 2505 . . . . . . . . . . . 12
4727, 46syl 17 . . . . . . . . . . 11
4828ltp1d 10559 . . . . . . . . . . 11
4947, 48eqbrtrd 4416 . . . . . . . . . 10
50 elbl 21481 . . . . . . . . . . 11
5125, 26, 31, 50syl3anc 1292 . . . . . . . . . 10
5227, 49, 51mpbir2and 936 . . . . . . . . 9
53 simpr 468 . . . . . . . . 9
5452, 53elind 3609 . . . . . . . 8
5527absge0d 13583 . . . . . . . . . 10
5628, 55ge0p1rpd 11391 . . . . . . . . 9
57 eqid 2471 . . . . . . . . 9
58 oveq2 6316 . . . . . . . . . . . 12
5958ineq1d 3624 . . . . . . . . . . 11
6059eqeq2d 2481 . . . . . . . . . 10
6160rspcev 3136 . . . . . . . . 9
6256, 57, 61sylancl 675 . . . . . . . 8
63 eleq2 2538 . . . . . . . . . 10
64 eqeq1 2475 . . . . . . . . . . 11
6564rexbidv 2892 . . . . . . . . . 10
6663, 65anbi12d 725 . . . . . . . . 9
6766rspcev 3136 . . . . . . . 8
6837, 54, 62, 67syl12anc 1290 . . . . . . 7
6918, 68syldan 478 . . . . . 6
7069ralrimiva 2809 . . . . 5
71 eqid 2471 . . . . . 6
72 oveq2 6316 . . . . . . . 8
7372ineq1d 3624 . . . . . . 7
7473eqeq2d 2481 . . . . . 6
7571, 74cmpcovf 20483 . . . . 5
766, 70, 75syl2anc 673 . . . 4
7716ad4antr 746 . . . . . . . . . . . . . 14
78 simpllr 777 . . . . . . . . . . . . . 14
7977, 78eqtrd 2505 . . . . . . . . . . . . 13
8079eleq2d 2534 . . . . . . . . . . . 12
81 eluni2 4194 . . . . . . . . . . . 12
8280, 81syl6bb 269 . . . . . . . . . . 11
83 elssuni 4219 . . . . . . . . . . . . . . . . . 18
8483ad2antrl 742 . . . . . . . . . . . . . . . . 17
8579adantr 472 . . . . . . . . . . . . . . . . 17
8684, 85sseqtr4d 3455 . . . . . . . . . . . . . . . 16
87 simp-6l 788 . . . . . . . . . . . . . . . 16
8886, 87sstrd 3428 . . . . . . . . . . . . . . 15
89 simprr 774 . . . . . . . . . . . . . . 15
9088, 89sseldd 3419 . . . . . . . . . . . . . 14
9190abscld 13575 . . . . . . . . . . . . 13
92 simplrl 778 . . . . . . . . . . . . 13
93 simprl 772 . . . . . . . . . . . . . . . . 17
9493ad2antrr 740 . . . . . . . . . . . . . . . 16
95 simprl 772 . . . . . . . . . . . . . . . 16
9694, 95ffvelrnd 6038 . . . . . . . . . . . . . . 15
9796rpred 11364 . . . . . . . . . . . . . 14
9890, 46syl 17 . . . . . . . . . . . . . . 15
99 inss1 3643 . . . . . . . . . . . . . . . . . 18
100 simprr 774 . . . . . . . . . . . . . . . . . . . . 21
101100ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20
102 id 22 . . . . . . . . . . . . . . . . . . . . . 22
103 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24
104103oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . 23
105104ineq1d 3624 . . . . . . . . . . . . . . . . . . . . . 22
106102, 105eqeq12d 2486 . . . . . . . . . . . . . . . . . . . . 21
107106rspcv 3132 . . . . . . . . . . . . . . . . . . . 20
10895, 101, 107sylc 61 . . . . . . . . . . . . . . . . . . 19
10989, 108eleqtrd 2551 . . . . . . . . . . . . . . . . . 18
11099, 109sseldi 3416 . . . . . . . . . . . . . . . . 17
11124a1i 11 . . . . . . . . . . . . . . . . . 18
112 0cnd 9654 . . . . . . . . . . . . . . . . . 18
11396rpxrd 11365 . . . . . . . . . . . . . . . . . 18
114 elbl 21481 . . . . . . . . . . . . . . . . . 18
115111, 112, 113, 114syl3anc 1292 . . . . . . . . . . . . . . . . 17
116110, 115mpbid 215 . . . . . . . . . . . . . . . 16
117116simprd 470 . . . . . . . . . . . . . . 15
11898, 117eqbrtrrd 4418 . . . . . . . . . . . . . 14
119 simplrr 779 . . . . . . . . . . . . . . 15
120103breq1d 4405 . . . . . . . . . . . . . . . 16
121120rspcv 3132 . . . . . . . . . . . . . . 15
12295, 119, 121sylc 61 . . . . . . . . . . . . . 14
12391, 97, 92, 118, 122ltletrd 9812 . . . . . . . . . . . . 13
12491, 92, 123ltled 9800 . . . . . . . . . . . 12
125124rexlimdvaa 2872 . . . . . . . . . . 11
12682, 125sylbid 223 . . . . . . . . . 10
127126ralrimiv 2808 . . . . . . . . 9
128 inss2 3644 . . . . . . . . . . 11
129 simpllr 777 . . . . . . . . . . 11
130128, 129sseldi 3416 . . . . . . . . . 10
131 ffvelrn 6035 . . . . . . . . . . . . 13
132131rpred 11364 . . . . . . . . . . . 12
133132ralrimiva 2809 . . . . . . . . . . 11
134133ad2antrl 742 . . . . . . . . . 10
135 fimaxre3 10575 . . . . . . . . . 10
136130, 134, 135syl2anc 673 . . . . . . . . 9
137127, 136reximddv 2859 . . . . . . . 8
138137ex 441 . . . . . . 7
139138exlimdv 1787 . . . . . 6
140139expimpd 614 . . . . 5
141140rexlimdva 2871 . . . 4
14276, 141mpd 15 . . 3
14311, 142jca 541 . 2
144 eqid 2471 . . . . . 6
145 eqid 2471 . . . . . 6
1461, 5, 144, 145cnheiborlem 22060 . . . . 5
147146rexlimdvaa 2872 . . . 4
148147imp 436 . . 3