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

Theorem npcand 10978
Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
negidd.1 (𝜑𝐴 ∈ ℂ)
pncand.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
npcand (𝜑 → ((𝐴𝐵) + 𝐵) = 𝐴)

Proof of Theorem npcand
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 pncand.2 . 2 (𝜑𝐵 ∈ ℂ)
3 npcan 10872 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴𝐵) + 𝐵) = 𝐴)
41, 2, 3syl2anc 587 1 (𝜑 → ((𝐴𝐵) + 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  (class class class)co 7130  cc 10512   + caddc 10517  cmin 10847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-po 5447  df-so 5448  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-er 8264  df-en 8485  df-dom 8486  df-sdom 8487  df-pnf 10654  df-mnf 10655  df-ltxr 10657  df-sub 10849
This theorem is referenced by:  addlsub  11033  npcan1  11042  ltsubadd  11087  lesubadd  11089  lesub1  11111  lincmb01cmp  12863  expaddzlem  13456  bcpasc  13665  bcn2m1  13668  cshwidxmod  14144  repswcshw  14153  swrds2m  14282  shftuz  14407  o1dif  14965  arisum2  15195  ntrivcvg  15232  ntrivcvgtail  15235  prodrblem  15262  fprodser  15282  fprodm1  15300  risefacval2  15343  fallfacval2  15344  fallfacfwd  15369  binomfallfaclem2  15373  sin01bnd  15517  moddvds  15597  dvdsexp  15656  bitscmp  15764  hashdvds  16089  vdwlem5  16298  vdwlem6  16299  vdwlem8  16301  srgbinomlem4  19271  uniioombllem3  24167  i1faddlem  24275  itg1addlem4  24281  dvcnp2  24501  ftc1lem4  24620  dgrcolem2  24849  plydivlem4  24870  aaliou3lem8  24919  dvtaylp  24943  dvntaylp0  24945  taylthlem1  24946  efif1olem4  25115  tanarg  25188  quart1  25420  dmgmaddnn0  25590  lgamgulm2  25599  gamfac  25630  basellem9  25652  chtublem  25773  logexprlim  25787  dchrptlem1  25826  lgsquadlem1  25942  mudivsum  26092  logsqvma  26104  log2sumbnd  26106  selberglem2  26108  pntrlog2bndlem5  26143  pntlem3  26171  ostth2lem2  26196  brbtwn2  26677  cusgrsize2inds  27221  clwlkclwwlklem2  27763  clwwisshclwws  27778  clwwlkel  27809  clwwlkf  27810  clwwlknonex2lem1  27870  2clwwlk2clwwlk  28113  numclwwlk2  28144  fzspl  30499  fzsplit3  30503  bcm1n  30504  wrdt2ind  30613  swrdrn3  30615  omndmul3  30721  psgnfzto1stlem  30749  cycpmco2lem5  30779  cycpmco2lem6  30780  freshmansdream  30866  ballotlemfc0  31757  ballotlemfcc  31758  signstfvn  31846  reprsuc  31893  breprexplemc  31910  lpadlen2  31959  revwlk  32378  bcm1nt  32976  itg2addnclem  34988  ftc1cnnclem  35008  ftc1anc  35018  caushft  35079  lcmfunnnd  39168  lcmineqlem4  39188  lcmineqlem23  39207  fltnltalem  39415  pellexlem6  39572  rmspecfund  39647  rmyluc  39675  jm2.18  39726  jm2.25  39737  hbtlem4  39867  bccm1k  40831  binomcxplemwb  40837  binomcxplemnotnn0  40845  oddfl  41699  zltlesub  41707  fzisoeu  41723  fperiodmul  41727  fzdifsuc2  41733  iccshift  41948  iooshift  41952  fmul01lt1lem2  42020  limcperiod  42063  sumnnodd  42065  cncfperiod  42314  fperdvper  42354  dvbdfbdioolem2  42364  dvnmul  42378  itgsinexp  42390  itgperiod  42416  stoweidlem11  42446  stoweidlem14  42449  stoweidlem26  42461  stoweidlem34  42469  wallispilem5  42504  stirlinglem5  42513  stirlinglem11  42519  stirlinglem12  42520  dirkercncflem1  42538  fourierdlem11  42553  fourierdlem15  42557  fourierdlem26  42568  fourierdlem41  42583  fourierdlem42  42584  fourierdlem48  42589  fourierdlem49  42590  fourierdlem63  42604  fourierdlem64  42605  fourierdlem65  42606  fourierdlem74  42615  fourierdlem75  42616  fourierdlem79  42620  fourierdlem81  42622  fourierdlem84  42625  fourierdlem88  42629  fourierdlem90  42631  fourierdlem92  42633  fourierdlem95  42636  fourierdlem97  42638  fourierdlem103  42644  fourierdlem104  42645  fourierdlem109  42650  fourierdlem111  42652  fourierswlem  42665  fouriersw  42666  elaa2lem  42668  etransclem23  42692  etransclem24  42693  etransclem28  42697  etransclem38  42707  smfmullem1  43216  fargshiftfo  43752  lighneallem3  43919  nnsum4primeseven  44112  nnsum4primesevenALTV  44113  bgoldbtbndlem4  44120  bgoldbtbnd  44121  m1modmmod  44728  dignn0flhalflem1  44822  affineid  44880  eenglngeehlnmlem1  44913  itsclquadb  44952
  Copyright terms: Public domain W3C validator