Metamath Proof Explorer


Theorem cnheibor

Description: Heine-Borel theorem for complex numbers. A subset of CC is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses cnheibor.2 J = TopOpen fld
cnheibor.3 T = J 𝑡 X
Assertion cnheibor X T Comp X Clsd J r x X x r

Proof

Step Hyp Ref Expression
1 cnheibor.2 J = TopOpen fld
2 cnheibor.3 T = J 𝑡 X
3 1 cnfldhaus J Haus
4 simpl X T Comp X
5 simpr X T Comp T Comp
6 2 5 eqeltrrid X T Comp J 𝑡 X Comp
7 1 cnfldtopon J TopOn
8 7 toponunii = J
9 8 hauscmp J Haus X J 𝑡 X Comp X Clsd J
10 3 4 6 9 mp3an2i X T Comp X Clsd J
11 1 cnfldtop J Top
12 8 restuni J Top X X = J 𝑡 X
13 11 4 12 sylancr X T Comp X = J 𝑡 X
14 2 unieqi T = J 𝑡 X
15 13 14 eqtr4di X T Comp X = T
16 15 eleq2d X T Comp x X x T
17 16 biimpar X T Comp x T x X
18 cnex V
19 ssexg X V X V
20 4 18 19 sylancl X T Comp X V
21 20 adantr X T Comp x X X V
22 cnxmet abs ∞Met
23 0cnd X T Comp x X 0
24 4 sselda X T Comp x X x
25 24 abscld X T Comp x X x
26 peano2re x x + 1
27 25 26 syl X T Comp x X x + 1
28 27 rexrd X T Comp x X x + 1 *
29 1 cnfldtopn J = MetOpen abs
30 29 blopn abs ∞Met 0 x + 1 * 0 ball abs x + 1 J
31 22 23 28 30 mp3an2i X T Comp x X 0 ball abs x + 1 J
32 elrestr J Top X V 0 ball abs x + 1 J 0 ball abs x + 1 X J 𝑡 X
33 11 21 31 32 mp3an2i X T Comp x X 0 ball abs x + 1 X J 𝑡 X
34 33 2 eleqtrrdi X T Comp x X 0 ball abs x + 1 X T
35 0cn 0
36 eqid abs = abs
37 36 cnmetdval 0 x 0 abs x = 0 x
38 35 37 mpan x 0 abs x = 0 x
39 df-neg x = 0 x
40 39 fveq2i x = 0 x
41 absneg x x = x
42 40 41 eqtr3id x 0 x = x
43 38 42 eqtrd x 0 abs x = x
44 24 43 syl X T Comp x X 0 abs x = x
45 25 ltp1d X T Comp x X x < x + 1
46 44 45 eqbrtrd X T Comp x X 0 abs x < x + 1
47 elbl abs ∞Met 0 x + 1 * x 0 ball abs x + 1 x 0 abs x < x + 1
48 22 23 28 47 mp3an2i X T Comp x X x 0 ball abs x + 1 x 0 abs x < x + 1
49 24 46 48 mpbir2and X T Comp x X x 0 ball abs x + 1
50 simpr X T Comp x X x X
51 49 50 elind X T Comp x X x 0 ball abs x + 1 X
52 24 absge0d X T Comp x X 0 x
53 25 52 ge0p1rpd X T Comp x X x + 1 +
54 eqid 0 ball abs x + 1 X = 0 ball abs x + 1 X
55 oveq2 r = x + 1 0 ball abs r = 0 ball abs x + 1
56 55 ineq1d r = x + 1 0 ball abs r X = 0 ball abs x + 1 X
57 56 rspceeqv x + 1 + 0 ball abs x + 1 X = 0 ball abs x + 1 X r + 0 ball abs x + 1 X = 0 ball abs r X
58 53 54 57 sylancl X T Comp x X r + 0 ball abs x + 1 X = 0 ball abs r X
59 eleq2 u = 0 ball abs x + 1 X x u x 0 ball abs x + 1 X
60 eqeq1 u = 0 ball abs x + 1 X u = 0 ball abs r X 0 ball abs x + 1 X = 0 ball abs r X
61 60 rexbidv u = 0 ball abs x + 1 X r + u = 0 ball abs r X r + 0 ball abs x + 1 X = 0 ball abs r X
62 59 61 anbi12d u = 0 ball abs x + 1 X x u r + u = 0 ball abs r X x 0 ball abs x + 1 X r + 0 ball abs x + 1 X = 0 ball abs r X
63 62 rspcev 0 ball abs x + 1 X T x 0 ball abs x + 1 X r + 0 ball abs x + 1 X = 0 ball abs r X u T x u r + u = 0 ball abs r X
64 34 51 58 63 syl12anc X T Comp x X u T x u r + u = 0 ball abs r X
65 17 64 syldan X T Comp x T u T x u r + u = 0 ball abs r X
66 65 ralrimiva X T Comp x T u T x u r + u = 0 ball abs r X
67 eqid T = T
68 oveq2 r = f u 0 ball abs r = 0 ball abs f u
69 68 ineq1d r = f u 0 ball abs r X = 0 ball abs f u X
70 69 eqeq2d r = f u u = 0 ball abs r X u = 0 ball abs f u X
71 67 70 cmpcovf T Comp x T u T x u r + u = 0 ball abs r X s 𝒫 T Fin T = s f f : s + u s u = 0 ball abs f u X
72 5 66 71 syl2anc X T Comp s 𝒫 T Fin T = s f f : s + u s u = 0 ball abs f u X
73 15 ad4antr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r X = T
74 simpllr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r T = s
75 73 74 eqtrd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r X = s
76 75 eleq2d X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r x X x s
77 eluni2 x s z s x z
78 76 77 bitrdi X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r x X z s x z
79 elssuni z s z s
80 79 ad2antrl X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z z s
81 75 adantr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z X = s
82 80 81 sseqtrrd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z z X
83 simp-6l X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z X
84 82 83 sstrd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z z
85 simprr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x z
86 84 85 sseldd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x
87 86 abscld X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x
88 simplrl X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z r
89 simprl X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X f : s +
90 89 ad2antrr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z f : s +
91 simprl X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z z s
92 90 91 ffvelrnd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z f z +
93 92 rpred X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z f z
94 86 43 syl X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z 0 abs x = x
95 id u = z u = z
96 fveq2 u = z f u = f z
97 96 oveq2d u = z 0 ball abs f u = 0 ball abs f z
98 97 ineq1d u = z 0 ball abs f u X = 0 ball abs f z X
99 95 98 eqeq12d u = z u = 0 ball abs f u X z = 0 ball abs f z X
100 simprr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X u s u = 0 ball abs f u X
101 100 ad2antrr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z u s u = 0 ball abs f u X
102 99 101 91 rspcdva X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z z = 0 ball abs f z X
103 85 102 eleqtrd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x 0 ball abs f z X
104 103 elin1d X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x 0 ball abs f z
105 0cnd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z 0
106 92 rpxrd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z f z *
107 elbl abs ∞Met 0 f z * x 0 ball abs f z x 0 abs x < f z
108 22 105 106 107 mp3an2i X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x 0 ball abs f z x 0 abs x < f z
109 104 108 mpbid X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x 0 abs x < f z
110 109 simprd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z 0 abs x < f z
111 94 110 eqbrtrrd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x < f z
112 96 breq1d u = z f u r f z r
113 simplrr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z u s f u r
114 112 113 91 rspcdva X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z f z r
115 87 93 88 111 114 ltletrd X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x < r
116 87 88 115 ltled X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x r
117 116 rexlimdvaa X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r z s x z x r
118 78 117 sylbid X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r x X x r
119 118 ralrimiv X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r x X x r
120 simpllr X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X s 𝒫 T Fin
121 120 elin2d X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X s Fin
122 ffvelrn f : s + u s f u +
123 122 rpred f : s + u s f u
124 123 ralrimiva f : s + u s f u
125 124 ad2antrl X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X u s f u
126 fimaxre3 s Fin u s f u r u s f u r
127 121 125 126 syl2anc X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r u s f u r
128 119 127 reximddv X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r x X x r
129 128 ex X T Comp s 𝒫 T Fin T = s f : s + u s u = 0 ball abs f u X r x X x r
130 129 exlimdv X T Comp s 𝒫 T Fin T = s f f : s + u s u = 0 ball abs f u X r x X x r
131 130 expimpd X T Comp s 𝒫 T Fin T = s f f : s + u s u = 0 ball abs f u X r x X x r
132 131 rexlimdva X T Comp s 𝒫 T Fin T = s f f : s + u s u = 0 ball abs f u X r x X x r
133 72 132 mpd X T Comp r x X x r
134 10 133 jca X T Comp X Clsd J r x X x r
135 eqid y , z y + i z = y , z y + i z
136 eqid y , z y + i z r r × r r = y , z y + i z r r × r r
137 1 2 135 136 cnheiborlem X Clsd J r x X x r T Comp
138 137 rexlimdvaa X Clsd J r x X x r T Comp
139 138 imp X Clsd J r x X x r T Comp
140 139 adantl X X Clsd J r x X x r T Comp
141 134 140 impbida X T Comp X Clsd J r x X x r