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

Theorem npcan 9316
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 9307 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
2 simpr 449 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  B  e.  CC )
31, 2addcomd 9270 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  -  B )  +  B
)  =  ( B  +  ( A  -  B ) ) )
4 pncan3 9315 . . 3  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  ( B  +  ( A  -  B ) )  =  A )
54ancoms 441 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( B  +  ( A  -  B ) )  =  A )
63, 5eqtrd 2470 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  -  B )  +  B
)  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726  (class class class)co 6083   CCcc 8990    + caddc 8995    - cmin 9293
This theorem is referenced by:  addsubass  9317  npncan  9325  nppcan  9326  subcan2  9328  nnncan  9338  npcand  9417  nn1suc  10023  elnnnn0  10265  zlem1lt  10329  zltlem1  10330  peano5uzi  10360  uzindOLD  10366  nummac  10416  uzp1  10521  peano2uzr  10534  qbtwnre  10787  fz01en  11081  fzsuc2  11106  fseq1m1p1  11125  fzm1  11129  fzoss2  11165  fzoaddel2  11178  fldiv  11243  seqm1  11342  monoord2  11356  sermono  11357  seqf1olem1  11364  seqf1olem2  11365  seqz  11373  expm1t  11410  expubnd  11442  facnn2  11577  bcm1k  11608  bcn2  11612  hashfzo  11696  hashbclem  11703  hashf1  11708  seqcoll  11714  wrdeqcats1  11790  shftlem  11885  shftfval  11887  seqshft  11902  iserex  12452  serf0  12476  iseralt  12480  sumrblem  12507  fsumm1  12539  fsumshft  12565  binomlem  12610  binom1dif  12614  isumsplit  12622  climcndslem1  12631  ruclem12  12842  dvdssub2  12889  4sqlem19  13333  vdwapun  13344  vdwapid1  13345  vdwlem5  13355  vdwlem8  13358  vdwnnlem2  13366  ramub1lem2  13397  1259lem4  13455  1259prm  13457  2503prm  13461  4001prm  13466  gsumccat  14789  sylow1lem1  15234  efgsres  15372  efgredleme  15377  icccvx  18977  reparphti  19024  ovolunlem1  19395  advlog  20547  cxpaddlelem  20637  ang180lem1  20653  ang180lem3  20655  asinlem2  20711  tanatan  20761  ppiub  20990  perfect1  21014  lgsquad2lem1  21144  rplogsumlem1  21180  selberg2lem  21246  logdivbnd  21252  pntrsumo1  21261  pntrsumbnd2  21263  eupares  21699  gxsuc  21862  addinv  21942  cvmliftlem7  24980  binomrisefac  25360  predfz  25480  ax5seglem3  25872  ax5seglem5  25874  axbtwnid  25880  axlowdimlem13  25895  axlowdimlem16  25898  axeuclidlem  25903  axcontlem2  25906  bpolycl  26100  bpolysum  26101  bpolydiflem  26102  bpoly2  26105  bpoly3  26106  fsumcube  26108  nndivsub  26209  ltflcei  26241  itg2addnclem3  26260  mettrifi  26465  irrapxlem1  26887  rmspecsqrnq  26971  jm2.24nn  27026  jm2.18  27061  jm2.23  27069  jm2.27c  27080  itgsinexp  27727  2elfz2melfz  28128  fzosplitsnm1  28142  addlenrevswrd  28207  cshwlen  28263  cshwidxm  28268  2cshw1lem1  28270  2cshw2lem1  28274  2cshw2lem2  28275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-po 4505  df-so 4506  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-riota 6551  df-er 6907  df-en 7112  df-dom 7113  df-sdom 7114  df-pnf 9124  df-mnf 9125  df-ltxr 9127  df-sub 9295
  Copyright terms: Public domain W3C validator