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

Theorem negsubd 10991
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 (𝜑𝐴 ∈ ℂ)
pncand.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
negsubd (𝜑 → (𝐴 + -𝐵) = (𝐴𝐵))

Proof of Theorem negsubd
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 pncand.2 . 2 (𝜑𝐵 ∈ ℂ)
3 negsub 10922 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴𝐵))
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 + -𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   + caddc 10528  cmin 10858  -cneg 10859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-ltxr 10668  df-sub 10860  df-neg 10861
This theorem is referenced by:  mulsub  11071  mulsubaddmulsub  11092  divsubdir  11322  divsubdiv  11344  ofnegsub  11624  icoshftf1o  12848  fzosubel  13084  modsub12d  13284  expaddzlem  13460  binom2sub  13569  discr  13589  cjreb  14470  recj  14471  remullem  14475  imcj  14479  sqreulem  14707  subcn2  14939  lo1sub  14975  iseraltlem2  15027  iseraltlem3  15028  fsumshftm  15124  fsumsub  15131  incexclem  15179  incexc  15180  bpoly3  15400  efmival  15494  cosadd  15506  sinsub  15509  sincossq  15517  moddvds  15606  dvdsadd2b  15644  bitsres  15810  pythagtriplem4  16144  mulgdirlem  18196  mulgmodid  18204  mulgsubdir  18205  cnsubrg  20533  zringlpirlem3  20561  cphipval  23773  pjthlem1  23967  mbfsub  24190  mbfmulc2  24191  itg2monolem1  24278  itgcnlem  24317  iblsub  24349  itgsub  24353  itgmulc2  24361  dvmptsub  24491  dvmptdiv  24498  dvexp3  24502  dvsincos  24505  dvlipcn  24518  ftc2  24568  aaliou3lem6  24864  logdiv2  25127  tanarg  25129  advlogexp  25165  cxpsub  25192  abscxpbnd  25261  relogbdiv  25284  isosctrlem2  25324  angpieqvdlem  25333  quad2  25344  dcubic1lem  25348  dcubic2  25349  dcubic  25351  mcubic  25352  dquartlem2  25357  dquart  25358  quart1lem  25360  quartlem1  25362  quart  25366  asinlem2  25374  cosasin  25409  atanlogsublem  25420  atantan  25428  atantayl2  25443  ftalem5  25581  basellem9  25593  lgseisenlem1  25878  2sqlem4  25924  rpvmasum2  26015  log2sumbnd  26047  chpdifbndlem1  26056  pntpbnd1  26089  axsegconlem9  26638  axeuclidlem  26675  smcnlem  28401  ipval2  28411  ipasslem2  28536  dipsubdir  28552  his2sub  28796  pjhthlem1  29095  circlemeth  31810  logdivsqrle  31820  fwddifnp1  33523  knoppndvlem2  33749  itg2gt0cn  34828  iblsubnc  34834  itgsubnc  34835  itgmulc2nc  34841  ftc1anclem8  34855  ftc2nc  34857  areacirclem1  34863  dffltz  39149  3cubeslem3r  39162  mzpsubmpt  39218  pellexlem6  39309  pell1234qrreccl  39329  pellfund14  39373  rmxyneg  39395  rmxm1  39409  rmym1  39410  congsub  39445  jm2.19lem1  39464  jm2.19lem4  39467  jm2.19  39468  jm2.26lem3  39476  sineq0ALT  41148  sub2times  41416  fzisoeu  41443  supsubc  41497  sublimc  41809  reclimc  41810  itgsincmulx  42135  itgsbtaddcnst  42143  stoweidlem10  42172  stoweidlem13  42175  stoweidlem22  42184  stoweidlem23  42185  stoweidlem26  42188  stoweidlem42  42204  stoweidlem47  42209  stirlinglem5  42240  dirkertrigeqlem2  42261  fourierdlem26  42295  fourierdlem36  42305  fourierdlem40  42309  fourierdlem41  42310  fourierdlem48  42316  fourierdlem49  42317  fourierdlem64  42332  fourierdlem78  42346  fourierdlem92  42360  fourierdlem97  42365  fourierdlem101  42369  fourierdlem107  42375  etransclem17  42413  etransclem46  42442  sigarperm  42994  quad1  43662  requad1  43664  requad2  43665  dignn0flhalflem1  44603  1subrec1sub  44620  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653  rrx2linest2  44659  itscnhlc0yqe  44674  itschlc0yqe  44675  itsclc0yqsol  44679  itsclinecirc0b  44689  itsclquadb  44691
  Copyright terms: Public domain W3C validator