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

Theorem npcan 9729
Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
npcan  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  -  B )  +  B
)  =  A )

Proof of Theorem npcan
StepHypRef Expression
1 subcl 9719 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
2 simpr 461 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  B  e.  CC )
31, 2addcomd 9681 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  -  B )  +  B
)  =  ( B  +  ( A  -  B ) ) )
4 pncan3 9728 . . 3  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  ( B  +  ( A  -  B ) )  =  A )
54ancoms 453 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( B  +  ( A  -  B ) )  =  A )
63, 5eqtrd 2495 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  -  B )  +  B
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758  (class class class)co 6199   CCcc 9390    + caddc 9395    - cmin 9705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-po 4748  df-so 4749  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-er 7210  df-en 7420  df-dom 7421  df-sdom 7422  df-pnf 9530  df-mnf 9531  df-ltxr 9533  df-sub 9707
This theorem is referenced by:  addsubass  9730  npncan  9740  nppcan  9741  nnpcan  9742  subcan2  9744  nnncan  9754  npcand  9833  nn1suc  10453  elnnnn0  10733  zlem1lt  10806  zltlem1  10807  peano5uzi  10840  uzindOLD  10846  nummac  10897  uzp1  11004  peano2uzr  11020  qbtwnre  11279  fz01en  11593  fzsuc2  11630  fseq1m1p1  11651  fzm1  11656  fzoss2  11693  fzoaddel2  11714  fzosplitsnm1  11724  fldiv  11815  seqm1  11939  monoord2  11953  sermono  11954  seqf1olem1  11961  seqf1olem2  11962  seqz  11970  expm1t  12008  expubnd  12040  facnn2  12176  bcm1k  12207  bcn2  12211  hashfzo  12307  hashbclem  12322  hashf1  12327  seqcoll  12333  addlenrevswrd  12447  swrdspsleq  12459  swrdlsw  12463  wrdeqcats1  12485  cshwlen  12553  cshwidxmod  12557  cshwidxm  12561  swrd2lsw  12669  shftlem  12674  shftfval  12676  seqshft  12691  iserex  13251  serf0  13275  iseralt  13279  sumrblem  13305  fsumm1  13337  mptfzshft  13362  binomlem  13409  binom1dif  13413  isumsplit  13420  climcndslem1  13429  ruclem12  13640  dvdssub2  13687  4sqlem19  14141  vdwapun  14152  vdwapid1  14153  vdwlem5  14163  vdwlem8  14166  vdwnnlem2  14174  ramub1lem2  14205  1259lem4  14275  1259prm  14277  2503prm  14281  4001prm  14286  gsumccat  15637  sylow1lem1  16217  efgsres  16355  efgredleme  16360  gsummptshft  16550  icccvx  20653  reparphti  20700  ovolunlem1  21111  advlog  22231  cxpaddlelem  22321  ang180lem1  22337  ang180lem3  22339  asinlem2  22396  tanatan  22446  ppiub  22675  perfect1  22699  lgsquad2lem1  22829  rplogsumlem1  22865  selberg2lem  22931  logdivbnd  22937  pntrsumo1  22946  pntrsumbnd2  22948  ax5seglem3  23328  ax5seglem5  23330  axbtwnid  23336  axlowdimlem13  23351  axlowdimlem16  23354  axeuclidlem  23359  axcontlem2  23362  eupares  23747  gxsuc  23910  addinv  23990  fzspl  26221  cvmliftlem7  27323  binomrisefac  27688  predfz  27807  bpolycl  28338  bpolysum  28339  bpolydiflem  28340  bpoly2  28343  bpoly3  28344  fsumcube  28346  nndivsub  28446  ltflcei  28566  itg2addnclem3  28592  mettrifi  28800  irrapxlem1  29310  rmspecsqrnq  29394  jm2.24nn  29449  jm2.18  29484  jm2.23  29492  jm2.27c  29503  itgsinexp  29942  2elfz2melfz  30349  fzosplitprm1  30371  numclwwlkovf2ex  30826  zlmodzxzsub  30904
  Copyright terms: Public domain W3C validator