Theorem npcan 11390

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 11380	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
2		simpr 484	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3	1, 2	addcomd 11336	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵)))
4		pncan3 11389	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
5	4	ancoms 458	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
6	3, 5	eqtrd 2764	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031   − cmin 11365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  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 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-sub 11367

This theorem is referenced by:  addsubass  11391  npncan  11403  nppcan  11404  nnpcan  11405  subcan2  11407  nnncan  11417  npcand  11497  nn1suc  12168  zlem1lt  12545  zltlem1  12546  peano5uzi  12583  nummac  12654  uzp1  12794  peano2uzr  12822  qbtwnre  13119  fz01en  13473  fzsuc2  13503  fseq1m1p1  13520  predfz  13574  fzoss2  13608  fzoaddel2  13641  fzosplitsnm1  13661  fldiv  13782  modfzo0difsn  13868  seqm1  13944  monoord2  13958  sermono  13959  seqf1olem1  13966  seqf1olem2  13967  seqz  13975  expm1t  14015  expubnd  14103  bcm1k  14240  bcn2  14244  hashfzo  14354  hashbclem  14377  hashf1  14382  seqcoll  14389  swrdfv2  14586  swrdspsleq  14590  swrdlsw  14592  ccatpfx  14625  cshwlen  14723  cshwidxmodr  14728  cshwidxm  14732  swrd2lsw  14877  shftlem  14993  shftfval  14995  seqshft  15010  iserex  15582  serf0  15606  iseralt  15610  sumrblem  15636  fsumm1  15676  mptfzshft  15703  binomlem  15754  binom1dif  15758  isumsplit  15765  climcndslem1  15774  binomrisefac  15967  bpolycl  15977  bpolysum  15978  bpolydiflem  15979  bpoly2  15982  bpoly3  15983  fsumcube  15985  ruclem12  16168  dvdssub2  16230  4sqlem19  16893  vdwapun  16904  vdwapid1  16905  vdwlem5  16915  vdwlem8  16918  vdwnnlem2  16926  ramub1lem2  16957  1259lem4  17063  1259prm  17065  2503prm  17069  4001prm  17074  gsumsgrpccat  18732  sylow1lem1  19495  efgsres  19635  efgredleme  19640  gsummptshft  19833  ablsimpgfindlem1  20006  icccvx  24864  reparphti  24912  reparphtiOLD  24913  ovolunlem1  25414  advlog  26579  cxpaddlelem  26677  ang180lem1  26735  ang180lem3  26737  asinlem2  26795  tanatan  26845  ppiub  27131  perfect1  27155  lgsquad2lem1  27311  rplogsumlem1  27411  selberg2lem  27477  logdivbnd  27483  pntrsumo1  27492  pntrsumbnd2  27494  ax5seglem3  28894  ax5seglem5  28896  axbtwnid  28902  axlowdimlem16  28920  axeuclidlem  28925  axcontlem2  28928  crctcshwlkn0lem6  29778  clwwlknonex2lem2  30070  clwwlknonex2  30071  eucrctshift  30205  cvmliftlem7  35263  nndivsub  36430  ltflcei  37587  itg2addnclem3  37652  mettrifi  37736  irrapxlem1  42795  rmspecsqrtnq  42879  jm2.24nn  42932  jm2.18  42961  jm2.23  42969  jm2.27c  42980  monoord2xrv  45463  itgsinexp  45937  2elfz2melfz  47303  sbgoldbwt  47762  sgoldbeven3prm  47768  evengpop3  47783  evengpoap3  47784  gpg5nbgrvtx13starlem2  48057  zlmodzxzsub  48345  ackval42  48682