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

Theorem negsubd 9159
Description: Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
negidd.1  |-  ( ph  ->  A  e.  CC )
pncand.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
negsubd  |-  ( ph  ->  ( A  +  -u B )  =  ( A  -  B ) )

Proof of Theorem negsubd
StepHypRef Expression
1 negidd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 pncand.2 . 2  |-  ( ph  ->  B  e.  CC )
3 negsub 9091 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  -u B )  =  ( A  -  B ) )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  ( A  +  -u B )  =  ( A  -  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1624    e. wcel 1685  (class class class)co 5820   CCcc 8731    + caddc 8736    - cmin 9033   -ucneg 9034
This theorem is referenced by:  mulsub  9218  divsubdir  9452  divsubdiv  9472  ofnegsub  9740  icoshftf1o  10754  fzosubel  10903  modsub12d  11001  expaddzlem  11140  binom2sub  11215  discr  11233  cjreb  11603  recj  11604  remullem  11608  imcj  11612  sqreulem  11838  subcn2  12063  lo1sub  12099  iseraltlem2  12150  iseraltlem3  12151  fsumshftm  12238  fsumsub  12245  incexclem  12290  incexc  12291  efmival  12428  cosadd  12440  sinsub  12443  sincossq  12451  moddvds  12533  dvdsadd2b  12566  bitsres  12659  pythagtriplem4  12867  mulgdirlem  14586  mulgsubdir  14593  cnsubrg  16427  zlpirlem3  16438  pjthlem1  18796  mbfsub  19012  mbfmulc2  19013  itg2monolem1  19100  itgcnlem  19139  iblsub  19171  itgsub  19175  itgmulc2  19183  dvmptsub  19311  dvexp3  19320  dvsincos  19323  dvlipcn  19336  ftc2  19386  aaliou3lem6  19723  tanarg  19965  advlogexp  19997  cxpsub  20024  abscxpbnd  20088  isosctrlem2  20114  angpieqvdlem  20120  quad2  20130  dcubic1lem  20134  dcubic2  20135  dcubic  20137  mcubic  20138  dquartlem2  20143  dquart  20144  quart1lem  20146  quartlem1  20148  quart  20152  asinlem2  20160  cosasin  20195  atanlogsublem  20206  atantan  20214  atantayl2  20229  ftalem5  20309  basellem9  20321  lgseisenlem1  20583  2sqlem4  20601  rpvmasum2  20656  log2sumbnd  20688  chpdifbndlem1  20697  pntpbnd1  20730  gxmodid  20939  smcnlem  21263  ipval2  21273  ipasslem2  21403  dipsubdir  21419  his2sub  21664  pjhthlem1  21963  axsegconlem9  23961  axeuclidlem  23998  mslb1  25007  mzpsubmpt  26221  pellexlem6  26319  pell1234qrreccl  26339  pellfund14  26383  rmxyneg  26405  rmxm1  26419  rmym1  26420  congsub  26457  jm2.19lem1  26482  jm2.19lem4  26485  jm2.19  26486  jm2.26lem3  26494  stirlinglem5  27227
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-resscn 8790  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-mulcom 8797  ax-addass 8798  ax-mulass 8799  ax-distr 8800  ax-i2m1 8801  ax-1ne0 8802  ax-1rid 8803  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806  ax-pre-lttri 8807  ax-pre-lttrn 8808  ax-pre-ltadd 8809
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4309  df-po 4314  df-so 4315  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5224  df-fn 5225  df-f 5226  df-f1 5227  df-fo 5228  df-f1o 5229  df-fv 5230  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-iota 6253  df-riota 6300  df-er 6656  df-en 6860  df-dom 6861  df-sdom 6862  df-pnf 8865  df-mnf 8866  df-ltxr 8868  df-sub 9035  df-neg 9036
  Copyright terms: Public domain W3C validator