Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dvmptneg | Structured version Visualization version GIF version |
Description: Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Ref | Expression |
---|---|
dvmptadd.s | โข (๐ โ ๐ โ {โ, โ}) |
dvmptadd.a | โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) |
dvmptadd.b | โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ ๐) |
dvmptadd.da | โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ ๐ด)) = (๐ฅ โ ๐ โฆ ๐ต)) |
Ref | Expression |
---|---|
dvmptneg | โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ -๐ด)) = (๐ฅ โ ๐ โฆ -๐ต)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvmptadd.s | . . 3 โข (๐ โ ๐ โ {โ, โ}) | |
2 | dvmptadd.a | . . 3 โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) | |
3 | dvmptadd.b | . . 3 โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ ๐) | |
4 | dvmptadd.da | . . 3 โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ ๐ด)) = (๐ฅ โ ๐ โฆ ๐ต)) | |
5 | neg1cn 12188 | . . . 4 โข -1 โ โ | |
6 | 5 | a1i 11 | . . 3 โข (๐ โ -1 โ โ) |
7 | 1, 2, 3, 4, 6 | dvmptcmul 25234 | . 2 โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ (-1 ยท ๐ด))) = (๐ฅ โ ๐ โฆ (-1 ยท ๐ต))) |
8 | 2 | mulm1d 11528 | . . . 4 โข ((๐ โง ๐ฅ โ ๐) โ (-1 ยท ๐ด) = -๐ด) |
9 | 8 | mpteq2dva 5192 | . . 3 โข (๐ โ (๐ฅ โ ๐ โฆ (-1 ยท ๐ด)) = (๐ฅ โ ๐ โฆ -๐ด)) |
10 | 9 | oveq2d 7353 | . 2 โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ (-1 ยท ๐ด))) = (๐ D (๐ฅ โ ๐ โฆ -๐ด))) |
11 | 1, 2, 3, 4 | dvmptcl 25229 | . . . 4 โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ โ) |
12 | 11 | mulm1d 11528 | . . 3 โข ((๐ โง ๐ฅ โ ๐) โ (-1 ยท ๐ต) = -๐ต) |
13 | 12 | mpteq2dva 5192 | . 2 โข (๐ โ (๐ฅ โ ๐ โฆ (-1 ยท ๐ต)) = (๐ฅ โ ๐ โฆ -๐ต)) |
14 | 7, 10, 13 | 3eqtr3d 2784 | 1 โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ -๐ด)) = (๐ฅ โ ๐ โฆ -๐ต)) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง wa 396 = wceq 1540 โ wcel 2105 {cpr 4575 โฆ cmpt 5175 (class class class)co 7337 โcc 10970 โcr 10971 1c1 10973 ยท cmul 10977 -cneg 11307 D cdv 25133 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5229 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 ax-cnex 11028 ax-resscn 11029 ax-1cn 11030 ax-icn 11031 ax-addcl 11032 ax-addrcl 11033 ax-mulcl 11034 ax-mulrcl 11035 ax-mulcom 11036 ax-addass 11037 ax-mulass 11038 ax-distr 11039 ax-i2m1 11040 ax-1ne0 11041 ax-1rid 11042 ax-rnegex 11043 ax-rrecex 11044 ax-cnre 11045 ax-pre-lttri 11046 ax-pre-lttrn 11047 ax-pre-ltadd 11048 ax-pre-mulgt0 11049 ax-pre-sup 11050 ax-addf 11051 ax-mulf 11052 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3917 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4853 df-int 4895 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5176 df-tr 5210 df-id 5518 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5575 df-se 5576 df-we 5577 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6238 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-isom 6488 df-riota 7293 df-ov 7340 df-oprab 7341 df-mpo 7342 df-of 7595 df-om 7781 df-1st 7899 df-2nd 7900 df-supp 8048 df-frecs 8167 df-wrecs 8198 df-recs 8272 df-rdg 8311 df-1o 8367 df-2o 8368 df-er 8569 df-map 8688 df-pm 8689 df-ixp 8757 df-en 8805 df-dom 8806 df-sdom 8807 df-fin 8808 df-fsupp 9227 df-fi 9268 df-sup 9299 df-inf 9300 df-oi 9367 df-card 9796 df-pnf 11112 df-mnf 11113 df-xr 11114 df-ltxr 11115 df-le 11116 df-sub 11308 df-neg 11309 df-div 11734 df-nn 12075 df-2 12137 df-3 12138 df-4 12139 df-5 12140 df-6 12141 df-7 12142 df-8 12143 df-9 12144 df-n0 12335 df-z 12421 df-dec 12539 df-uz 12684 df-q 12790 df-rp 12832 df-xneg 12949 df-xadd 12950 df-xmul 12951 df-icc 13187 df-fz 13341 df-fzo 13484 df-seq 13823 df-exp 13884 df-hash 14146 df-cj 14909 df-re 14910 df-im 14911 df-sqrt 15045 df-abs 15046 df-struct 16945 df-sets 16962 df-slot 16980 df-ndx 16992 df-base 17010 df-ress 17039 df-plusg 17072 df-mulr 17073 df-starv 17074 df-sca 17075 df-vsca 17076 df-ip 17077 df-tset 17078 df-ple 17079 df-ds 17081 df-unif 17082 df-hom 17083 df-cco 17084 df-rest 17230 df-topn 17231 df-0g 17249 df-gsum 17250 df-topgen 17251 df-pt 17252 df-prds 17255 df-xrs 17310 df-qtop 17315 df-imas 17316 df-xps 17318 df-mre 17392 df-mrc 17393 df-acs 17395 df-mgm 18423 df-sgrp 18472 df-mnd 18483 df-submnd 18528 df-mulg 18797 df-cntz 19019 df-cmn 19483 df-psmet 20695 df-xmet 20696 df-met 20697 df-bl 20698 df-mopn 20699 df-fbas 20700 df-fg 20701 df-cnfld 20704 df-top 22149 df-topon 22166 df-topsp 22188 df-bases 22202 df-cld 22276 df-ntr 22277 df-cls 22278 df-nei 22355 df-lp 22393 df-perf 22394 df-cn 22484 df-cnp 22485 df-haus 22572 df-tx 22819 df-hmeo 23012 df-fil 23103 df-fm 23195 df-flim 23196 df-flf 23197 df-xms 23579 df-ms 23580 df-tms 23581 df-cncf 24147 df-limc 25136 df-dv 25137 |
This theorem is referenced by: dvmptsub 25237 dvsincos 25251 rolle 25260 dvivth 25280 lhop2 25285 dvfsumge 25292 dvfsum2 25304 logtayl 25921 logccv 25924 fdvneggt 32880 fdvnegge 32882 expgrowth 42282 itgsin0pilem1 43835 itgsinexplem1 43839 itgsincmulx 43859 fourierdlem39 44031 etransclem46 44165 |
Copyright terms: Public domain | W3C validator |