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

Theorem pncan 10325
Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
pncan ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)

Proof of Theorem pncan
StepHypRef Expression
1 simpr 476 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
2 simpl 472 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
31, 2addcomd 10276 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵))
4 addcl 10056 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5 subadd 10322 . . 3 (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
64, 1, 2, 5syl3anc 1366 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵)))
73, 6mpbird 247 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972   + caddc 9977  cmin 10304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-ltxr 10117  df-sub 10306
This theorem is referenced by:  pncan2  10326  addsubass  10329  pncan3oi  10335  subid1  10339  nppcan2  10350  pncand  10431  nn1m1nn  11078  nnsub  11097  elnn0nn  11373  elz2  11432  zrevaddcl  11460  nzadd  11463  qrevaddcl  11848  irradd  11850  fzrev3  12444  elfzp1b  12455  fzrevral3  12465  fzval3  12576  seqf1olem1  12880  seqf1olem2  12881  subsq2  13013  bcp1nk  13144  bcp1m1  13147  bcpasc  13148  hashbclem  13274  ccatalpha  13411  wrdind  13522  wrd2ind  13523  2cshwcshw  13617  shftlem  13852  shftval5  13862  isershft  14438  isercoll2  14443  fsump1  14531  mptfzshft  14554  telfsumo  14578  fsumparts  14582  bcxmas  14611  isum1p  14617  geolim  14645  mertenslem2  14661  mertens  14662  fsumkthpow  14831  eftlub  14883  effsumlt  14885  eirrlem  14976  dvdsadd  15071  prmind2  15445  iserodd  15587  fldivp1  15648  prmpwdvds  15655  pockthlem  15656  prmreclem4  15670  prmreclem6  15672  4sqlem11  15706  vdwapun  15725  ramub1lem1  15777  ramcl  15780  efgsval2  18192  efgsrel  18193  pcoass  22870  shft2rab  23322  uniioombllem3  23399  uniioombllem4  23400  dvexp  23761  dvfsumlem1  23834  degltp1le  23878  ply1divex  23941  plyaddlem1  24014  plymullem1  24015  dvply1  24084  dvply2g  24085  vieta1lem2  24111  aaliou3lem7  24149  dvradcnv  24220  pserdvlem2  24227  abssinper  24315  advlogexp  24446  atantayl3  24711  leibpilem1  24712  leibpilem2  24713  emcllem2  24768  harmonicbnd4  24782  wilthlem2  24840  basellem8  24859  ppiprm  24922  ppinprm  24923  chtprm  24924  chtnprm  24925  chpp1  24926  chtub  24982  perfectlem1  24999  perfectlem2  25000  perfect  25001  bcp1ctr  25049  lgsvalmod  25086  lgseisen  25149  lgsquadlem1  25150  lgsquad2lem1  25154  2sqlem10  25198  rplogsumlem1  25218  selberg2lem  25284  logdivbnd  25290  pntrsumo1  25299  pntpbnd2  25321  wwlksnext  26856  clwwlkf1  27012  subfacp1lem5  31292  subfacp1lem6  31293  subfacval2  31295  subfaclim  31296  cvmliftlem7  31399  cvmliftlem10  31402  mblfinlem2  33577  itg2addnclem3  33593  fdc  33671  mettrifi  33683  heiborlem4  33743  heiborlem6  33745  lzenom  37650  2nn0ind  37827  jm2.17a  37844  jm2.17b  37845  jm2.17c  37846  evensumeven  41941  perfectALTVlem2  41956  perfectALTV  41957
  Copyright terms: Public domain W3C validator