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

Theorem negsubd 10017
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 9947 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  -u B )  =  ( A  -  B ) )
41, 2, 3syl2anc 671 1  |-  ( ph  ->  ( A  +  -u B )  =  ( A  -  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454    e. wcel 1897  (class class class)co 6314   CCcc 9562    + caddc 9567    - cmin 9885   -ucneg 9886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-po 4773  df-so 4774  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-ltxr 9705  df-sub 9887  df-neg 9888
This theorem is referenced by:  mulsub  10088  divsubdir  10330  divsubdiv  10350  ofnegsub  10634  icoshftf1o  11783  fzosubel  12003  modsub12d  12178  expaddzlem  12346  binom2sub  12422  discr  12440  cjreb  13234  recj  13235  remullem  13239  imcj  13243  sqreulem  13470  subcn2  13706  lo1sub  13742  iseraltlem2  13797  iseraltlem3  13798  fsumshftm  13890  fsumsub  13897  incexclem  13942  incexc  13943  bpoly3  14159  efmival  14255  cosadd  14267  sinsub  14270  sincossq  14278  moddvds  14360  dvdsadd2b  14395  bitsres  14495  pythagtriplem4  14817  mulgdirlem  16830  mulgsubdir  16837  cnsubrg  19076  zringlpirlem3OLD  19103  zringlpirlem3  19105  pjthlem1  22439  mbfsub  22666  mbfmulc2  22667  itg2monolem1  22756  itgcnlem  22795  iblsub  22827  itgsub  22831  itgmulc2  22839  dvmptsub  22969  dvexp3  22978  dvsincos  22981  dvlipcn  22994  ftc2  23044  aaliou3lem6  23352  logdiv2  23614  tanarg  23616  advlogexp  23648  cxpsub  23675  abscxpbnd  23741  relogbdiv  23764  isosctrlem2  23796  angpieqvdlem  23802  quad2  23813  dcubic1lem  23817  dcubic2  23818  dcubic  23820  mcubic  23821  dquartlem2  23826  dquart  23827  quart1lem  23829  quartlem1  23831  quart  23835  asinlem2  23843  cosasin  23878  atanlogsublem  23889  atantan  23897  atantayl2  23912  ftalem5  24049  ftalem5OLD  24051  basellem9  24063  lgseisenlem1  24325  2sqlem4  24343  rpvmasum2  24398  log2sumbnd  24430  chpdifbndlem1  24439  pntpbnd1  24472  axsegconlem9  25003  axeuclidlem  25040  gxmodid  26055  smcnlem  26381  ipval2  26391  ipasslem2  26521  dipsubdir  26537  his2sub  26793  pjhthlem1  27092  fwddifnp1  30980  itg2gt0cn  32041  iblsubnc  32047  itgsubnc  32048  itgmulc2nc  32054  ftc1anclem8  32068  ftc2nc  32070  areacirclem1  32076  mzpsubmpt  35629  pellexlem6  35722  pell1234qrreccl  35744  pellfund14  35790  rmxyneg  35812  rmxm1  35826  rmym1  35827  congsub  35864  jm2.19lem1  35888  jm2.19lem4  35891  jm2.19  35892  jm2.26lem3  35900  sineq0ALT  37373  sub2times  37520  fzisoeu  37555  supsubc  37613  sublimc  37770  reclimc  37771  dvmptdiv  37826  itgsincmulx  37888  itgsbtaddcnst  37896  stoweidlem10  37907  stoweidlem13  37910  stoweidlem22  37919  stoweidlem23  37920  stoweidlem26  37923  stoweidlem42  37940  stoweidlem47  37945  stirlinglem5  37977  dirkertrigeqlem2  37998  fourierdlem26  38032  fourierdlem36  38043  fourierdlem40  38047  fourierdlem41  38048  fourierdlem48  38055  fourierdlem49  38056  fourierdlem64  38071  fourierdlem78  38085  fourierdlem92  38099  fourierdlem97  38104  fourierdlem101  38108  fourierdlem107  38114  etransclem17  38153  etransclem46  38182  sigarperm  38506  dignn0flhalflem1  40698
  Copyright terms: Public domain W3C validator