Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  dvmulxxbr Unicode version

Theorem dvmulxxbr 12709
 Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 12711. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
Hypotheses
Ref Expression
Assertion
Ref Expression
dvmulxxbr

Proof of Theorem dvmulxxbr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvadd.bf . . . 4
2 eqid 2115 . . . . 5 t t
3 dvaddcntop.j . . . . 5
4 eqid 2115 . . . . 5 # #
5 dvaddbr.s . . . . 5
6 dvadd.f . . . . 5
7 dvadd.x . . . . 5
82, 3, 4, 5, 6, 7eldvap 12694 . . . 4 t # lim
91, 8mpbid 146 . . 3 t # lim
109simpld 111 . 2 t
117, 5sstrd 3075 . . . . . 6
123cntoptopon 12596 . . . . . . . . . 10 TopOn
13 resttopon 12235 . . . . . . . . . 10 TopOn t TopOn
1412, 5, 13sylancr 408 . . . . . . . . 9 t TopOn
15 topontop 12076 . . . . . . . . 9 t TopOn t
1614, 15syl 14 . . . . . . . 8 t
17 toponuni 12077 . . . . . . . . . 10 t TopOn t
1814, 17syl 14 . . . . . . . . 9 t
197, 18sseqtrd 3103 . . . . . . . 8 t
20 eqid 2115 . . . . . . . . 9 t t
2120ntrss2 12185 . . . . . . . 8 t t t
2216, 19, 21syl2anc 406 . . . . . . 7 t
2322, 10sseldd 3066 . . . . . 6
246, 11, 23dvlemap 12692 . . . . 5 #
25 dvaddxx.g . . . . . . 7
2625adantr 272 . . . . . 6 #
27 elrabi 2808 . . . . . . 7 #
2827adantl 273 . . . . . 6 #
2926, 28ffvelrnd 5522 . . . . 5 #
3024, 29mulcld 7750 . . . 4 #
3125, 11, 23dvlemap 12692 . . . . 5 #
326, 23ffvelrnd 5522 . . . . . 6
3332adantr 272 . . . . 5 #
3431, 33mulcld 7750 . . . 4 #
35 ssidd 3086 . . . 4
36 txtopon 12326 . . . . . 6 TopOn TopOn TopOn
3712, 12, 36mp2an 420 . . . . 5 TopOn
3837toponrestid 12083 . . . 4 t
399simprd 113 . . . . 5 # lim
40 cnex 7708 . . . . . . . . . . . . 13
4140a1i 9 . . . . . . . . . . . 12
4241, 5ssexd 4036 . . . . . . . . . . . 12
43 elpm2r 6526 . . . . . . . . . . . 12
4441, 42, 25, 7, 43syl22anc 1200 . . . . . . . . . . 11
45 reldvg 12691 . . . . . . . . . . 11
465, 44, 45syl2anc 406 . . . . . . . . . 10
47 dvadd.bg . . . . . . . . . 10
48 releldm 4742 . . . . . . . . . 10
4946, 47, 48syl2anc 406 . . . . . . . . 9
50 eqid 2115 . . . . . . . . . 10 t t
5150, 3dvcnp2cntop 12706 . . . . . . . . 9 t
525, 25, 7, 49, 51syl31anc 1202 . . . . . . . 8 t
533, 50cnplimccntop 12682 . . . . . . . . 9 t lim
5411, 23, 53syl2anc 406 . . . . . . . 8 t lim
5552, 54mpbid 146 . . . . . . 7 lim
5655simprd 113 . . . . . 6 lim
5725, 11limcdifap 12674 . . . . . . 7 lim # lim
58 ssrab2 3150 . . . . . . . . . 10 #
5958a1i 9 . . . . . . . . 9 #
6025, 59feqresmpt 5441 . . . . . . . 8 # #
6160oveq1d 5755 . . . . . . 7 # lim # lim
6257, 61eqtrd 2148 . . . . . 6 lim # lim
6356, 62eleqtrd 2194 . . . . 5 # lim
643mulcncntop 12618 . . . . . 6
655, 6, 7dvcl 12695 . . . . . . . 8
661, 65mpdan 415 . . . . . . 7
6725, 23ffvelrnd 5522 . . . . . . 7
6866, 67opelxpd 4540 . . . . . 6
6937toponunii 12079 . . . . . . 7
7069cncnpi 12292 . . . . . 6
7164, 68, 70sylancr 408 . . . . 5
7224, 29, 35, 35, 3, 38, 39, 63, 71limccnp2cntop 12689 . . . 4 # lim
73 eqid 2115 . . . . . . . 8 # #
742, 3, 73, 5, 25, 7eldvap 12694 . . . . . . 7 t # lim
7547, 74mpbid 146 . . . . . 6 t # lim
7675simprd 113 . . . . 5 # lim
77 cncfmptc 12646 . . . . . . . 8
7832, 11, 35, 77syl3anc 1199 . . . . . . 7
79 eqidd 2116 . . . . . . 7
8078, 23, 79cnmptlimc 12686 . . . . . 6 lim
8132adantr 272 . . . . . . . . 9
8281fmpttd 5541 . . . . . . . 8
8382, 11limcdifap 12674 . . . . . . 7 lim # lim
84 resmpt 4835 . . . . . . . . 9 # # #
8558, 84mp1i 10 . . . . . . . 8 # #
8685oveq1d 5755 . . . . . . 7 # lim # lim
8783, 86eqtrd 2148 . . . . . 6 lim # lim
8880, 87eleqtrd 2194 . . . . 5 # lim
895, 25, 7dvcl 12695 . . . . . . . 8
9047, 89mpdan 415 . . . . . . 7
9190, 32opelxpd 4540 . . . . . 6
9269cncnpi 12292 . . . . . 6
9364, 91, 92sylancr 408 . . . . 5
9431, 33, 35, 35, 3, 38, 76, 88, 93limccnp2cntop 12689 . . . 4 # lim
953addcncntop 12616 . . . . 5
9666, 67mulcld 7750 . . . . . 6
9790, 32mulcld 7750 . . . . . 6
9896, 97opelxpd 4540 . . . . 5
9969cncnpi 12292 . . . . 5
10095, 98, 99sylancr 408 . . . 4
10130, 34, 35, 35, 3, 38, 72, 94, 100limccnp2cntop 12689 . . 3 # lim
1026adantr 272 . . . . . . . . . 10 #
103102, 28ffvelrnd 5522 . . . . . . . . 9 #
104103, 33subcld 8037 . . . . . . . 8 #
105104, 29mulcld 7750 . . . . . . 7 #
10667adantr 272 . . . . . . . . 9 #
10729, 106subcld 8037 . . . . . . . 8 #
108107, 33mulcld 7750 . . . . . . 7 #
10911adantr 272 . . . . . . . . 9 #
110109, 28sseldd 3066 . . . . . . . 8 #
11111, 23sseldd 3066 . . . . . . . . 9
112111adantr 272 . . . . . . . 8 #
113110, 112subcld 8037 . . . . . . 7 #
114 breq1 3900 . . . . . . . . . . 11 # #
115114elrab 2811 . . . . . . . . . 10 # #
116115simprbi 271 . . . . . . . . 9 # #
117116adantl 273 . . . . . . . 8 # #
118110, 112, 117subap0d 8368 . . . . . . 7 # #
119105, 108, 113, 118divdirapd 8549 . . . . . 6 #
120103, 29mulcld 7750 . . . . . . . . 9 #
12133, 29mulcld 7750 . . . . . . . . 9 #
12233, 106mulcld 7750 . . . . . . . . 9 #
123120, 121, 122npncand 8061 . . . . . . . 8 #
124103, 33, 29subdird 8141 . . . . . . . . 9 #
125107, 33mulcomd 7751 . . . . . . . . . 10 #
12633, 29, 106subdid 8140 . . . . . . . . . 10 #
127125, 126eqtrd 2148 . . . . . . . . 9 #
128124, 127oveq12d 5758 . . . . . . . 8 #
12928, 28elind 3229 . . . . . . . . . 10 #
1306ffnd 5241 . . . . . . . . . . . 12
131130adantr 272 . . . . . . . . . . 11 #
13225ffnd 5241 . . . . . . . . . . . 12
133132adantr 272 . . . . . . . . . . 11 #
134 ssexg 4035 . . . . . . . . . . . . 13
13511, 40, 134sylancl 407 . . . . . . . . . . . 12
136135adantr 272 . . . . . . . . . . 11 #
137 eqid 2115 . . . . . . . . . . 11
138 eqidd 2116 . . . . . . . . . . 11 #
139 eqidd 2116 . . . . . . . . . . 11 #
140120adantr 272 . . . . . . . . . . 11 #
141131, 133, 136, 136, 137, 138, 139, 140ofvalg 5957 . . . . . . . . . 10 #
142129, 141mpdan 415 . . . . . . . . 9 #
14323, 23elind 3229 . . . . . . . . . 10
144 eqidd 2116 . . . . . . . . . . 11 #
145 eqidd 2116 . . . . . . . . . . 11 #
146122adantr 272 . . . . . . . . . . 11 #
147131, 133, 136, 136, 137, 144, 145, 146ofvalg 5957 . . . . . . . . . 10 #
148143, 147mpidan 417 . . . . . . . . 9 #
149142, 148oveq12d 5758 . . . . . . . 8 #
150123, 128, 1493eqtr4d 2158 . . . . . . 7 #
151150oveq1d 5755 . . . . . 6 #
152104, 29, 113, 118div23apd 8548 . . . . . . 7 #
153107, 33, 113, 118div23apd 8548 . . . . . . 7 #
154152, 153oveq12d 5758 . . . . . 6 #
155119, 151, 1543eqtr3d 2156 . . . . 5 #
156155mpteq2dva 3986 . . . 4 # #
157156oveq1d 5755 . . 3 # lim # lim
158101, 157eleqtrrd 2195 . 2 # lim
159 eqid 2115 . . 3 # #
160 mulcl 7711 . . . . 5
161160adantl 273 . . . 4
162 inidm 3253 . . . 4
163161, 6, 25, 135, 135, 162off 5960 . . 3
1642, 3, 159, 5, 163, 7eldvap 12694 . 2 t # lim
16510, 158, 164mpbir2and 911 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wceq 1314   wcel 1463  crab 2395  cvv 2658   cin 3038   wss 3039  cop 3498  cuni 3704   class class class wbr 3897   cmpt 3957   cxp 4505   cdm 4507   cres 4509   ccom 4511   wrel 4512   wfn 5086  wf 5087  cfv 5091  (class class class)co 5740   cof 5946   cpm 6509  cc 7582   caddc 7587   cmul 7589   cmin 7897   # cap 8306   cdiv 8392  cabs 10709   ↾t crest 12015  cmopn 12049  ctop 12059  TopOnctopon 12072  cnt 12157   ccn 12249   ccnp 12250   ctx 12316  ccncf 12621   lim climc 12666   cdv 12667 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704  ax-addf 7706  ax-mulf 7707 This theorem depends on definitions:  df-bi 116  df-stab 799  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-isom 5100  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-of 5948  df-1st 6004  df-2nd 6005  df-recs 6168  df-frec 6254  df-map 6510  df-pm 6511  df-sup 6837  df-inf 6838  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8393  df-inn 8678  df-2 8736  df-3 8737  df-4 8738  df-n0 8929  df-z 9006  df-uz 9276  df-q 9361  df-rp 9391  df-xneg 9499  df-xadd 9500  df-seqfrec 10159  df-exp 10233  df-cj 10554  df-re 10555  df-im 10556  df-rsqrt 10710  df-abs 10711  df-rest 12017  df-topgen 12036  df-psmet 12051  df-xmet 12052  df-met 12053  df-bl 12054  df-mopn 12055  df-top 12060  df-topon 12073  df-bases 12105  df-ntr 12160  df-cn 12252  df-cnp 12253  df-tx 12317  df-cncf 12622  df-limced 12668  df-dvap 12669 This theorem is referenced by:  dvmulxx  12711  dvimulf  12713  dvef  12730
 Copyright terms: Public domain W3C validator