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

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

Proof of Theorem pncan
StepHypRef Expression
1 simpr 448 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  B  e.  CC )
2 simpl 444 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  A  e.  CC )
31, 2addcomd 9193 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( B  +  A
)  =  ( A  +  B ) )
4 addcl 8998 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
5 subadd 9233 . . 3  |-  ( ( ( A  +  B
)  e.  CC  /\  B  e.  CC  /\  A  e.  CC )  ->  (
( ( A  +  B )  -  B
)  =  A  <->  ( B  +  A )  =  ( A  +  B ) ) )
64, 1, 2, 5syl3anc 1184 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  B )  -  B )  =  A  <-> 
( B  +  A
)  =  ( A  +  B ) ) )
73, 6mpbird 224 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  -  B
)  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717  (class class class)co 6013   CCcc 8914    + caddc 8919    - cmin 9216
This theorem is referenced by:  pncan2  9237  addsubass  9240  subid1  9247  nppcan2  9257  pncand  9337  nn1m1nn  9945  nnsub  9963  elnn0nn  10187  elz2  10223  zrevaddcl  10246  uzindOLD  10289  qrevaddcl  10521  irradd  10523  fzrev3  11035  fzrevral3  11056  fzval3  11101  seqf1olem1  11282  seqf1olem2  11283  subsq2  11409  bcp1nk  11528  bcp1m1  11531  bcpasc  11532  hashbclem  11621  wrdind  11711  shftlem  11803  shftval5  11813  isershft  12377  isercoll2  12382  fsump1  12460  fsumshft  12483  fsumtscopo  12501  fsumparts  12505  bcxmas  12535  isum1p  12541  climcndslem1  12549  geolim  12567  mertenslem2  12582  mertens  12583  eftlub  12630  effsumlt  12632  eirrlem  12723  dvdsadd  12808  3dvds  12832  prmind2  13010  iserodd  13129  fldivp1  13186  prmpwdvds  13192  pockthlem  13193  prmreclem4  13207  prmreclem6  13209  4sqlem11  13243  vdwapun  13262  ramub1lem1  13314  ramcl  13317  1259lem4  13373  1259prm  13375  2503lem2  13377  2503prm  13379  4001lem3  13382  4001prm  13384  efgsval2  15285  efgsrel  15286  pcoass  18913  shft2rab  19264  ovolicc2lem4  19276  uniioombllem3  19337  uniioombllem4  19338  dvexp  19699  dvfsumlem1  19770  degltp1le  19856  ply1divex  19919  plyaddlem1  19992  plymullem1  19993  dvply1  20061  dvply2g  20062  vieta1lem2  20088  aaliou3lem7  20126  dvradcnv  20197  pserdvlem2  20204  abssinper  20286  eff1o  20311  advlogexp  20406  atantayl3  20639  leibpilem1  20640  leibpilem2  20641  log2tlbnd  20645  log2ub  20649  birthday  20653  emcllem2  20695  harmonicbnd4  20709  wilthlem2  20712  basellem8  20730  ppiprm  20794  ppinprm  20795  chtprm  20796  chtnprm  20797  chpp1  20798  ppiublem2  20847  ppiub  20848  chtub  20856  perfectlem1  20873  perfectlem2  20874  perfect  20875  bcp1ctr  20923  bposlem6  20933  bposlem8  20935  lgsvalmod  20959  lgseisen  20997  lgsquadlem1  20998  lgsquad2lem1  21002  2sqlem10  21018  rplogsumlem1  21038  selberg2lem  21104  logdivbnd  21110  pntrsumo1  21119  pntpbnd2  21141  eupap1  21539  eupath2lem3  21542  gxadd  21704  lnfn0i  23386  subfacp1lem5  24642  subfacp1lem6  24643  subfacval2  24645  subfaclim  24646  cvmliftlem7  24750  cvmliftlem10  24753  elfzp1b  24888  fsumkthpow  25809  itg2addnc  25952  fdc  26133  mettrifi  26147  heiborlem4  26207  heiborlem6  26209  lzenom  26512  2nn0ind  26692  jm2.17a  26709  jm2.17b  26710  jm2.17c  26711  stoweidlem34  27444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634  ax-resscn 8973  ax-1cn 8974  ax-icn 8975  ax-addcl 8976  ax-addrcl 8977  ax-mulcl 8978  ax-mulrcl 8979  ax-mulcom 8980  ax-addass 8981  ax-mulass 8982  ax-distr 8983  ax-i2m1 8984  ax-1ne0 8985  ax-1rid 8986  ax-rnegex 8987  ax-rrecex 8988  ax-cnre 8989  ax-pre-lttri 8990  ax-pre-lttrn 8991  ax-pre-ltadd 8992
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-nel 2546  df-ral 2647  df-rex 2648  df-reu 2649  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-br 4147  df-opab 4201  df-mpt 4202  df-id 4432  df-po 4437  df-so 4438  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-ov 6016  df-oprab 6017  df-mpt2 6018  df-riota 6478  df-er 6834  df-en 7039  df-dom 7040  df-sdom 7041  df-pnf 9048  df-mnf 9049  df-ltxr 9051  df-sub 9218
  Copyright terms: Public domain W3C validator