Step | Hyp | Ref
| Expression |
1 | | iftrue 4092 |
. . . . . . . . . . 11
|
2 | 1 | fveq2d 6195 |
. . . . . . . . . 10
|
3 | 2 | adantl 482 |
. . . . . . . . 9
|
4 | | 2cn 11091 |
. . . . . . . . . . . . 13
|
5 | | 0re 10040 |
. . . . . . . . . . . . . . . . 17
|
6 | | 1re 10039 |
. . . . . . . . . . . . . . . . 17
|
7 | 5, 6 | elicc2i 12239 |
. . . . . . . . . . . . . . . 16
|
8 | 7 | simp1bi 1076 |
. . . . . . . . . . . . . . 15
|
9 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
|
10 | 9 | recnd 10068 |
. . . . . . . . . . . . 13
|
11 | | mulcom 10022 |
. . . . . . . . . . . . 13
|
12 | 4, 10, 11 | sylancr 695 |
. . . . . . . . . . . 12
|
13 | 7 | simp2bi 1077 |
. . . . . . . . . . . . . . 15
|
14 | 13 | adantr 481 |
. . . . . . . . . . . . . 14
|
15 | | simpr 477 |
. . . . . . . . . . . . . 14
|
16 | | 4nn 11187 |
. . . . . . . . . . . . . . . 16
|
17 | | nnrecre 11057 |
. . . . . . . . . . . . . . . 16
|
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
19 | 5, 18 | elicc2i 12239 |
. . . . . . . . . . . . . 14
|
20 | 9, 14, 15, 19 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
|
21 | | 2rp 11837 |
. . . . . . . . . . . . . 14
|
22 | 4 | mul02i 10225 |
. . . . . . . . . . . . . 14
|
23 | 18 | recni 10052 |
. . . . . . . . . . . . . . 15
|
24 | 23 | 2timesi 11147 |
. . . . . . . . . . . . . . . 16
|
25 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | | recdiv2 10738 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | 4, 25, 4, 25, 26 | mp4an 709 |
. . . . . . . . . . . . . . . . . . 19
|
28 | | 2t2e4 11177 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 28 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 27, 29 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
31 | 30, 30 | oveq12i 6662 |
. . . . . . . . . . . . . . . . 17
|
32 | | halfcn 11247 |
. . . . . . . . . . . . . . . . . 18
|
33 | | 2halves 11260 |
. . . . . . . . . . . . . . . . . 18
|
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
35 | 31, 34 | eqtr3i 2646 |
. . . . . . . . . . . . . . . 16
|
36 | 24, 35 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
37 | 4, 23, 36 | mulcomli 10047 |
. . . . . . . . . . . . . 14
|
38 | 5, 18, 21, 22, 37 | iccdili 12311 |
. . . . . . . . . . . . 13
|
39 | 20, 38 | syl 17 |
. . . . . . . . . . . 12
|
40 | 12, 39 | eqeltrd 2701 |
. . . . . . . . . . 11
|
41 | | pcoass.2 |
. . . . . . . . . . . . 13
|
42 | | pcoass.3 |
. . . . . . . . . . . . . 14
|
43 | | pcoass.4 |
. . . . . . . . . . . . . 14
|
44 | | pcoass.6 |
. . . . . . . . . . . . . 14
|
45 | 42, 43, 44 | pcocn 22817 |
. . . . . . . . . . . . 13
|
46 | 41, 45 | pcoval1 22813 |
. . . . . . . . . . . 12
|
47 | 41, 42 | pcoval1 22813 |
. . . . . . . . . . . 12
|
48 | 46, 47 | eqtr4d 2659 |
. . . . . . . . . . 11
|
49 | 40, 48 | sylan2 491 |
. . . . . . . . . 10
|
50 | 49 | anassrs 680 |
. . . . . . . . 9
|
51 | 3, 50 | eqtrd 2656 |
. . . . . . . 8
|
52 | 51 | adantlr 751 |
. . . . . . 7
|
53 | | simplll 798 |
. . . . . . . . . 10
|
54 | 8 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
55 | 54 | adantr 481 |
. . . . . . . . . . . 12
|
56 | | letric 10137 |
. . . . . . . . . . . . . 14
|
57 | 54, 18, 56 | sylancl 694 |
. . . . . . . . . . . . 13
|
58 | 57 | orcanai 952 |
. . . . . . . . . . . 12
|
59 | | simplr 792 |
. . . . . . . . . . . 12
|
60 | | halfre 11246 |
. . . . . . . . . . . . 13
|
61 | 18, 60 | elicc2i 12239 |
. . . . . . . . . . . 12
|
62 | 55, 58, 59, 61 | syl3anbrc 1246 |
. . . . . . . . . . 11
|
63 | 61 | simp1bi 1076 |
. . . . . . . . . . . . 13
|
64 | | readdcl 10019 |
. . . . . . . . . . . . 13
|
65 | 63, 18, 64 | sylancl 694 |
. . . . . . . . . . . 12
|
66 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
|
67 | 61 | simp2bi 1077 |
. . . . . . . . . . . . . 14
|
68 | 66, 63, 66, 67 | leadd1dd 10641 |
. . . . . . . . . . . . 13
|
69 | 35, 68 | syl5eqbrr 4689 |
. . . . . . . . . . . 12
|
70 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
|
71 | 61 | simp3bi 1078 |
. . . . . . . . . . . . . 14
|
72 | | 2lt4 11198 |
. . . . . . . . . . . . . . . . 17
|
73 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
|
74 | | 4re 11097 |
. . . . . . . . . . . . . . . . . 18
|
75 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . 18
|
76 | | 4pos 11116 |
. . . . . . . . . . . . . . . . . 18
|
77 | 73, 74, 75, 76 | ltrecii 10940 |
. . . . . . . . . . . . . . . . 17
|
78 | 72, 77 | mpbi 220 |
. . . . . . . . . . . . . . . 16
|
79 | 18, 60, 78 | ltleii 10160 |
. . . . . . . . . . . . . . 15
|
80 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
|
81 | 63, 66, 70, 70, 71, 80 | le2addd 10646 |
. . . . . . . . . . . . 13
|
82 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
|
83 | | 2halves 11260 |
. . . . . . . . . . . . . 14
|
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . . . 13
|
85 | 81, 84 | syl6breq 4694 |
. . . . . . . . . . . 12
|
86 | 60, 6 | elicc2i 12239 |
. . . . . . . . . . . 12
|
87 | 65, 69, 85, 86 | syl3anbrc 1246 |
. . . . . . . . . . 11
|
88 | 62, 87 | syl 17 |
. . . . . . . . . 10
|
89 | | pcoass.5 |
. . . . . . . . . . . 12
|
90 | 42, 43 | pco0 22814 |
. . . . . . . . . . . 12
|
91 | 89, 90 | eqtr4d 2659 |
. . . . . . . . . . 11
|
92 | 41, 45, 91 | pcoval2 22816 |
. . . . . . . . . 10
|
93 | 53, 88, 92 | syl2anc 693 |
. . . . . . . . 9
|
94 | 84 | oveq2i 6661 |
. . . . . . . . . . . 12
|
95 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
|
96 | 55 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
97 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
|
98 | 95, 96, 97 | adddid 10064 |
. . . . . . . . . . . . . 14
|
99 | 36 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
100 | 98, 99 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
101 | 100 | oveq1d 6665 |
. . . . . . . . . . . 12
|
102 | 94, 101 | syl5eqr 2670 |
. . . . . . . . . . 11
|
103 | | remulcl 10021 |
. . . . . . . . . . . . . 14
|
104 | 73, 55, 103 | sylancr 695 |
. . . . . . . . . . . . 13
|
105 | 104 | recnd 10068 |
. . . . . . . . . . . 12
|
106 | 32 | a1i 11 |
. . . . . . . . . . . 12
|
107 | 105, 106,
106 | pnpcan2d 10430 |
. . . . . . . . . . 11
|
108 | 102, 107 | eqtrd 2656 |
. . . . . . . . . 10
|
109 | 108 | fveq2d 6195 |
. . . . . . . . 9
|
110 | 4, 96, 11 | sylancr 695 |
. . . . . . . . . . . . 13
|
111 | 82, 4, 25 | divcan1i 10769 |
. . . . . . . . . . . . . . 15
|
112 | 18, 60, 21, 37, 111 | iccdili 12311 |
. . . . . . . . . . . . . 14
|
113 | 62, 112 | syl 17 |
. . . . . . . . . . . . 13
|
114 | 110, 113 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
115 | 32 | subidi 10352 |
. . . . . . . . . . . . 13
|
116 | | 1mhlfehlf 11251 |
. . . . . . . . . . . . 13
|
117 | 60, 6, 60, 115, 116 | iccshftli 12309 |
. . . . . . . . . . . 12
|
118 | 114, 117 | syl 17 |
. . . . . . . . . . 11
|
119 | 42, 43 | pcoval1 22813 |
. . . . . . . . . . 11
|
120 | 53, 118, 119 | syl2anc 693 |
. . . . . . . . . 10
|
121 | 95, 105, 106 | subdid 10486 |
. . . . . . . . . . . 12
|
122 | 4, 25 | recidi 10756 |
. . . . . . . . . . . . 13
|
123 | 122 | oveq2i 6661 |
. . . . . . . . . . . 12
|
124 | 121, 123 | syl6eq 2672 |
. . . . . . . . . . 11
|
125 | 124 | fveq2d 6195 |
. . . . . . . . . 10
|
126 | 120, 125 | eqtrd 2656 |
. . . . . . . . 9
|
127 | 93, 109, 126 | 3eqtrd 2660 |
. . . . . . . 8
|
128 | | iffalse 4095 |
. . . . . . . . . 10
|
129 | 128 | fveq2d 6195 |
. . . . . . . . 9
|
130 | 129 | adantl 482 |
. . . . . . . 8
|
131 | 41, 42, 89 | pcoval2 22816 |
. . . . . . . . 9
|
132 | 53, 114, 131 | syl2anc 693 |
. . . . . . . 8
|
133 | 127, 130,
132 | 3eqtr4d 2666 |
. . . . . . 7
|
134 | 52, 133 | pm2.61dan 832 |
. . . . . 6
|
135 | | iftrue 4092 |
. . . . . . . 8
|
136 | 135 | fveq2d 6195 |
. . . . . . 7
|
137 | 136 | adantl 482 |
. . . . . 6
|
138 | | iftrue 4092 |
. . . . . . 7
|
139 | 138 | adantl 482 |
. . . . . 6
|
140 | 134, 137,
139 | 3eqtr4d 2666 |
. . . . 5
|
141 | | elii2 22735 |
. . . . . . . 8
|
142 | | halfgt0 11248 |
. . . . . . . . . . . . . . 15
|
143 | 5, 60, 142 | ltleii 10160 |
. . . . . . . . . . . . . 14
|
144 | | halflt1 11250 |
. . . . . . . . . . . . . . 15
|
145 | 60, 6, 144 | ltleii 10160 |
. . . . . . . . . . . . . 14
|
146 | 5, 6 | elicc2i 12239 |
. . . . . . . . . . . . . 14
|
147 | 60, 143, 145, 146 | mpbir3an 1244 |
. . . . . . . . . . . . 13
|
148 | | 1elunit 12291 |
. . . . . . . . . . . . 13
|
149 | | iccss2 12244 |
. . . . . . . . . . . . 13
|
150 | 147, 148,
149 | mp2an 708 |
. . . . . . . . . . . 12
|
151 | 150 | sseli 3599 |
. . . . . . . . . . 11
|
152 | 4, 25 | div0i 10759 |
. . . . . . . . . . . 12
|
153 | | eqid 2622 |
. . . . . . . . . . . 12
|
154 | 5, 6, 21, 152, 153 | icccntri 12313 |
. . . . . . . . . . 11
|
155 | 32 | addid2i 10224 |
. . . . . . . . . . . 12
|
156 | 5, 60, 60, 155, 84 | iccshftri 12307 |
. . . . . . . . . . 11
|
157 | 151, 154,
156 | 3syl 18 |
. . . . . . . . . 10
|
158 | 41, 45, 91 | pcoval2 22816 |
. . . . . . . . . 10
|
159 | 157, 158 | sylan2 491 |
. . . . . . . . 9
|
160 | 60, 6 | elicc2i 12239 |
. . . . . . . . . . . . . . . . . 18
|
161 | 160 | simp1bi 1076 |
. . . . . . . . . . . . . . . . 17
|
162 | 161 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
163 | 82 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
164 | | 2cnd 11093 |
. . . . . . . . . . . . . . . 16
|
165 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
166 | 162, 163,
164, 165 | divdird 10839 |
. . . . . . . . . . . . . . 15
|
167 | 166 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
168 | | peano2cn 10208 |
. . . . . . . . . . . . . . . 16
|
169 | 162, 168 | syl 17 |
. . . . . . . . . . . . . . 15
|
170 | 169, 164,
165 | divcan2d 10803 |
. . . . . . . . . . . . . 14
|
171 | 167, 170 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
172 | 171 | oveq1d 6665 |
. . . . . . . . . . . 12
|
173 | | pncan 10287 |
. . . . . . . . . . . . 13
|
174 | 162, 82, 173 | sylancl 694 |
. . . . . . . . . . . 12
|
175 | 172, 174 | eqtrd 2656 |
. . . . . . . . . . 11
|
176 | 175 | fveq2d 6195 |
. . . . . . . . . 10
|
177 | 176 | adantl 482 |
. . . . . . . . 9
|
178 | 42, 43, 44 | pcoval2 22816 |
. . . . . . . . 9
|
179 | 159, 177,
178 | 3eqtrd 2660 |
. . . . . . . 8
|
180 | 141, 179 | sylan2 491 |
. . . . . . 7
|
181 | 180 | anassrs 680 |
. . . . . 6
|
182 | | iffalse 4095 |
. . . . . . . 8
|
183 | 182 | fveq2d 6195 |
. . . . . . 7
|
184 | 183 | adantl 482 |
. . . . . 6
|
185 | | iffalse 4095 |
. . . . . . 7
|
186 | 185 | adantl 482 |
. . . . . 6
|
187 | 181, 184,
186 | 3eqtr4d 2666 |
. . . . 5
|
188 | 140, 187 | pm2.61dan 832 |
. . . 4
|
189 | 188 | mpteq2dva 4744 |
. . 3
|
190 | | pcoass.7 |
. . . . . . 7
|
191 | | iitopon 22682 |
. . . . . . . . 9
TopOn |
192 | 191 | a1i 11 |
. . . . . . . 8
TopOn |
193 | 192 | cnmptid 21464 |
. . . . . . . 8
|
194 | | 0elunit 12290 |
. . . . . . . . . 10
|
195 | 194 | a1i 11 |
. . . . . . . . 9
|
196 | 192, 192,
195 | cnmptc 21465 |
. . . . . . . 8
|
197 | | eqid 2622 |
. . . . . . . . 9
|
198 | | eqid 2622 |
. . . . . . . . 9
↾t ↾t |
199 | | eqid 2622 |
. . . . . . . . 9
↾t ↾t |
200 | | dfii2 22685 |
. . . . . . . . 9
↾t |
201 | | 0red 10041 |
. . . . . . . . 9
|
202 | | 1red 10055 |
. . . . . . . . 9
|
203 | 147 | a1i 11 |
. . . . . . . . 9
|
204 | | simprl 794 |
. . . . . . . . . . . 12
|
205 | 204 | oveq1d 6665 |
. . . . . . . . . . 11
|
206 | 32, 23 | addcomi 10227 |
. . . . . . . . . . 11
|
207 | 205, 206 | syl6eq 2672 |
. . . . . . . . . 10
|
208 | 18, 60 | ltnlei 10158 |
. . . . . . . . . . . . 13
|
209 | 78, 208 | mpbi 220 |
. . . . . . . . . . . 12
|
210 | 204 | breq1d 4663 |
. . . . . . . . . . . 12
|
211 | 209, 210 | mtbiri 317 |
. . . . . . . . . . 11
|
212 | 211 | iffalsed 4097 |
. . . . . . . . . 10
|
213 | 204 | oveq1d 6665 |
. . . . . . . . . . . 12
|
214 | 213, 30 | syl6eq 2672 |
. . . . . . . . . . 11
|
215 | 214 | oveq1d 6665 |
. . . . . . . . . 10
|
216 | 207, 212,
215 | 3eqtr4d 2666 |
. . . . . . . . 9
|
217 | | eqid 2622 |
. . . . . . . . . 10
↾t ↾t |
218 | | eqid 2622 |
. . . . . . . . . 10
↾t ↾t |
219 | 60 | a1i 11 |
. . . . . . . . . 10
|
220 | 74, 76 | recgt0ii 10929 |
. . . . . . . . . . . . 13
|
221 | 5, 18, 220 | ltleii 10160 |
. . . . . . . . . . . 12
|
222 | 5, 60 | elicc2i 12239 |
. . . . . . . . . . . 12
|
223 | 18, 221, 79, 222 | mpbir3an 1244 |
. . . . . . . . . . 11
|
224 | 223 | a1i 11 |
. . . . . . . . . 10
|
225 | | simprl 794 |
. . . . . . . . . . . 12
|
226 | 225 | oveq2d 6666 |
. . . . . . . . . . 11
|
227 | 225 | oveq1d 6665 |
. . . . . . . . . . 11
|
228 | 24, 226, 227 | 3eqtr4a 2682 |
. . . . . . . . . 10
|
229 | | retopon 22567 |
. . . . . . . . . . . . 13
TopOn |
230 | | 0xr 10086 |
. . . . . . . . . . . . . . . 16
|
231 | 60 | rexri 10097 |
. . . . . . . . . . . . . . . 16
|
232 | | lbicc2 12288 |
. . . . . . . . . . . . . . . 16
|
233 | 230, 231,
143, 232 | mp3an 1424 |
. . . . . . . . . . . . . . 15
|
234 | | iccss2 12244 |
. . . . . . . . . . . . . . 15
|
235 | 233, 223,
234 | mp2an 708 |
. . . . . . . . . . . . . 14
|
236 | | iccssre 12255 |
. . . . . . . . . . . . . . 15
|
237 | 5, 60, 236 | mp2an 708 |
. . . . . . . . . . . . . 14
|
238 | 235, 237 | sstri 3612 |
. . . . . . . . . . . . 13
|
239 | | resttopon 20965 |
. . . . . . . . . . . . 13
TopOn
↾t TopOn |
240 | 229, 238,
239 | mp2an 708 |
. . . . . . . . . . . 12
↾t TopOn |
241 | 240 | a1i 11 |
. . . . . . . . . . 11
↾t TopOn |
242 | 241, 192 | cnmpt1st 21471 |
. . . . . . . . . . 11
↾t
↾t |
243 | | retop 22565 |
. . . . . . . . . . . . . 14
|
244 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
245 | | restabs 20969 |
. . . . . . . . . . . . . 14
↾t
↾t ↾t |
246 | 243, 235,
244, 245 | mp3an 1424 |
. . . . . . . . . . . . 13
↾t ↾t ↾t |
247 | 246 | eqcomi 2631 |
. . . . . . . . . . . 12
↾t ↾t ↾t |
248 | | resttopon 20965 |
. . . . . . . . . . . . . 14
TopOn
↾t TopOn |
249 | 229, 237,
248 | mp2an 708 |
. . . . . . . . . . . . 13
↾t TopOn |
250 | 249 | a1i 11 |
. . . . . . . . . . . 12
↾t TopOn |
251 | 235 | a1i 11 |
. . . . . . . . . . . 12
|
252 | 198 | iihalf1cn 22731 |
. . . . . . . . . . . . 13
↾t |
253 | 252 | a1i 11 |
. . . . . . . . . . . 12
↾t |
254 | 247, 250,
251, 253 | cnmpt1res 21479 |
. . . . . . . . . . 11
↾t |
255 | | oveq2 6658 |
. . . . . . . . . . 11
|
256 | 241, 192,
242, 241, 254, 255 | cnmpt21 21474 |
. . . . . . . . . 10
↾t
|
257 | | iccssre 12255 |
. . . . . . . . . . . . . 14
|
258 | 18, 60, 257 | mp2an 708 |
. . . . . . . . . . . . 13
|
259 | | resttopon 20965 |
. . . . . . . . . . . . 13
TopOn
↾t TopOn |
260 | 229, 258,
259 | mp2an 708 |
. . . . . . . . . . . 12
↾t TopOn |
261 | 260 | a1i 11 |
. . . . . . . . . . 11
↾t TopOn |
262 | 261, 192 | cnmpt1st 21471 |
. . . . . . . . . . 11
↾t
↾t |
263 | | eqid 2622 |
. . . . . . . . . . . 12
ℂfld ℂfld |
264 | 258 | a1i 11 |
. . . . . . . . . . . 12
|
265 | | unitssre 12319 |
. . . . . . . . . . . . 13
|
266 | 265 | a1i 11 |
. . . . . . . . . . . 12
|
267 | 150, 87 | sseldi 3601 |
. . . . . . . . . . . . 13
|
268 | 267 | adantl 482 |
. . . . . . . . . . . 12
|
269 | 263 | cnfldtopon 22586 |
. . . . . . . . . . . . . 14
ℂfld TopOn |
270 | 269 | a1i 11 |
. . . . . . . . . . . . 13
ℂfld
TopOn |
271 | 270 | cnmptid 21464 |
. . . . . . . . . . . . 13
ℂfld
ℂfld |
272 | 18 | a1i 11 |
. . . . . . . . . . . . . . 15
|
273 | 272 | recnd 10068 |
. . . . . . . . . . . . . 14
|
274 | 270, 270,
273 | cnmptc 21465 |
. . . . . . . . . . . . 13
ℂfld
ℂfld |
275 | 263 | addcn 22668 |
. . . . . . . . . . . . . 14
ℂfld ℂfld ℂfld |
276 | 275 | a1i 11 |
. . . . . . . . . . . . 13
ℂfld
ℂfld ℂfld |
277 | 270, 271,
274, 276 | cnmpt12f 21469 |
. . . . . . . . . . . 12
ℂfld
ℂfld |
278 | 263, 218,
200, 264, 266, 268, 277 | cnmptre 22726 |
. . . . . . . . . . 11
↾t |
279 | | oveq1 6657 |
. . . . . . . . . . 11
|
280 | 261, 192,
262, 261, 278, 279 | cnmpt21 21474 |
. . . . . . . . . 10
↾t
|
281 | 197, 217,
218, 198, 201, 219, 224, 192, 228, 256, 280 | cnmpt2pc 22727 |
. . . . . . . . 9
↾t |
282 | | iccssre 12255 |
. . . . . . . . . . . . 13
|
283 | 60, 6, 282 | mp2an 708 |
. . . . . . . . . . . 12
|
284 | | resttopon 20965 |
. . . . . . . . . . . 12
TopOn
↾t TopOn |
285 | 229, 283,
284 | mp2an 708 |
. . . . . . . . . . 11
↾t TopOn |
286 | 285 | a1i 11 |
. . . . . . . . . 10
↾t TopOn |
287 | 286, 192 | cnmpt1st 21471 |
. . . . . . . . . 10
↾t
↾t |
288 | 283 | a1i 11 |
. . . . . . . . . . 11
|
289 | 150, 157 | sseldi 3601 |
. . . . . . . . . . . 12
|
290 | 289 | adantl 482 |
. . . . . . . . . . 11
|
291 | 263 | divccn 22676 |
. . . . . . . . . . . . . 14
ℂfld
ℂfld |
292 | 4, 25, 291 | mp2an 708 |
. . . . . . . . . . . . 13
ℂfld ℂfld |
293 | 292 | a1i 11 |
. . . . . . . . . . . 12
ℂfld
ℂfld |
294 | 32 | a1i 11 |
. . . . . . . . . . . . 13
|
295 | 270, 270,
294 | cnmptc 21465 |
. . . . . . . . . . . 12
ℂfld
ℂfld |
296 | 270, 293,
295, 276 | cnmpt12f 21469 |
. . . . . . . . . . 11
ℂfld
ℂfld |
297 | 263, 199,
200, 288, 266, 290, 296 | cnmptre 22726 |
. . . . . . . . . 10
↾t |
298 | | oveq1 6657 |
. . . . . . . . . . 11
|
299 | 298 | oveq1d 6665 |
. . . . . . . . . 10
|
300 | 286, 192,
287, 286, 297, 299 | cnmpt21 21474 |
. . . . . . . . 9
↾t
|
301 | 197, 198,
199, 200, 201, 202, 203, 192, 216, 281, 300 | cnmpt2pc 22727 |
. . . . . . . 8
|
302 | | breq1 4656 |
. . . . . . . . . . . 12
|
303 | | breq1 4656 |
. . . . . . . . . . . . 13
|
304 | 303, 255,
279 | ifbieq12d 4113 |
. . . . . . . . . . . 12
|
305 | 302, 304,
299 | ifbieq12d 4113 |
. . . . . . . . . . 11
|
306 | 305 | equcoms 1947 |
. . . . . . . . . 10
|
307 | 306 | adantr 481 |
. . . . . . . . 9
|
308 | 307 | eqcomd 2628 |
. . . . . . . 8
|
309 | 192, 193,
196, 192, 192, 301, 308 | cnmpt12 21470 |
. . . . . . 7
|
310 | 190, 309 | syl5eqel 2705 |
. . . . . 6
|
311 | | iiuni 22684 |
. . . . . . 7
|
312 | 311, 311 | cnf 21050 |
. . . . . 6
|
313 | 310, 312 | syl 17 |
. . . . 5
|
314 | 190 | fmpt 6381 |
. . . . 5
|
315 | 313, 314 | sylibr 224 |
. . . 4
|
316 | 190 | a1i 11 |
. . . 4
|
317 | 41, 45, 91 | pcocn 22817 |
. . . . . 6
|
318 | | eqid 2622 |
. . . . . . 7
|
319 | 311, 318 | cnf 21050 |
. . . . . 6
|
320 | 317, 319 | syl 17 |
. . . . 5
|
321 | 320 | feqmptd 6249 |
. . . 4
|
322 | | fveq2 6191 |
. . . 4
|
323 | 315, 316,
321, 322 | fmptcof 6397 |
. . 3
|
324 | 41, 42, 89 | pcocn 22817 |
. . . 4
|
325 | 324, 43 | pcoval 22811 |
. . 3
|
326 | 189, 323,
325 | 3eqtr4rd 2667 |
. 2
|
327 | | id 22 |
. . . . . . . 8
|
328 | 327, 143 | syl6eqbr 4692 |
. . . . . . 7
|
329 | 328 | iftrued 4094 |
. . . . . 6
|
330 | 327, 221 | syl6eqbr 4692 |
. . . . . . 7
|
331 | 330 | iftrued 4094 |
. . . . . 6
|
332 | | oveq2 6658 |
. . . . . . 7
|
333 | | 2t0e0 11183 |
. . . . . . 7
|
334 | 332, 333 | syl6eq 2672 |
. . . . . 6
|
335 | 329, 331,
334 | 3eqtrd 2660 |
. . . . 5
|
336 | | c0ex 10034 |
. . . . 5
|
337 | 335, 190,
336 | fvmpt 6282 |
. . . 4
|
338 | 195, 337 | syl 17 |
. . 3
|
339 | 148 | a1i 11 |
. . . 4
|
340 | 60, 6 | ltnlei 10158 |
. . . . . . . . 9
|
341 | 144, 340 | mpbi 220 |
. . . . . . . 8
|
342 | | breq1 4656 |
. . . . . . . 8
|
343 | 341, 342 | mtbiri 317 |
. . . . . . 7
|
344 | 343 | iffalsed 4097 |
. . . . . 6
|
345 | | oveq1 6657 |
. . . . . . . 8
|
346 | 345 | oveq1d 6665 |
. . . . . . 7
|
347 | 346, 84 | syl6eq 2672 |
. . . . . 6
|
348 | 344, 347 | eqtrd 2656 |
. . . . 5
|
349 | | 1ex 10035 |
. . . . 5
|
350 | 348, 190,
349 | fvmpt 6282 |
. . . 4
|
351 | 339, 350 | syl 17 |
. . 3
|
352 | 317, 310,
338, 351 | reparpht 22798 |
. 2
|
353 | 326, 352 | eqbrtrd 4675 |
1
|