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

Theorem dvmulbr 19778
 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 2404 . . . . . . 7 t t
3 dvadd.j . . . . . . 7 fld
4 eqid 2404 . . . . . . 7
5 dvaddbr.s . . . . . . 7
6 dvadd.f . . . . . . 7
7 dvadd.x . . . . . . 7
82, 3, 4, 5, 6, 7eldv 19738 . . . . . 6 t lim
91, 8mpbid 202 . . . . 5 t lim
109simpld 446 . . . 4 t
11 dvadd.bg . . . . . 6
12 eqid 2404 . . . . . . 7
13 dvadd.g . . . . . . 7
14 dvadd.y . . . . . . 7
152, 3, 12, 5, 13, 14eldv 19738 . . . . . 6 t lim
1611, 15mpbid 202 . . . . 5 t lim
1716simpld 446 . . . 4 t
18 elin 3490 . . . 4 t t t t
1910, 17, 18sylanbrc 646 . . 3 t t
203cnfldtopon 18770 . . . . . 6 TopOn
21 resttopon 17179 . . . . . 6 TopOn t TopOn
2220, 5, 21sylancr 645 . . . . 5 t TopOn
23 topontop 16946 . . . . 5 t TopOn t
2422, 23syl 16 . . . 4 t
25 toponuni 16947 . . . . . 6 t TopOn t
2622, 25syl 16 . . . . 5 t
277, 26sseqtrd 3344 . . . 4 t
2814, 26sseqtrd 3344 . . . 4 t
29 eqid 2404 . . . . 5 t t
3029ntrin 17080 . . . 4 t t t t t t
3124, 27, 28, 30syl3anc 1184 . . 3 t t t
3219, 31eleqtrrd 2481 . 2 t
336adantr 452 . . . . . . . 8
34 inss1 3521 . . . . . . . . 9
35 eldifi 3429 . . . . . . . . . 10
3635adantl 453 . . . . . . . . 9
3734, 36sseldi 3306 . . . . . . . 8
3833, 37ffvelrnd 5830 . . . . . . 7
395, 6, 7dvbss 19741 . . . . . . . . . 10
40 reldv 19710 . . . . . . . . . . 11
41 releldm 5061 . . . . . . . . . . 11
4240, 1, 41sylancr 645 . . . . . . . . . 10
4339, 42sseldd 3309 . . . . . . . . 9
446, 43ffvelrnd 5830 . . . . . . . 8
4544adantr 452 . . . . . . 7
4638, 45subcld 9367 . . . . . 6
477, 5sstrd 3318 . . . . . . . . 9
4847adantr 452 . . . . . . . 8
4948, 37sseldd 3309 . . . . . . 7
5047, 43sseldd 3309 . . . . . . . 8
5150adantr 452 . . . . . . 7
5249, 51subcld 9367 . . . . . 6
53 eldifsni 3888 . . . . . . . 8
5453adantl 453 . . . . . . 7
5549, 51, 54subne0d 9376 . . . . . 6
5646, 52, 55divcld 9746 . . . . 5
5713adantr 452 . . . . . 6
58 inss2 3522 . . . . . . 7
5958, 36sseldi 3306 . . . . . 6
6057, 59ffvelrnd 5830 . . . . 5
6156, 60mulcld 9064 . . . 4
62 ssdif 3442 . . . . . . . 8
6358, 62mp1i 12 . . . . . . 7
6463sselda 3308 . . . . . 6
6514, 5sstrd 3318 . . . . . . 7
665, 13, 14dvbss 19741 . . . . . . . 8
67 reldv 19710 . . . . . . . . 9
68 releldm 5061 . . . . . . . . 9
6967, 11, 68sylancr 645 . . . . . . . 8
7066, 69sseldd 3309 . . . . . . 7
7113, 65, 70dvlem 19736 . . . . . 6
7264, 71syldan 457 . . . . 5
7372, 45mulcld 9064 . . . 4
74 ssid 3327 . . . . 5
7574a1i 11 . . . 4
76 txtopon 17576 . . . . . . 7 TopOn TopOn TopOn
7720, 20, 76mp2an 654 . . . . . 6 TopOn
7877toponunii 16952 . . . . . . 7
7978restid 13616 . . . . . 6 TopOn t
8077, 79ax-mp 8 . . . . 5 t
8180eqcomi 2408 . . . 4 t
829simprd 450 . . . . . 6 lim
836, 47, 43dvlem 19736 . . . . . . . . 9
8483, 4fmptd 5852 . . . . . . . 8
85 ssdif 3442 . . . . . . . . 9
8634, 85mp1i 12 . . . . . . . 8
8747ssdifssd 3445 . . . . . . . 8
88 eqid 2404 . . . . . . . 8 t t
8934, 7syl5ss 3319 . . . . . . . . . . . . . . 15
9089, 26sseqtrd 3344 . . . . . . . . . . . . . 14 t
91 difssd 3435 . . . . . . . . . . . . . 14 t t
9290, 91unssd 3483 . . . . . . . . . . . . 13 t t
93 ssun1 3470 . . . . . . . . . . . . . 14 t
9493a1i 11 . . . . . . . . . . . . 13 t
9529ntrss 17074 . . . . . . . . . . . . 13 t t t t t t t
9624, 92, 94, 95syl3anc 1184 . . . . . . . . . . . 12 t t t
9796, 32sseldd 3309 . . . . . . . . . . 11 t t
98 elin 3490 . . . . . . . . . . 11 t t t t
9997, 43, 98sylanbrc 646 . . . . . . . . . 10 t t
10034a1i 11 . . . . . . . . . . . 12
101 eqid 2404 . . . . . . . . . . . . 13 t t t t
10229, 101restntr 17200 . . . . . . . . . . . 12 t t t t t t
10324, 27, 100, 102syl3anc 1184 . . . . . . . . . . 11 t t t t
1043cnfldtop 18771 . . . . . . . . . . . . . . 15
105104a1i 11 . . . . . . . . . . . . . 14
106 cnex 9027 . . . . . . . . . . . . . . 15
107 ssexg 4309 . . . . . . . . . . . . . . 15
1085, 106, 107sylancl 644 . . . . . . . . . . . . . 14
109 restabs 17183 . . . . . . . . . . . . . 14 t t t
110105, 7, 108, 109syl3anc 1184 . . . . . . . . . . . . 13 t t t
111110fveq2d 5691 . . . . . . . . . . . 12 t t t
112111fveq1d 5689 . . . . . . . . . . 11 t t t
113103, 112eqtr3d 2438 . . . . . . . . . 10 t t t
11499, 113eleqtrd 2480 . . . . . . . . 9 t
115 undif1 3663 . . . . . . . . . . . . 13
11643snssd 3903 . . . . . . . . . . . . . 14
117 ssequn2 3480 . . . . . . . . . . . . . 14
118116, 117sylib 189 . . . . . . . . . . . . 13
119115, 118syl5eq 2448 . . . . . . . . . . . 12
120119oveq2d 6056 . . . . . . . . . . 11 t t
121120fveq2d 5691 . . . . . . . . . 10 t t
122 undif1 3663 . . . . . . . . . . 11
123 elin 3490 . . . . . . . . . . . . . 14
12443, 70, 123sylanbrc 646 . . . . . . . . . . . . 13
125124snssd 3903 . . . . . . . . . . . 12
126 ssequn2 3480 . . . . . . . . . . . 12
127125, 126sylib 189 . . . . . . . . . . 11
128122, 127syl5eq 2448 . . . . . . . . . 10
129121, 128fveq12d 5693 . . . . . . . . 9 t t
130114, 129eleqtrrd 2481 . . . . . . . 8 t
13184, 86, 87, 3, 88, 130limcres 19726 . . . . . . 7 lim lim
132 resmpt 5150 . . . . . . . . 9
13386, 132syl 16 . . . . . . . 8
134133oveq1d 6055 . . . . . . 7 lim lim
135131, 134eqtr3d 2438 . . . . . 6 lim lim
13682, 135eleqtrd 2480 . . . . 5 lim
137 eqid 2404 . . . . . . . . . 10 t t
138137, 3dvcnp2 19759 . . . . . . . . 9 t
1395, 13, 14, 69, 138syl31anc 1187 . . . . . . . 8 t
1403, 137cnplimc 19727 . . . . . . . . 9 t lim
14165, 70, 140syl2anc 643 . . . . . . . 8 t lim
142139, 141mpbid 202 . . . . . . 7 lim
143142simprd 450 . . . . . 6 lim
144 difss 3434 . . . . . . . . . 10
145144, 58sstri 3317 . . . . . . . . 9
146145a1i 11 . . . . . . . 8
147 eqid 2404 . . . . . . . 8 t t
148 difssd 3435 . . . . . . . . . . . . . 14 t t
14990, 148unssd 3483 . . . . . . . . . . . . 13 t t
150 ssun1 3470 . . . . . . . . . . . . . 14 t
151150a1i 11 . . . . . . . . . . . . 13 t
15229ntrss 17074 . . . . . . . . . . . . 13 t t t t t t t
15324, 149, 151, 152syl3anc 1184 . . . . . . . . . . . 12 t t t
154153, 32sseldd 3309 . . . . . . . . . . 11 t t
155 elin 3490 . . . . . . . . . . 11 t t t t
156154, 70, 155sylanbrc 646 . . . . . . . . . 10 t t
15758a1i 11 . . . . . . . . . . . 12
158 eqid 2404 . . . . . . . . . . . . 13 t t t t
15929, 158restntr 17200 . . . . . . . . . . . 12 t t t t t t
16024, 28, 157, 159syl3anc 1184 . . . . . . . . . . 11 t t t t
161 restabs 17183 . . . . . . . . . . . . . 14 t t t
162105, 14, 108, 161syl3anc 1184 . . . . . . . . . . . . 13 t t t
163162fveq2d 5691 . . . . . . . . . . . 12 t t t
164163fveq1d 5689 . . . . . . . . . . 11 t t t
165160, 164eqtr3d 2438 . . . . . . . . . 10 t t t
166156, 165eleqtrd 2480 . . . . . . . . 9 t
16770snssd 3903 . . . . . . . . . . . . 13
168 ssequn2 3480 . . . . . . . . . . . . 13
169167, 168sylib 189 . . . . . . . . . . . 12
170169oveq2d 6056 . . . . . . . . . . 11 t t
171170fveq2d 5691 . . . . . . . . . 10 t t
172171, 128fveq12d 5693 . . . . . . . . 9 t t
173166, 172eleqtrrd 2481 . . . . . . . 8 t
17413, 146, 65, 3, 147, 173limcres 19726 . . . . . . 7 lim lim
17513, 146feqresmpt 5739 . . . . . . . 8
176175oveq1d 6055 . . . . . . 7 lim lim
177174, 176eqtr3d 2438 . . . . . 6 lim lim
178143, 177eleqtrd 2480 . . . . 5 lim
1793mulcn 18850 . . . . . 6
1805, 6, 7dvcl 19739 . . . . . . . 8
1811, 180mpdan 650 . . . . . . 7
18213, 70ffvelrnd 5830 . . . . . . 7
183 opelxpi 4869 . . . . . . 7
184181, 182, 183syl2anc 643 . . . . . 6
18578cncnpi 17296 . . . . . 6
186179, 184, 185sylancr 645 . . . . 5
18756, 60, 75, 75, 3, 81, 136, 178, 186limccnp2 19732 . . . 4 lim
18816simprd 450 . . . . . 6 lim
18971, 12fmptd 5852 . . . . . . . 8
19065ssdifssd 3445 . . . . . . . 8
191 eqid 2404 . . . . . . . 8 t t
192 undif1 3663 . . . . . . . . . . . . 13
193192, 169syl5eq 2448 . . . . . . . . . . . 12
194193oveq2d 6056 . . . . . . . . . . 11 t t
195194fveq2d 5691 . . . . . . . . . 10 t t
196195, 128fveq12d 5693 . . . . . . . . 9 t t
197166, 196eleqtrrd 2481 . . . . . . . 8 t
198189, 63, 190, 3, 191, 197limcres 19726 . . . . . . 7 lim lim
199 resmpt 5150 . . . . . . . . 9
20063, 199syl 16 . . . . . . . 8
201200oveq1d 6055 . . . . . . 7 lim lim
202198, 201eqtr3d 2438 . . . . . 6 lim lim
203188, 202eleqtrd 2480 . . . . 5 lim
20489, 5sstrd 3318 . . . . . . . 8
205 cncfmptc 18894 . . . . . . . 8
20644, 204, 75, 205syl3anc 1184 . . . . . . 7
207 eqidd 2405 . . . . . . 7
208206, 124, 207cnmptlimc 19730 . . . . . 6 lim
20944adantr 452 . . . . . . . . 9
210 eqid 2404 . . . . . . . . 9
211209, 210fmptd 5852 . . . . . . . 8
212211limcdif 19716 . . . . . . 7 lim lim
213 resmpt 5150 . . . . . . . . 9
214144, 213mp1i 12 . . . . . . . 8
215214oveq1d 6055 . . . . . . 7 lim lim
216212, 215eqtrd 2436 . . . . . 6 lim lim
217208, 216eleqtrd 2480 . . . . 5 lim
2185, 13, 14dvcl 19739 . . . . . . . 8
21911, 218mpdan 650 . . . . . . 7
220 opelxpi 4869 . . . . . . 7
221219, 44, 220syl2anc 643 . . . . . 6
22278cncnpi 17296 . . . . . 6
223179, 221, 222sylancr 645 . . . . 5
22472, 45, 75, 75, 3, 81, 203, 217, 223limccnp2 19732 . . . 4 lim
2253addcn 18848 . . . . 5
226181, 182mulcld 9064 . . . . . 6
227219, 44mulcld 9064 . . . . . 6
228 opelxpi 4869 . . . . . 6
229226, 227, 228syl2anc 643 . . . . 5
23078cncnpi 17296 . . . . 5
231225, 229, 230sylancr 645 . . . 4
23261, 73, 75, 75, 3, 81, 187, 224, 231limccnp2 19732 . . 3 lim
23343adantr 452 . . . . . . . . . 10
23433, 233ffvelrnd 5830 . . . . . . . . 9
23538, 234subcld 9367 . . . . . . . 8
236235, 60mulcld 9064 . . . . . . 7
23770adantr 452 . . . . . . . . . 10
23857, 237ffvelrnd 5830 . . . . . . . . 9
23960, 238subcld 9367 . . . . . . . 8
240239, 234mulcld 9064 . . . . . . 7
24148, 233sseldd 3309 . . . . . . . 8
24249, 241subcld 9367 . . . . . . 7
243236, 240, 242, 55divdird 9784 . . . . . 6
24438, 60mulcld 9064 . . . . . . . . 9
245234, 60mulcld 9064 . . . . . . . . 9
246234, 238mulcld 9064 . . . . . . . . 9
247244, 245, 246npncand 9391 . . . . . . . 8
24838, 234, 60subdird 9446 . . . . . . . . 9
249239, 234mulcomd 9065 . . . . . . . . . 10
250234, 60, 238subdid 9445 . . . . . . . . . 10
251249, 250eqtrd 2436 . . . . . . . . 9
252248, 251oveq12d 6058 . . . . . . . 8
253 ffn 5550 . . . . . . . . . . . . 13
2546, 253syl 16 . . . . . . . . . . . 12
255254adantr 452 . . . . . . . . . . 11
256 ffn 5550 . . . . . . . . . . . . 13
25713, 256syl 16 . . . . . . . . . . . 12
258257adantr 452 . . . . . . . . . . 11
259 ssexg 4309 . . . . . . . . . . . . 13
26047, 106, 259sylancl 644 . . . . . . . . . . . 12
261260adantr 452 . . . . . . . . . . 11
262 ssexg 4309 . . . . . . . . . . . . 13
26365, 106, 262sylancl 644 . . . . . . . . . . . 12
264263adantr 452 . . . . . . . . . . 11
265 eqid 2404 . . . . . . . . . . 11
266 eqidd 2405 . . . . . . . . . . 11
267 eqidd 2405 . . . . . . . . . . 11
268255, 258, 261, 264, 265, 266, 267ofval 6273 . . . . . . . . . 10
26936, 268mpdan 650 . . . . . . . . 9
270124adantr 452 . . . . . . . . . 10
271 eqidd 2405 . . . . . . . . . . 11
272 eqidd 2405 . . . . . . . . . . 11
273255, 258, 261, 264, 265, 271, 272ofval 6273 . . . . . . . . . 10
274270, 273mpdan 650 . . . . . . . . 9
275269, 274oveq12d 6058 . . . . . . . 8
276247, 252, 2753eqtr4d 2446 . . . . . . 7
277276oveq1d 6055 . . . . . 6
278235, 60, 242, 55div23d 9783 . . . . . . 7
279239, 234, 242, 55div23d 9783 . . . . . . 7
280278, 279oveq12d 6058 . . . . . 6
281243, 277, 2803eqtr3d 2444 . . . . 5
282281mpteq2dva 4255 . . . 4
283282oveq1d 6055 . . 3 lim lim
284232, 283eleqtrrd 2481 . 2 lim
285 eqid 2404 . . 3
286 mulcl 9030 . . . . 5
287286adantl 453 . . . 4
288287, 6, 13, 260, 263, 265off 6279 . . 3
2892, 3, 285, 5, 288, 89eldv 19738 . 2 t lim
29032, 284, 289mpbir2and 889 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1649   wcel 1721   wne 2567  cvv 2916   cdif 3277   cun 3278   cin 3279   wss 3280  csn 3774  cop 3777  cuni 3975   class class class wbr 4172   cmpt 4226   cxp 4835   cdm 4837   cres 4839   wrel 4842   wfn 5408  wf 5409  cfv 5413  (class class class)co 6040   cof 6262  cc 8944   caddc 8949   cmul 8951   cmin 9247   cdiv 9633   ↾t crest 13603  ctopn 13604  ℂfldccnfld 16658  ctop 16913  TopOnctopon 16914  cnt 17036   ccn 17242   ccnp 17243   ctx 17545  ccncf 18859   lim climc 19702   cdv 19703 This theorem is referenced by:  dvmul  19780  dvmulf  19782  dvef  19817 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-icc 10879  df-fz 11000  df-fzo 11091  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-hom 13508  df-cco 13509  df-rest 13605  df-topn 13606  df-topgen 13622  df-pt 13623  df-prds 13626  df-xrs 13681  df-0g 13682  df-gsum 13683  df-qtop 13688  df-imas 13689  df-xps 13691  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-submnd 14694  df-mulg 14770  df-cntz 15071  df-cmn 15369  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-cnfld 16659  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-cld 17038  df-ntr 17039  df-cls 17040  df-cn 17245  df-cnp 17246  df-tx 17547  df-hmeo 17740  df-xms 18303  df-ms 18304  df-tms 18305  df-cncf 18861  df-limc 19706  df-dv 19707
 Copyright terms: Public domain W3C validator