Step | Hyp | Ref
| Expression |
1 | | bndth.1 |
. . . . 5
|
2 | | bndth.2 |
. . . . 5
|
3 | | bndth.3 |
. . . . . 6
|
4 | 3 | adantr 481 |
. . . . 5
|
5 | | cmptop 21198 |
. . . . . . . . . 10
|
6 | 4, 5 | syl 17 |
. . . . . . . . 9
|
7 | 1 | toptopon 20722 |
. . . . . . . . 9
TopOn |
8 | 6, 7 | sylib 208 |
. . . . . . . 8
TopOn |
9 | | eqid 2622 |
. . . . . . . . . . 11
ℂfld ℂfld |
10 | 9 | cnfldtopon 22586 |
. . . . . . . . . 10
ℂfld TopOn |
11 | 10 | a1i 11 |
. . . . . . . . 9
ℂfld TopOn |
12 | | 1cnd 10056 |
. . . . . . . . 9
|
13 | 8, 11, 12 | cnmptc 21465 |
. . . . . . . 8
ℂfld |
14 | | bndth.4 |
. . . . . . . . . . . . . . . . 17
|
15 | | uniretop 22566 |
. . . . . . . . . . . . . . . . . . 19
|
16 | 2 | unieqi 4445 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 15, 16 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . . 18
|
18 | 1, 17 | cnf 21050 |
. . . . . . . . . . . . . . . . 17
|
19 | 14, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
|
20 | | frn 6053 |
. . . . . . . . . . . . . . . 16
|
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
|
22 | | fdm 6051 |
. . . . . . . . . . . . . . . . . 18
|
23 | 19, 22 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
24 | | evth.5 |
. . . . . . . . . . . . . . . . 17
|
25 | 23, 24 | eqnetrd 2861 |
. . . . . . . . . . . . . . . 16
|
26 | | dm0rn0 5342 |
. . . . . . . . . . . . . . . . 17
|
27 | 26 | necon3bii 2846 |
. . . . . . . . . . . . . . . 16
|
28 | 25, 27 | sylib 208 |
. . . . . . . . . . . . . . 15
|
29 | 1, 2, 3, 14 | bndth 22757 |
. . . . . . . . . . . . . . . 16
|
30 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
|
31 | 19, 30 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
32 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32 | ralrn 6362 |
. . . . . . . . . . . . . . . . . 18
|
34 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
35 | 34 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
|
36 | 29, 35 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
37 | 21, 28, 36 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
38 | | suprcl 10983 |
. . . . . . . . . . . . . 14
|
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
|
40 | 39 | recnd 10068 |
. . . . . . . . . . . 12
|
41 | 40 | adantr 481 |
. . . . . . . . . . 11
|
42 | 8, 11, 41 | cnmptc 21465 |
. . . . . . . . . 10
ℂfld |
43 | 19 | feqmptd 6249 |
. . . . . . . . . . . 12
|
44 | 9 | cnfldtop 22587 |
. . . . . . . . . . . . . 14
ℂfld |
45 | | cnrest2r 21091 |
. . . . . . . . . . . . . 14
ℂfld ℂfld ↾t
ℂfld |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
ℂfld ↾t ℂfld |
47 | 9 | tgioo2 22606 |
. . . . . . . . . . . . . . . 16
ℂfld
↾t |
48 | 2, 47 | eqtri 2644 |
. . . . . . . . . . . . . . 15
ℂfld
↾t |
49 | 48 | oveq2i 6661 |
. . . . . . . . . . . . . 14
ℂfld
↾t |
50 | 14, 49 | syl6eleq 2711 |
. . . . . . . . . . . . 13
ℂfld ↾t |
51 | 46, 50 | sseldi 3601 |
. . . . . . . . . . . 12
ℂfld |
52 | 43, 51 | eqeltrrd 2702 |
. . . . . . . . . . 11
ℂfld |
53 | 52 | adantr 481 |
. . . . . . . . . 10
ℂfld |
54 | 9 | subcn 22669 |
. . . . . . . . . . 11
ℂfld ℂfld ℂfld |
55 | 54 | a1i 11 |
. . . . . . . . . 10
ℂfld ℂfld ℂfld |
56 | 8, 42, 53, 55 | cnmpt12f 21469 |
. . . . . . . . 9
ℂfld |
57 | 39 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
58 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58 | adantll 750 |
. . . . . . . . . . . . . . . . 17
|
60 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . 17
|
61 | 59, 60 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
62 | 61 | simpld 475 |
. . . . . . . . . . . . . . 15
|
63 | 57, 62 | resubcld 10458 |
. . . . . . . . . . . . . 14
|
64 | 63 | recnd 10068 |
. . . . . . . . . . . . 13
|
65 | 57 | recnd 10068 |
. . . . . . . . . . . . . 14
|
66 | 62 | recnd 10068 |
. . . . . . . . . . . . . 14
|
67 | 61 | simprd 479 |
. . . . . . . . . . . . . . 15
|
68 | 67 | necomd 2849 |
. . . . . . . . . . . . . 14
|
69 | 65, 66, 68 | subne0d 10401 |
. . . . . . . . . . . . 13
|
70 | | eldifsn 4317 |
. . . . . . . . . . . . 13
|
71 | 64, 69, 70 | sylanbrc 698 |
. . . . . . . . . . . 12
|
72 | | eqid 2622 |
. . . . . . . . . . . 12
|
73 | 71, 72 | fmptd 6385 |
. . . . . . . . . . 11
|
74 | | frn 6053 |
. . . . . . . . . . 11
|
75 | 73, 74 | syl 17 |
. . . . . . . . . 10
|
76 | | difssd 3738 |
. . . . . . . . . 10
|
77 | | cnrest2 21090 |
. . . . . . . . . 10
ℂfld
TopOn
ℂfld
ℂfld ↾t |
78 | 11, 75, 76, 77 | syl3anc 1326 |
. . . . . . . . 9
ℂfld
ℂfld ↾t |
79 | 56, 78 | mpbid 222 |
. . . . . . . 8
ℂfld
↾t |
80 | | eqid 2622 |
. . . . . . . . . 10
ℂfld ↾t ℂfld ↾t |
81 | 9, 80 | divcn 22671 |
. . . . . . . . 9
ℂfld ℂfld
↾t ℂfld |
82 | 81 | a1i 11 |
. . . . . . . 8
ℂfld ℂfld
↾t ℂfld |
83 | 8, 13, 79, 82 | cnmpt12f 21469 |
. . . . . . 7
ℂfld |
84 | 63, 69 | rereccld 10852 |
. . . . . . . . . 10
|
85 | | eqid 2622 |
. . . . . . . . . 10
|
86 | 84, 85 | fmptd 6385 |
. . . . . . . . 9
|
87 | | frn 6053 |
. . . . . . . . 9
|
88 | 86, 87 | syl 17 |
. . . . . . . 8
|
89 | | ax-resscn 9993 |
. . . . . . . . 9
|
90 | 89 | a1i 11 |
. . . . . . . 8
|
91 | | cnrest2 21090 |
. . . . . . . 8
ℂfld
TopOn
ℂfld ℂfld ↾t |
92 | 11, 88, 90, 91 | syl3anc 1326 |
. . . . . . 7
ℂfld
ℂfld ↾t |
93 | 83, 92 | mpbid 222 |
. . . . . 6
ℂfld
↾t |
94 | 93, 49 | syl6eleqr 2712 |
. . . . 5
|
95 | 1, 2, 4, 94 | bndth 22757 |
. . . 4
|
96 | 39 | ad2antrr 762 |
. . . . . . . 8
|
97 | | simpr 477 |
. . . . . . . . . . 11
|
98 | | 1re 10039 |
. . . . . . . . . . 11
|
99 | | ifcl 4130 |
. . . . . . . . . . 11
|
100 | 97, 98, 99 | sylancl 694 |
. . . . . . . . . 10
|
101 | | 0red 10041 |
. . . . . . . . . . . 12
|
102 | 98 | a1i 11 |
. . . . . . . . . . . 12
|
103 | | 0lt1 10550 |
. . . . . . . . . . . . 13
|
104 | 103 | a1i 11 |
. . . . . . . . . . . 12
|
105 | | max1 12016 |
. . . . . . . . . . . . 13
|
106 | 98, 97, 105 | sylancr 695 |
. . . . . . . . . . . 12
|
107 | 101, 102,
100, 104, 106 | ltletrd 10197 |
. . . . . . . . . . 11
|
108 | 107 | gt0ne0d 10592 |
. . . . . . . . . 10
|
109 | 100, 108 | rereccld 10852 |
. . . . . . . . 9
|
110 | 100, 107 | recgt0d 10958 |
. . . . . . . . 9
|
111 | 109, 110 | elrpd 11869 |
. . . . . . . 8
|
112 | 96, 111 | ltsubrpd 11904 |
. . . . . . 7
|
113 | 96, 109 | resubcld 10458 |
. . . . . . . 8
|
114 | 113, 96 | ltnled 10184 |
. . . . . . 7
|
115 | 112, 114 | mpbid 222 |
. . . . . 6
|
116 | | simprl 794 |
. . . . . . . . . . . 12
|
117 | | max2 12018 |
. . . . . . . . . . . 12
|
118 | 98, 116, 117 | sylancr 695 |
. . . . . . . . . . 11
|
119 | 39 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
120 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
|
121 | 120 | ad2ant2l 782 |
. . . . . . . . . . . . . . . 16
|
122 | | eldifsn 4317 |
. . . . . . . . . . . . . . . 16
|
123 | 121, 122 | sylib 208 |
. . . . . . . . . . . . . . 15
|
124 | 123 | simpld 475 |
. . . . . . . . . . . . . 14
|
125 | 119, 124 | resubcld 10458 |
. . . . . . . . . . . . 13
|
126 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
127 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . 19
|
128 | 31, 127 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
|
129 | | suprub 10984 |
. . . . . . . . . . . . . . . . . 18
|
130 | 126, 128,
129 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
131 | 130 | ad2ant2rl 785 |
. . . . . . . . . . . . . . . 16
|
132 | 123 | simprd 479 |
. . . . . . . . . . . . . . . . 17
|
133 | 132 | necomd 2849 |
. . . . . . . . . . . . . . . 16
|
134 | 124, 119 | ltlend 10182 |
. . . . . . . . . . . . . . . 16
|
135 | 131, 133,
134 | mpbir2and 957 |
. . . . . . . . . . . . . . 15
|
136 | 124, 119 | posdifd 10614 |
. . . . . . . . . . . . . . 15
|
137 | 135, 136 | mpbid 222 |
. . . . . . . . . . . . . 14
|
138 | 137 | gt0ne0d 10592 |
. . . . . . . . . . . . 13
|
139 | 125, 138 | rereccld 10852 |
. . . . . . . . . . . 12
|
140 | 116, 98, 99 | sylancl 694 |
. . . . . . . . . . . 12
|
141 | | letr 10131 |
. . . . . . . . . . . 12
|
142 | 139, 116,
140, 141 | syl3anc 1326 |
. . . . . . . . . . 11
|
143 | 118, 142 | mpan2d 710 |
. . . . . . . . . 10
|
144 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
145 | 144 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
146 | 145 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
147 | | ovex 6678 |
. . . . . . . . . . . . 13
|
148 | 146, 85, 147 | fvmpt 6282 |
. . . . . . . . . . . 12
|
149 | 148 | breq1d 4663 |
. . . . . . . . . . 11
|
150 | 149 | ad2antll 765 |
. . . . . . . . . 10
|
151 | 109 | adantrr 753 |
. . . . . . . . . . . 12
|
152 | 107 | adantrr 753 |
. . . . . . . . . . . . 13
|
153 | 140, 152 | recgt0d 10958 |
. . . . . . . . . . . 12
|
154 | | lerec 10906 |
. . . . . . . . . . . 12
|
155 | 151, 153,
125, 137, 154 | syl22anc 1327 |
. . . . . . . . . . 11
|
156 | | lesub 10507 |
. . . . . . . . . . . 12
|
157 | 151, 119,
124, 156 | syl3anc 1326 |
. . . . . . . . . . 11
|
158 | 140 | recnd 10068 |
. . . . . . . . . . . . 13
|
159 | 108 | adantrr 753 |
. . . . . . . . . . . . 13
|
160 | 158, 159 | recrecd 10798 |
. . . . . . . . . . . 12
|
161 | 160 | breq2d 4665 |
. . . . . . . . . . 11
|
162 | 155, 157,
161 | 3bitr3d 298 |
. . . . . . . . . 10
|
163 | 143, 150,
162 | 3imtr4d 283 |
. . . . . . . . 9
|
164 | 163 | anassrs 680 |
. . . . . . . 8
|
165 | 164 | ralimdva 2962 |
. . . . . . 7
|
166 | 37 | ad2antrr 762 |
. . . . . . . . 9
|
167 | | suprleub 10989 |
. . . . . . . . 9
|
168 | 166, 113,
167 | syl2anc 693 |
. . . . . . . 8
|
169 | 31 | ad2antrr 762 |
. . . . . . . . 9
|
170 | | breq1 4656 |
. . . . . . . . . 10
|
171 | 170 | ralrn 6362 |
. . . . . . . . 9
|
172 | 169, 171 | syl 17 |
. . . . . . . 8
|
173 | 168, 172 | bitrd 268 |
. . . . . . 7
|
174 | 165, 173 | sylibrd 249 |
. . . . . 6
|
175 | 115, 174 | mtod 189 |
. . . . 5
|
176 | 175 | nrexdv 3001 |
. . . 4
|
177 | 95, 176 | pm2.65da 600 |
. . 3
|
178 | 130 | ralrimiva 2966 |
. . . . . . . . 9
|
179 | | breq2 4657 |
. . . . . . . . . 10
|
180 | 179 | ralbidv 2986 |
. . . . . . . . 9
|
181 | 178, 180 | syl5ibrcom 237 |
. . . . . . . 8
|
182 | 181 | necon3bd 2808 |
. . . . . . 7
|
183 | 182 | adantr 481 |
. . . . . 6
|
184 | 19 | ffvelrnda 6359 |
. . . . . . 7
|
185 | | eldifsn 4317 |
. . . . . . . 8
|
186 | 185 | baib 944 |
. . . . . . 7
|
187 | 184, 186 | syl 17 |
. . . . . 6
|
188 | 183, 187 | sylibrd 249 |
. . . . 5
|
189 | 188 | ralimdva 2962 |
. . . 4
|
190 | | ffnfv 6388 |
. . . . . 6
|
191 | 190 | baib 944 |
. . . . 5
|
192 | 31, 191 | syl 17 |
. . . 4
|
193 | 189, 192 | sylibrd 249 |
. . 3
|
194 | 177, 193 | mtod 189 |
. 2
|
195 | | dfrex2 2996 |
. 2
|
196 | 194, 195 | sylibr 224 |
1
|