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

Theorem negsubd 9993
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 9923 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  -u B )  =  ( A  -  B ) )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  +  -u B )  =  ( A  -  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1868  (class class class)co 6302   CCcc 9538    + caddc 9543    - cmin 9861   -ucneg 9862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-po 4771  df-so 4772  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9678  df-mnf 9679  df-ltxr 9681  df-sub 9863  df-neg 9864
This theorem is referenced by:  mulsub  10062  divsubdir  10304  divsubdiv  10324  ofnegsub  10608  icoshftf1o  11756  fzosubel  11973  modsub12d  12147  expaddzlem  12315  binom2sub  12391  discr  12409  cjreb  13175  recj  13176  remullem  13180  imcj  13184  sqreulem  13411  subcn2  13646  lo1sub  13682  iseraltlem2  13737  iseraltlem3  13738  fsumshftm  13830  fsumsub  13837  incexclem  13882  incexc  13883  bpoly3  14099  efmival  14195  cosadd  14207  sinsub  14210  sincossq  14218  moddvds  14300  dvdsadd2b  14335  bitsres  14435  pythagtriplem4  14757  mulgdirlem  16770  mulgsubdir  16777  cnsubrg  19016  zringlpirlem3OLD  19042  zringlpirlem3  19044  pjthlem1  22378  mbfsub  22605  mbfmulc2  22606  itg2monolem1  22695  itgcnlem  22734  iblsub  22766  itgsub  22770  itgmulc2  22778  dvmptsub  22908  dvexp3  22917  dvsincos  22920  dvlipcn  22933  ftc2  22983  aaliou3lem6  23291  logdiv2  23553  tanarg  23555  advlogexp  23587  cxpsub  23614  abscxpbnd  23680  relogbdiv  23703  isosctrlem2  23735  angpieqvdlem  23741  quad2  23752  dcubic1lem  23756  dcubic2  23757  dcubic  23759  mcubic  23760  dquartlem2  23765  dquart  23766  quart1lem  23768  quartlem1  23770  quart  23774  asinlem2  23782  cosasin  23817  atanlogsublem  23828  atantan  23836  atantayl2  23851  ftalem5  23988  ftalem5OLD  23990  basellem9  24002  lgseisenlem1  24264  2sqlem4  24282  rpvmasum2  24337  log2sumbnd  24369  chpdifbndlem1  24378  pntpbnd1  24411  axsegconlem9  24942  axeuclidlem  24979  gxmodid  25993  smcnlem  26319  ipval2  26329  ipasslem2  26459  dipsubdir  26475  his2sub  26731  pjhthlem1  27030  fwddifnp1  30925  itg2gt0cn  31911  iblsubnc  31917  itgsubnc  31918  itgmulc2nc  31924  ftc1anclem8  31938  ftc2nc  31940  areacirclem1  31946  mzpsubmpt  35504  pellexlem6  35598  pell1234qrreccl  35620  pellfund14  35666  rmxyneg  35688  rmxm1  35702  rmym1  35703  congsub  35740  jm2.19lem1  35764  jm2.19lem4  35767  jm2.19  35768  jm2.26lem3  35776  sineq0ALT  37195  sub2times  37325  fzisoeu  37360  sublimc  37553  reclimc  37554  dvmptdiv  37609  itgsincmulx  37671  itgsbtaddcnst  37679  stoweidlem10  37690  stoweidlem13  37693  stoweidlem22  37702  stoweidlem23  37703  stoweidlem26  37706  stoweidlem42  37723  stoweidlem47  37728  stirlinglem5  37760  dirkertrigeqlem2  37781  fourierdlem26  37815  fourierdlem36  37826  fourierdlem40  37830  fourierdlem41  37831  fourierdlem48  37838  fourierdlem49  37839  fourierdlem64  37854  fourierdlem78  37868  fourierdlem92  37882  fourierdlem97  37887  fourierdlem101  37891  fourierdlem107  37897  etransclem17  37936  etransclem46  37965  sigarperm  38182  dignn0flhalflem1  39700
  Copyright terms: Public domain W3C validator