Theorem npcan 11484

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 11474	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
2		simpr 490	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3	1, 2	addcomd 11430	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵)))
4		pncan3 11483	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
5	4	ancoms 464	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
6	3, 5	eqtrd 2801	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   + caddc 11121   − cmin 11459

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-po 5574  df-so 5575  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-ltxr 11266  df-sub 11461

This theorem is used by:  addsubass  11485  npncan  11497  nppcan  11498  nnpcan  11499  subcan2  11501  nnncan  11511  npcand  11591  nn1suc  12273  zlem1lt  12664  zltlem1  12665  peano5uzi  12703  nummac  12779  uzp1  12917  peano2uzr  12945  qbtwnre  13243  fz01en  13599  fzsuc2  13629  fseq1m1p1  13646  predfz  13700  fzoss2  13735  fzoaddel2  13768  fzosplitsnm1  13788  fldiv  13913  modfzo0difsn  13999  seqm1  14075  monoord2  14089  sermono  14090  seqf1olem1  14097  seqf1olem2  14098  seqz  14106  expm1t  14146  expubnd  14234  bcm1k  14371  bcn2  14375  hashfzo  14486  hashbclem  14509  hashf1  14514  seqcoll  14521  swrdfv2  14723  swrdspsleq  14727  swrdlsw  14729  ccatpfx  14762  cshwlen  14862  cshwidxmodr  14867  cshwidxm  14871  swrd2lsw  15015  shftlem  15131  shftfval  15133  seqshft  15148  iserex  15734  serf0  15758  iseralt  15762  sumrblem  15788  fsumm1  15828  mptfzshft  15855  binomlem  15909  binom1dif  15913  isumsplit  15920  climcndslem1  15929  binomrisefac  16121  bpolycl  16131  bpolysum  16132  bpolydiflem  16133  bpoly2  16136  bpoly3  16137  fsumcube  16139  ruclem12  16322  dvdssub2  16384  4sqlem19  17048  vdwapun  17059  vdwapid1  17060  vdwlem5  17070  vdwlem8  17073  vdwnnlem2  17081  ramub1lem2  17112  1259lem4  17219  1259prm  17221  2503prm  17225  4001prm  17230  gsumsgrpccat  18930  sylow1lem1  19699  efgsres  19839  efgredleme  19844  gsummptshft  20037  ablsimpgfindlem1  20210  icccvx  25146  reparphti  25193  ovolunlem1  25693  advlog  26856  cxpaddlelem  26953  ang180lem1  27011  ang180lem3  27013  asinlem2  27071  tanatan  27121  ppiub  27405  perfect1  27429  lgsquad2lem1  27585  rplogsumlem1  27685  selberg2lem  27751  logdivbnd  27757  pntrsumo1  27766  pntrsumbnd2  27768  ax5seglem3  29318  ax5seglem5  29320  axbtwnid  29326  axlowdimlem16  29344  axeuclidlem  29349  axcontlem2  29352  crctcshwlkn0lem6  30201  clwwlknonex2lem2  30496  clwwlknonex2  30497  eucrctshift  30631  cvmliftlem7  35804  nndivsub  37009  ltflcei  38300  itg2addnclem3  38365  mettrifi  38449  irrapxlem1  43590  rmspecsqrtnq  43674  jm2.24nn  43727  jm2.18  43756  jm2.23  43764  jm2.27c  43775  monoord2xrv  46238  itgsinexp  46710  2elfz2melfz  48096  sbgoldbwt  48583  sgoldbeven3prm  48589  evengpop3  48604  evengpoap3  48605  gpg5nbgrvtx13starlem2  48878  zlmodzxzsub  49181  ackval42  49517