Theorem npcan 11376

Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)

Assertion

Ref	Expression
npcan	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Proof of Theorem npcan

Step	Hyp	Ref	Expression
1		subcl 11366	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
2		simpr 484	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3	1, 2	addcomd 11322	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵)))
4		pncan3 11375	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
5	4	ancoms 458	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
6	3, 5	eqtrd 2768	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   + caddc 11016   − cmin 11351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-ltxr 11158  df-sub 11353

This theorem is referenced by:  addsubass  11377  npncan  11389  nppcan  11390  nnpcan  11391  subcan2  11393  nnncan  11403  npcand  11483  nn1suc  12154  zlem1lt  12530  zltlem1  12531  peano5uzi  12568  nummac  12639  uzp1  12775  peano2uzr  12803  qbtwnre  13100  fz01en  13454  fzsuc2  13484  fseq1m1p1  13501  predfz  13555  fzoss2  13589  fzoaddel2  13622  fzosplitsnm1  13642  fldiv  13766  modfzo0difsn  13852  seqm1  13928  monoord2  13942  sermono  13943  seqf1olem1  13950  seqf1olem2  13951  seqz  13959  expm1t  13999  expubnd  14087  bcm1k  14224  bcn2  14228  hashfzo  14338  hashbclem  14361  hashf1  14366  seqcoll  14373  swrdfv2  14571  swrdspsleq  14575  swrdlsw  14577  ccatpfx  14610  cshwlen  14708  cshwidxmodr  14713  cshwidxm  14717  swrd2lsw  14861  shftlem  14977  shftfval  14979  seqshft  14994  iserex  15566  serf0  15590  iseralt  15594  sumrblem  15620  fsumm1  15660  mptfzshft  15687  binomlem  15738  binom1dif  15742  isumsplit  15749  climcndslem1  15758  binomrisefac  15951  bpolycl  15961  bpolysum  15962  bpolydiflem  15963  bpoly2  15966  bpoly3  15967  fsumcube  15969  ruclem12  16152  dvdssub2  16214  4sqlem19  16877  vdwapun  16888  vdwapid1  16889  vdwlem5  16899  vdwlem8  16902  vdwnnlem2  16910  ramub1lem2  16941  1259lem4  17047  1259prm  17049  2503prm  17053  4001prm  17058  gsumsgrpccat  18750  sylow1lem1  19512  efgsres  19652  efgredleme  19657  gsummptshft  19850  ablsimpgfindlem1  20023  icccvx  24876  reparphti  24924  reparphtiOLD  24925  ovolunlem1  25426  advlog  26591  cxpaddlelem  26689  ang180lem1  26747  ang180lem3  26749  asinlem2  26807  tanatan  26857  ppiub  27143  perfect1  27167  lgsquad2lem1  27323  rplogsumlem1  27423  selberg2lem  27489  logdivbnd  27495  pntrsumo1  27504  pntrsumbnd2  27506  ax5seglem3  28911  ax5seglem5  28913  axbtwnid  28919  axlowdimlem16  28937  axeuclidlem  28942  axcontlem2  28945  crctcshwlkn0lem6  29795  clwwlknonex2lem2  30090  clwwlknonex2  30091  eucrctshift  30225  cvmliftlem7  35356  nndivsub  36522  ltflcei  37669  itg2addnclem3  37734  mettrifi  37818  irrapxlem1  42940  rmspecsqrtnq  43024  jm2.24nn  43077  jm2.18  43106  jm2.23  43114  jm2.27c  43125  monoord2xrv  45606  itgsinexp  46078  2elfz2melfz  47443  sbgoldbwt  47902  sgoldbeven3prm  47908  evengpop3  47923  evengpoap3  47924  gpg5nbgrvtx13starlem2  48197  zlmodzxzsub  48485  ackval42  48822