Step |
Hyp |
Ref |
Expression |
1 |
|
dvadd.f |
|
2 |
|
dvadd.x |
|
3 |
|
dvadd.g |
|
4 |
|
dvadd.y |
|
5 |
|
dvaddbr.s |
|
6 |
|
dvadd.bf |
|
7 |
|
dvadd.bg |
|
8 |
|
dvadd.j |
|
9 |
|
eqid |
|
10 |
|
eqid |
|
11 |
9 8 10 5 1 2
|
eldv |
|
12 |
6 11
|
mpbid |
|
13 |
12
|
simpld |
|
14 |
|
eqid |
|
15 |
9 8 14 5 3 4
|
eldv |
|
16 |
7 15
|
mpbid |
|
17 |
16
|
simpld |
|
18 |
13 17
|
elind |
|
19 |
8
|
cnfldtopon |
|
20 |
|
resttopon |
|
21 |
19 5 20
|
sylancr |
|
22 |
|
topontop |
|
23 |
21 22
|
syl |
|
24 |
|
toponuni |
|
25 |
21 24
|
syl |
|
26 |
2 25
|
sseqtrd |
|
27 |
4 25
|
sseqtrd |
|
28 |
|
eqid |
|
29 |
28
|
ntrin |
|
30 |
23 26 27 29
|
syl3anc |
|
31 |
18 30
|
eleqtrrd |
|
32 |
1
|
adantr |
|
33 |
|
inss1 |
|
34 |
|
eldifi |
|
35 |
34
|
adantl |
|
36 |
33 35
|
sselid |
|
37 |
32 36
|
ffvelcdmd |
|
38 |
5 1 2
|
dvbss |
|
39 |
|
reldv |
|
40 |
|
releldm |
|
41 |
39 6 40
|
sylancr |
|
42 |
38 41
|
sseldd |
|
43 |
1 42
|
ffvelcdmd |
|
44 |
43
|
adantr |
|
45 |
37 44
|
subcld |
|
46 |
2 5
|
sstrd |
|
47 |
46
|
adantr |
|
48 |
47 36
|
sseldd |
|
49 |
46 42
|
sseldd |
|
50 |
49
|
adantr |
|
51 |
48 50
|
subcld |
|
52 |
|
eldifsni |
|
53 |
52
|
adantl |
|
54 |
48 50 53
|
subne0d |
|
55 |
45 51 54
|
divcld |
|
56 |
3
|
adantr |
|
57 |
|
inss2 |
|
58 |
57 35
|
sselid |
|
59 |
56 58
|
ffvelcdmd |
|
60 |
55 59
|
mulcld |
|
61 |
|
ssdif |
|
62 |
57 61
|
mp1i |
|
63 |
62
|
sselda |
|
64 |
4 5
|
sstrd |
|
65 |
5 3 4
|
dvbss |
|
66 |
|
reldv |
|
67 |
|
releldm |
|
68 |
66 7 67
|
sylancr |
|
69 |
65 68
|
sseldd |
|
70 |
3 64 69
|
dvlem |
|
71 |
63 70
|
syldan |
|
72 |
71 44
|
mulcld |
|
73 |
|
ssidd |
|
74 |
|
txtopon |
|
75 |
19 19 74
|
mp2an |
|
76 |
75
|
toponrestid |
|
77 |
12
|
simprd |
|
78 |
1 46 42
|
dvlem |
|
79 |
78
|
fmpttd |
|
80 |
|
ssdif |
|
81 |
33 80
|
mp1i |
|
82 |
46
|
ssdifssd |
|
83 |
|
eqid |
|
84 |
33 2
|
sstrid |
|
85 |
84 25
|
sseqtrd |
|
86 |
|
difssd |
|
87 |
85 86
|
unssd |
|
88 |
|
ssun1 |
|
89 |
88
|
a1i |
|
90 |
28
|
ntrss |
|
91 |
23 87 89 90
|
syl3anc |
|
92 |
|
eqid |
|
93 |
9 8 92 5 1 2
|
eldv |
|
94 |
6 93
|
mpbid |
|
95 |
94
|
simpld |
|
96 |
|
eqid |
|
97 |
9 8 96 5 3 4
|
eldv |
|
98 |
7 97
|
mpbid |
|
99 |
98
|
simpld |
|
100 |
95 99
|
elind |
|
101 |
100 30
|
eleqtrrd |
|
102 |
91 101
|
sseldd |
|
103 |
102 42
|
elind |
|
104 |
33
|
a1i |
|
105 |
|
eqid |
|
106 |
28 105
|
restntr |
|
107 |
23 26 104 106
|
syl3anc |
|
108 |
8
|
cnfldtop |
|
109 |
108
|
a1i |
|
110 |
|
cnex |
|
111 |
|
ssexg |
|
112 |
5 110 111
|
sylancl |
|
113 |
|
restabs |
|
114 |
109 2 112 113
|
syl3anc |
|
115 |
114
|
fveq2d |
|
116 |
115
|
fveq1d |
|
117 |
107 116
|
eqtr3d |
|
118 |
103 117
|
eleqtrd |
|
119 |
|
undif1 |
|
120 |
42
|
snssd |
|
121 |
|
ssequn2 |
|
122 |
120 121
|
sylib |
|
123 |
119 122
|
eqtrid |
|
124 |
123
|
oveq2d |
|
125 |
124
|
fveq2d |
|
126 |
|
undif1 |
|
127 |
42 69
|
elind |
|
128 |
127
|
snssd |
|
129 |
|
ssequn2 |
|
130 |
128 129
|
sylib |
|
131 |
126 130
|
eqtrid |
|
132 |
125 131
|
fveq12d |
|
133 |
118 132
|
eleqtrrd |
|
134 |
79 81 82 8 83 133
|
limcres |
|
135 |
81
|
resmptd |
|
136 |
135
|
oveq1d |
|
137 |
134 136
|
eqtr3d |
|
138 |
77 137
|
eleqtrd |
|
139 |
|
eqid |
|
140 |
139 8
|
dvcnp2 |
|
141 |
5 3 4 68 140
|
syl31anc |
|
142 |
8 139
|
cnplimc |
|
143 |
64 69 142
|
syl2anc |
|
144 |
141 143
|
mpbid |
|
145 |
144
|
simprd |
|
146 |
|
difss |
|
147 |
146 57
|
sstri |
|
148 |
147
|
a1i |
|
149 |
|
eqid |
|
150 |
|
difssd |
|
151 |
85 150
|
unssd |
|
152 |
|
ssun1 |
|
153 |
152
|
a1i |
|
154 |
28
|
ntrss |
|
155 |
23 151 153 154
|
syl3anc |
|
156 |
155 101
|
sseldd |
|
157 |
156 69
|
elind |
|
158 |
57
|
a1i |
|
159 |
|
eqid |
|
160 |
28 159
|
restntr |
|
161 |
23 27 158 160
|
syl3anc |
|
162 |
|
restabs |
|
163 |
109 4 112 162
|
syl3anc |
|
164 |
163
|
fveq2d |
|
165 |
164
|
fveq1d |
|
166 |
161 165
|
eqtr3d |
|
167 |
157 166
|
eleqtrd |
|
168 |
69
|
snssd |
|
169 |
|
ssequn2 |
|
170 |
168 169
|
sylib |
|
171 |
170
|
oveq2d |
|
172 |
171
|
fveq2d |
|
173 |
172 131
|
fveq12d |
|
174 |
167 173
|
eleqtrrd |
|
175 |
3 148 64 8 149 174
|
limcres |
|
176 |
3 148
|
feqresmpt |
|
177 |
176
|
oveq1d |
|
178 |
175 177
|
eqtr3d |
|
179 |
145 178
|
eleqtrd |
|
180 |
8
|
mpomulcn |
|
181 |
5 1 2
|
dvcl |
|
182 |
6 181
|
mpdan |
|
183 |
3 69
|
ffvelcdmd |
|
184 |
182 183
|
opelxpd |
|
185 |
75
|
toponunii |
|
186 |
185
|
cncnpi |
|
187 |
180 184 186
|
sylancr |
|
188 |
55 59 73 73 8 76 138 179 187
|
limccnp2 |
|
189 |
|
df-mpt |
|
190 |
189
|
oveq1i |
|
191 |
188 190
|
eleqtrdi |
|
192 |
|
ovmpot |
|
193 |
182 183 192
|
syl2anc |
|
194 |
|
ovmpot |
|
195 |
55 59 194
|
syl2anc |
|
196 |
195
|
eqeq2d |
|
197 |
196
|
pm5.32da |
|
198 |
197
|
opabbidv |
|
199 |
|
df-mpt |
|
200 |
198 199
|
eqtr4di |
|
201 |
200
|
oveq1d |
|
202 |
191 193 201
|
3eltr3d |
|
203 |
16
|
simprd |
|
204 |
70
|
fmpttd |
|
205 |
64
|
ssdifssd |
|
206 |
|
eqid |
|
207 |
|
undif1 |
|
208 |
207 170
|
eqtrid |
|
209 |
208
|
oveq2d |
|
210 |
209
|
fveq2d |
|
211 |
210 131
|
fveq12d |
|
212 |
167 211
|
eleqtrrd |
|
213 |
204 62 205 8 206 212
|
limcres |
|
214 |
62
|
resmptd |
|
215 |
214
|
oveq1d |
|
216 |
213 215
|
eqtr3d |
|
217 |
203 216
|
eleqtrd |
|
218 |
84 5
|
sstrd |
|
219 |
|
cncfmptc |
|
220 |
43 218 73 219
|
syl3anc |
|
221 |
|
eqidd |
|
222 |
220 127 221
|
cnmptlimc |
|
223 |
43
|
adantr |
|
224 |
223
|
fmpttd |
|
225 |
224
|
limcdif |
|
226 |
|
resmpt |
|
227 |
146 226
|
mp1i |
|
228 |
227
|
oveq1d |
|
229 |
225 228
|
eqtrd |
|
230 |
222 229
|
eleqtrd |
|
231 |
5 3 4
|
dvcl |
|
232 |
7 231
|
mpdan |
|
233 |
232 43
|
opelxpd |
|
234 |
185
|
cncnpi |
|
235 |
180 233 234
|
sylancr |
|
236 |
71 44 73 73 8 76 217 230 235
|
limccnp2 |
|
237 |
|
df-mpt |
|
238 |
237
|
oveq1i |
|
239 |
236 238
|
eleqtrdi |
|
240 |
|
ovmpot |
|
241 |
232 43 240
|
syl2anc |
|
242 |
42
|
adantr |
|
243 |
32 242
|
ffvelcdmd |
|
244 |
|
ovmpot |
|
245 |
71 243 244
|
syl2anc |
|
246 |
245
|
eqeq2d |
|
247 |
246
|
pm5.32da |
|
248 |
247
|
opabbidv |
|
249 |
|
df-mpt |
|
250 |
248 249
|
eqtr4di |
|
251 |
250
|
oveq1d |
|
252 |
239 241 251
|
3eltr3d |
|
253 |
8
|
addcn |
|
254 |
182 183
|
mulcld |
|
255 |
232 43
|
mulcld |
|
256 |
254 255
|
opelxpd |
|
257 |
185
|
cncnpi |
|
258 |
253 256 257
|
sylancr |
|
259 |
60 72 73 73 8 76 202 252 258
|
limccnp2 |
|
260 |
37 243
|
subcld |
|
261 |
260 59
|
mulcld |
|
262 |
69
|
adantr |
|
263 |
56 262
|
ffvelcdmd |
|
264 |
59 263
|
subcld |
|
265 |
264 243
|
mulcld |
|
266 |
47 242
|
sseldd |
|
267 |
48 266
|
subcld |
|
268 |
261 265 267 54
|
divdird |
|
269 |
37 59
|
mulcld |
|
270 |
243 59
|
mulcld |
|
271 |
243 263
|
mulcld |
|
272 |
269 270 271
|
npncand |
|
273 |
37 243 59
|
subdird |
|
274 |
264 243
|
mulcomd |
|
275 |
243 59 263
|
subdid |
|
276 |
274 275
|
eqtrd |
|
277 |
273 276
|
oveq12d |
|
278 |
1
|
ffnd |
|
279 |
278
|
adantr |
|
280 |
3
|
ffnd |
|
281 |
280
|
adantr |
|
282 |
|
ssexg |
|
283 |
46 110 282
|
sylancl |
|
284 |
283
|
adantr |
|
285 |
|
ssexg |
|
286 |
64 110 285
|
sylancl |
|
287 |
286
|
adantr |
|
288 |
|
eqid |
|
289 |
|
eqidd |
|
290 |
|
eqidd |
|
291 |
279 281 284 287 288 289 290
|
ofval |
|
292 |
35 291
|
mpdan |
|
293 |
|
eqidd |
|
294 |
|
eqidd |
|
295 |
279 281 284 287 288 293 294
|
ofval |
|
296 |
127 295
|
mpidan |
|
297 |
292 296
|
oveq12d |
|
298 |
272 277 297
|
3eqtr4d |
|
299 |
298
|
oveq1d |
|
300 |
260 59 267 54
|
div23d |
|
301 |
264 243 267 54
|
div23d |
|
302 |
300 301
|
oveq12d |
|
303 |
268 299 302
|
3eqtr3d |
|
304 |
303
|
mpteq2dva |
|
305 |
304
|
oveq1d |
|
306 |
259 305
|
eleqtrrd |
|
307 |
|
eqid |
|
308 |
|
mulcl |
|
309 |
308
|
adantl |
|
310 |
309 1 3 283 286 288
|
off |
|
311 |
9 8 307 5 310 84
|
eldv |
|
312 |
31 306 311
|
mpbir2and |
|