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

Theorem dvmulbr 19386
 Description: The product rule for derivatives at a point. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
Assertion
Ref Expression
dvmulbr

Proof of Theorem dvmulbr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvadd.bf . . . . . 6
2 eqid 2358 . . . . . . 7 t t
3 dvadd.j . . . . . . 7 fld
4 eqid 2358 . . . . . . 7
5 dvaddbr.s . . . . . . 7
6 dvadd.f . . . . . . 7
7 dvadd.x . . . . . . 7
82, 3, 4, 5, 6, 7eldv 19346 . . . . . 6 t lim
91, 8mpbid 201 . . . . 5 t lim
109simpld 445 . . . 4 t
11 dvadd.bg . . . . . 6
12 eqid 2358 . . . . . . 7
13 dvadd.g . . . . . . 7
14 dvadd.y . . . . . . 7
152, 3, 12, 5, 13, 14eldv 19346 . . . . . 6 t lim
1611, 15mpbid 201 . . . . 5 t lim
1716simpld 445 . . . 4 t
18 elin 3434 . . . 4 t t t t
1910, 17, 18sylanbrc 645 . . 3 t t
203cnfldtopon 18388 . . . . . 6 TopOn
21 resttopon 16992 . . . . . 6 TopOn t TopOn
2220, 5, 21sylancr 644 . . . . 5 t TopOn
23 topontop 16764 . . . . 5 t TopOn t
2422, 23syl 15 . . . 4 t
25 toponuni 16765 . . . . . 6 t TopOn t
2622, 25syl 15 . . . . 5 t
277, 26sseqtrd 3290 . . . 4 t
2814, 26sseqtrd 3290 . . . 4 t
29 eqid 2358 . . . . 5 t t
3029ntrin 16898 . . . 4 t t t t t t
3124, 27, 28, 30syl3anc 1182 . . 3 t t t
3219, 31eleqtrrd 2435 . 2 t
336adantr 451 . . . . . . . 8
34 inss1 3465 . . . . . . . . 9
35 eldifi 3374 . . . . . . . . . 10
3635adantl 452 . . . . . . . . 9
3734, 36sseldi 3254 . . . . . . . 8
38 ffvelrn 5743 . . . . . . . 8
3933, 37, 38syl2anc 642 . . . . . . 7
405, 6, 7dvbss 19349 . . . . . . . . . 10
41 reldv 19318 . . . . . . . . . . 11
42 releldm 4990 . . . . . . . . . . 11
4341, 1, 42sylancr 644 . . . . . . . . . 10
4440, 43sseldd 3257 . . . . . . . . 9
45 ffvelrn 5743 . . . . . . . . 9
466, 44, 45syl2anc 642 . . . . . . . 8
4746adantr 451 . . . . . . 7
4839, 47subcld 9244 . . . . . 6
497, 5sstrd 3265 . . . . . . . . 9
5049adantr 451 . . . . . . . 8
5150, 37sseldd 3257 . . . . . . 7
5249, 44sseldd 3257 . . . . . . . 8
5352adantr 451 . . . . . . 7
5451, 53subcld 9244 . . . . . 6
55 eldifsni 3826 . . . . . . . 8
5655adantl 452 . . . . . . 7
57 subeq0 9160 . . . . . . . . 9
5851, 53, 57syl2anc 642 . . . . . . . 8
5958necon3bid 2556 . . . . . . 7
6056, 59mpbird 223 . . . . . 6
6148, 54, 60divcld 9623 . . . . 5
6213adantr 451 . . . . . 6
63 inss2 3466 . . . . . . . 8
6463sseli 3252 . . . . . . 7
6536, 64syl 15 . . . . . 6
66 ffvelrn 5743 . . . . . 6
6762, 65, 66syl2anc 642 . . . . 5
6861, 67mulcld 8942 . . . 4
69 ssdif 3387 . . . . . . . 8
7063, 69mp1i 11 . . . . . . 7
7170sselda 3256 . . . . . 6
7214, 5sstrd 3265 . . . . . . 7
735, 13, 14dvbss 19349 . . . . . . . 8
74 reldv 19318 . . . . . . . . 9
75 releldm 4990 . . . . . . . . 9
7674, 11, 75sylancr 644 . . . . . . . 8
7773, 76sseldd 3257 . . . . . . 7
7813, 72, 77dvlem 19344 . . . . . 6
7971, 78syldan 456 . . . . 5
8079, 47mulcld 8942 . . . 4
81 ssid 3273 . . . . 5
8281a1i 10 . . . 4
83 txtopon 17386 . . . . . . 7 TopOn TopOn TopOn
8420, 20, 83mp2an 653 . . . . . 6 TopOn
8584toponunii 16770 . . . . . . 7
8685restid 13431 . . . . . 6 TopOn t
8784, 86ax-mp 8 . . . . 5 t
8887eqcomi 2362 . . . 4 t
899simprd 449 . . . . . 6 lim
906, 49, 44dvlem 19344 . . . . . . . . 9
9190, 4fmptd 5764 . . . . . . . 8
92 ssdif 3387 . . . . . . . . 9
9334, 92mp1i 11 . . . . . . . 8
94 difss 3379 . . . . . . . . 9
9594, 49syl5ss 3266 . . . . . . . 8
96 eqid 2358 . . . . . . . 8 t t
9734, 7syl5ss 3266 . . . . . . . . . . . . . . 15
9897, 26sseqtrd 3290 . . . . . . . . . . . . . 14 t
99 difss 3379 . . . . . . . . . . . . . . 15 t t
10099a1i 10 . . . . . . . . . . . . . 14 t t
10198, 100unssd 3427 . . . . . . . . . . . . 13 t t
102 ssun1 3414 . . . . . . . . . . . . . 14 t
103102a1i 10 . . . . . . . . . . . . 13 t
10429ntrss 16892 . . . . . . . . . . . . 13 t t t t t t t
10524, 101, 103, 104syl3anc 1182 . . . . . . . . . . . 12 t t t
106105, 32sseldd 3257 . . . . . . . . . . 11 t t
107 elin 3434 . . . . . . . . . . 11 t t t t
108106, 44, 107sylanbrc 645 . . . . . . . . . 10 t t
10934a1i 10 . . . . . . . . . . . 12
110 eqid 2358 . . . . . . . . . . . . 13 t t t t
11129, 110restntr 17012 . . . . . . . . . . . 12 t t t t t t
11224, 27, 109, 111syl3anc 1182 . . . . . . . . . . 11 t t t t
1133cnfldtop 18389 . . . . . . . . . . . . . . 15
114113a1i 10 . . . . . . . . . . . . . 14
115 cnex 8905 . . . . . . . . . . . . . . 15
116 ssexg 4239 . . . . . . . . . . . . . . 15
1175, 115, 116sylancl 643 . . . . . . . . . . . . . 14
118 restabs 16996 . . . . . . . . . . . . . 14 t t t
119114, 7, 117, 118syl3anc 1182 . . . . . . . . . . . . 13 t t t
120119fveq2d 5609 . . . . . . . . . . . 12 t t t
121120fveq1d 5607 . . . . . . . . . . 11 t t t
122112, 121eqtr3d 2392 . . . . . . . . . 10 t t t
123108, 122eleqtrd 2434 . . . . . . . . 9 t
124 undif1 3605 . . . . . . . . . . . . 13
12544snssd 3839 . . . . . . . . . . . . . 14
126 ssequn2 3424 . . . . . . . . . . . . . 14
127125, 126sylib 188 . . . . . . . . . . . . 13
128124, 127syl5eq 2402 . . . . . . . . . . . 12
129128oveq2d 5958 . . . . . . . . . . 11 t t
130129fveq2d 5609 . . . . . . . . . 10 t t
131 undif1 3605 . . . . . . . . . . 11
132 elin 3434 . . . . . . . . . . . . . 14
13344, 77, 132sylanbrc 645 . . . . . . . . . . . . 13
134133snssd 3839 . . . . . . . . . . . 12
135 ssequn2 3424 . . . . . . . . . . . 12
136134, 135sylib 188 . . . . . . . . . . 11
137131, 136syl5eq 2402 . . . . . . . . . 10
138130, 137fveq12d 5611 . . . . . . . . 9 t t
139123, 138eleqtrrd 2435 . . . . . . . 8 t
14091, 93, 95, 3, 96, 139limcres 19334 . . . . . . 7 lim lim
141 resmpt 5079 . . . . . . . . 9
14293, 141syl 15 . . . . . . . 8
143142oveq1d 5957 . . . . . . 7 lim lim
144140, 143eqtr3d 2392 . . . . . 6 lim lim
14589, 144eleqtrd 2434 . . . . 5 lim
146 eqid 2358 . . . . . . . . . 10 t t
147146, 3dvcnp2 19367 . . . . . . . . 9 t
1485, 13, 14, 76, 147syl31anc 1185 . . . . . . . 8 t
1493, 146cnplimc 19335 . . . . . . . . 9 t lim
15072, 77, 149syl2anc 642 . . . . . . . 8 t lim
151148, 150mpbid 201 . . . . . . 7 lim
152151simprd 449 . . . . . 6 lim
153 difss 3379 . . . . . . . . . 10
154153, 63sstri 3264 . . . . . . . . 9
155154a1i 10 . . . . . . . 8
156 eqid 2358 . . . . . . . 8 t t
157 difss 3379 . . . . . . . . . . . . . . 15 t t
158157a1i 10 . . . . . . . . . . . . . 14 t t
15998, 158unssd 3427 . . . . . . . . . . . . 13 t t
160 ssun1 3414 . . . . . . . . . . . . . 14 t
161160a1i 10 . . . . . . . . . . . . 13 t
16229ntrss 16892 . . . . . . . . . . . . 13 t t t t t t t
16324, 159, 161, 162syl3anc 1182 . . . . . . . . . . . 12 t t t
164163, 32sseldd 3257 . . . . . . . . . . 11 t t
165 elin 3434 . . . . . . . . . . 11 t t t t
166164, 77, 165sylanbrc 645 . . . . . . . . . 10 t t
16763a1i 10 . . . . . . . . . . . 12
168 eqid 2358 . . . . . . . . . . . . 13 t t t t
16929, 168restntr 17012 . . . . . . . . . . . 12 t t t t t t
17024, 28, 167, 169syl3anc 1182 . . . . . . . . . . 11 t t t t
171 restabs 16996 . . . . . . . . . . . . . 14 t t t
172114, 14, 117, 171syl3anc 1182 . . . . . . . . . . . . 13 t t t
173172fveq2d 5609 . . . . . . . . . . . 12 t t t
174173fveq1d 5607 . . . . . . . . . . 11 t t t
175170, 174eqtr3d 2392 . . . . . . . . . 10 t t t
176166, 175eleqtrd 2434 . . . . . . . . 9 t
177134, 167sstrd 3265 . . . . . . . . . . . . 13
178 ssequn2 3424 . . . . . . . . . . . . 13
179177, 178sylib 188 . . . . . . . . . . . 12
180179oveq2d 5958 . . . . . . . . . . 11 t t
181180fveq2d 5609 . . . . . . . . . 10 t t
182181, 137fveq12d 5611 . . . . . . . . 9 t t
183176, 182eleqtrrd 2435 . . . . . . . 8 t
18413, 155, 72, 3, 156, 183limcres 19334 . . . . . . 7 lim lim
18513feqmptd 5655 . . . . . . . . . 10
186185reseq1d 5033 . . . . . . . . 9
187 resmpt 5079 . . . . . . . . . 10
188155, 187syl 15 . . . . . . . . 9
189186, 188eqtrd 2390 . . . . . . . 8
190189oveq1d 5957 . . . . . . 7 lim lim
191184, 190eqtr3d 2392 . . . . . 6 lim lim
192152, 191eleqtrd 2434 . . . . 5 lim
1933mulcn 18468 . . . . . 6
1945, 6, 7dvcl 19347 . . . . . . . 8
1951, 194mpdan 649 . . . . . . 7
196 ffvelrn 5743 . . . . . . . 8
19713, 77, 196syl2anc 642 . . . . . . 7
198 opelxpi 4800 . . . . . . 7
199195, 197, 198syl2anc 642 . . . . . 6
20085cncnpi 17107 . . . . . 6
201193, 199, 200sylancr 644 . . . . 5
20261, 67, 82, 82, 3, 88, 145, 192, 201limccnp2 19340 . . . 4 lim
20316simprd 449 . . . . . 6 lim
20478, 12fmptd 5764 . . . . . . . 8
205 difss 3379 . . . . . . . . 9
206205, 72syl5ss 3266 . . . . . . . 8
207 eqid 2358 . . . . . . . 8 t t
208 undif1 3605 . . . . . . . . . . . . 13
209208, 179syl5eq 2402 . . . . . . . . . . . 12
210209oveq2d 5958 . . . . . . . . . . 11 t t
211210fveq2d 5609 . . . . . . . . . 10 t t
212211, 137fveq12d 5611 . . . . . . . . 9 t t
213176, 212eleqtrrd 2435 . . . . . . . 8 t
214204, 70, 206, 3, 207, 213limcres 19334 . . . . . . 7 lim lim
215 resmpt 5079 . . . . . . . . 9
21670, 215syl 15 . . . . . . . 8
217216oveq1d 5957 . . . . . . 7 lim lim
218214, 217eqtr3d 2392 . . . . . 6 lim lim
219203, 218eleqtrd 2434 . . . . 5 lim
22097, 5sstrd 3265 . . . . . . . 8
221 cncfmptc 18512 . . . . . . . 8
22246, 220, 82, 221syl3anc 1182 . . . . . . 7
223 eqidd 2359 . . . . . . 7
224222, 133, 223cnmptlimc 19338 . . . . . 6 lim
22546adantr 451 . . . . . . . . 9
226 eqid 2358 . . . . . . . . 9
227225, 226fmptd 5764 . . . . . . . 8
228227limcdif 19324 . . . . . . 7 lim lim
229 resmpt 5079 . . . . . . . . 9
230153, 229mp1i 11 . . . . . . . 8
231230oveq1d 5957 . . . . . . 7 lim lim
232228, 231eqtrd 2390 . . . . . 6 lim lim
233224, 232eleqtrd 2434 . . . . 5 lim
2345, 13, 14dvcl 19347 . . . . . . . 8
23511, 234mpdan 649 . . . . . . 7
236 opelxpi 4800 . . . . . . 7
237235, 46, 236syl2anc 642 . . . . . 6
23885cncnpi 17107 . . . . . 6
239193, 237, 238sylancr 644 . . . . 5
24079, 47, 82, 82, 3, 88, 219, 233, 239limccnp2 19340 . . . 4 lim
2413addcn 18466 . . . . 5
242195, 197mulcld 8942 . . . . . 6
243235, 46mulcld 8942 . . . . . 6
244 opelxpi 4800 . . . . . 6
245242, 243, 244syl2anc 642 . . . . 5
24685cncnpi 17107 . . . . 5
247241, 245, 246sylancr 644 . . . 4
24868, 80, 82, 82, 3, 88, 202, 240, 247limccnp2 19340 . . 3 lim
24944adantr 451 . . . . . . . . . 10
25033, 249, 45syl2anc 642 . . . . . . . . 9
25139, 250subcld 9244 . . . . . . . 8
252251, 67mulcld 8942 . . . . . . 7
25377adantr 451 . . . . . . . . . 10
25462, 253, 196syl2anc 642 . . . . . . . . 9
25567, 254subcld 9244 . . . . . . . 8
256255, 250mulcld 8942 . . . . . . 7
25750, 249sseldd 3257 . . . . . . . 8
25851, 257subcld 9244 . . . . . . 7
259252, 256, 258, 60divdird 9661 . . . . . 6
26039, 67mulcld 8942 . . . . . . . . 9
261250, 67mulcld 8942 . . . . . . . . 9
262250, 254mulcld 8942 . . . . . . . . 9
263260, 261, 262npncand 9268 . . . . . . . 8
26439, 250, 67subdird 9323 . . . . . . . . 9
265255, 250mulcomd 8943 . . . . . . . . . 10
266250, 67, 254subdid 9322 . . . . . . . . . 10
267265, 266eqtrd 2390 . . . . . . . . 9
268264, 267oveq12d 5960 . . . . . . . 8
269 ffn 5469 . . . . . . . . . . . . 13
2706, 269syl 15 . . . . . . . . . . . 12
271270adantr 451 . . . . . . . . . . 11
272 ffn 5469 . . . . . . . . . . . . 13
27313, 272syl 15 . . . . . . . . . . . 12
274273adantr 451 . . . . . . . . . . 11
275 ssexg 4239 . . . . . . . . . . . . 13
27649, 115, 275sylancl 643 . . . . . . . . . . . 12
277276adantr 451 . . . . . . . . . . 11
278 ssexg 4239 . . . . . . . . . . . . 13
27972, 115, 278sylancl 643 . . . . . . . . . . . 12
280279adantr 451 . . . . . . . . . . 11
281 eqid 2358 . . . . . . . . . . 11
282 eqidd 2359 . . . . . . . . . . 11
283 eqidd 2359 . . . . . . . . . . 11
284271, 274, 277, 280, 281, 282, 283ofval 6171 . . . . . . . . . 10
28536, 284mpdan 649 . . . . . . . . 9
286133adantr 451 . . . . . . . . . 10
287 eqidd 2359 . . . . . . . . . . 11
288 eqidd 2359 . . . . . . . . . . 11
289271, 274, 277, 280, 281, 287, 288ofval 6171 . . . . . . . . . 10
290286, 289mpdan 649 . . . . . . . . 9
291285, 290oveq12d 5960 . . . . . . . 8
292263, 268, 2913eqtr4d 2400 . . . . . . 7
293292oveq1d 5957 . . . . . 6
294251, 67, 258, 60div23d 9660 . . . . . . 7
295255, 250, 258, 60div23d 9660 . . . . . . 7
296294, 295oveq12d 5960 . . . . . 6
297259, 293, 2963eqtr3d 2398 . . . . 5
298297mpteq2dva 4185 . . . 4
299298oveq1d 5957 . . 3 lim lim
300248, 299eleqtrrd 2435 . 2 lim
301 eqid 2358 . . 3
302 mulcl 8908 . . . . 5
303302adantl 452 . . . 4
304303, 6, 13, 276, 279, 281off 6177 . . 3
3052, 3, 301, 5, 304, 97eldv 19346 . 2 t lim
30632, 300, 305mpbir2and 888 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wceq 1642   wcel 1710   wne 2521  cvv 2864   cdif 3225   cun 3226   cin 3227   wss 3228  csn 3716  cop 3719  cuni 3906   class class class wbr 4102   cmpt 4156   cxp 4766   cdm 4768   cres 4770   wrel 4773   wfn 5329  wf 5330  cfv 5334  (class class class)co 5942   cof 6160  cc 8822  cc0 8824   caddc 8827   cmul 8829   cmin 9124   cdiv 9510   ↾t crest 13418  ctopn 13419  ℂfldccnfld 16476  ctop 16731  TopOnctopon 16732  cnt 16854   ccn 17054   ccnp 17055   ctx 17355  ccncf 18477   lim climc 19310   cdv 19311 This theorem is referenced by:  dvmul  19388  dvmulf  19390  dvef  19425 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4210  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-inf2 7429  ax-cnex 8880  ax-resscn 8881  ax-1cn 8882  ax-icn 8883  ax-addcl 8884  ax-addrcl 8885  ax-mulcl 8886  ax-mulrcl 8887  ax-mulcom 8888  ax-addass 8889  ax-mulass 8890  ax-distr 8891  ax-i2m1 8892  ax-1ne0 8893  ax-1rid 8894  ax-rnegex 8895  ax-rrecex 8896  ax-cnre 8897  ax-pre-lttri 8898  ax-pre-lttrn 8899  ax-pre-ltadd 8900  ax-pre-mulgt0 8901  ax-pre-sup 8902  ax-addf 8903  ax-mulf 8904 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rmo 2627  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-iin 3987  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-se 4432  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-isom 5343  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-of 6162  df-1st 6206  df-2nd 6207  df-riota 6388  df-recs 6472  df-rdg 6507  df-1o 6563  df-2o 6564  df-oadd 6567  df-er 6744  df-map 6859  df-pm 6860  df-ixp 6903  df-en 6949  df-dom 6950  df-sdom 6951  df-fin 6952  df-fi 7252  df-sup 7281  df-oi 7312  df-card 7659  df-cda 7881  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960  df-sub 9126  df-neg 9127  df-div 9511  df-nn 9834  df-2 9891  df-3 9892  df-4 9893  df-5 9894  df-6 9895  df-7 9896  df-8 9897  df-9 9898  df-10 9899  df-n0 10055  df-z 10114  df-dec 10214  df-uz 10320  df-q 10406  df-rp 10444  df-xneg 10541  df-xadd 10542  df-xmul 10543  df-icc 10752  df-fz 10872  df-fzo 10960  df-seq 11136  df-exp 11195  df-hash 11428  df-cj 11674  df-re 11675  df-im 11676  df-sqr 11810  df-abs 11811  df-struct 13241  df-ndx 13242  df-slot 13243  df-base 13244  df-sets 13245  df-ress 13246  df-plusg 13312  df-mulr 13313  df-starv 13314  df-sca 13315  df-vsca 13316  df-tset 13318  df-ple 13319  df-ds 13321  df-unif 13322  df-hom 13323  df-cco 13324  df-rest 13420  df-topn 13421  df-topgen 13437  df-pt 13438  df-prds 13441  df-xrs 13496  df-0g 13497  df-gsum 13498  df-qtop 13503  df-imas 13504  df-xps 13506  df-mre 13581  df-mrc 13582  df-acs 13584  df-mnd 14460  df-submnd 14509  df-mulg 14585  df-cntz 14886  df-cmn 15184  df-xmet 16469  df-met 16470  df-bl 16471  df-mopn 16472  df-cnfld 16477  df-top 16736  df-bases 16738  df-topon 16739  df-topsp 16740  df-cld 16856  df-ntr 16857  df-cls 16858  df-cn 17057  df-cnp 17058  df-tx 17357  df-hmeo 17546  df-xms 17981  df-ms 17982  df-tms 17983  df-cncf 18479  df-limc 19314  df-dv 19315
 Copyright terms: Public domain W3C validator