Theorem npcan 11467

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  (class class class)co 7402  ℂcc 11105   + caddc 11110   − cmin 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-po 5579  df-so 5580  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11248  df-mnf 11249  df-ltxr 11251  df-sub 11444

This theorem is referenced by:  addsubass  11468  npncan  11479  nppcan  11480  nnpcan  11481  subcan2  11483  nnncan  11493  npcand  11573  nn1suc  12232  zlem1lt  12612  zltlem1  12613  peano5uzi  12649  nummac  12720  uzp1  12861  peano2uzr  12885  qbtwnre  13176  fz01en  13527  fzsuc2  13557  fseq1m1p1  13574  predfz  13624  fzoss2  13658  fzoaddel2  13686  fzosplitsnm1  13705  fldiv  13823  modfzo0difsn  13906  seqm1  13983  monoord2  13997  sermono  13998  seqf1olem1  14005  seqf1olem2  14006  seqz  14014  expm1t  14054  expubnd  14140  bcm1k  14273  bcn2  14277  hashfzo  14387  hashbclem  14409  hashf1  14416  seqcoll  14423  swrdfv2  14609  swrdspsleq  14613  swrdlsw  14615  addlenrevpfx  14638  ccatpfx  14649  cshwlen  14747  cshwidxmodr  14752  cshwidxm  14756  swrd2lsw  14901  shftlem  15013  shftfval  15015  seqshft  15030  iserex  15601  serf0  15625  iseralt  15629  sumrblem  15655  fsumm1  15695  mptfzshft  15722  binomlem  15773  binom1dif  15777  isumsplit  15784  climcndslem1  15793  binomrisefac  15984  bpolycl  15994  bpolysum  15995  bpolydiflem  15996  bpoly2  15999  bpoly3  16000  fsumcube  16002  ruclem12  16183  dvdssub2  16243  4sqlem19  16897  vdwapun  16908  vdwapid1  16909  vdwlem5  16919  vdwlem8  16922  vdwnnlem2  16930  ramub1lem2  16961  1259lem4  17068  1259prm  17070  2503prm  17074  4001prm  17079  gsumsgrpccat  18757  sylow1lem1  19510  efgsres  19650  efgredleme  19655  gsummptshft  19848  ablsimpgfindlem1  20021  icccvx  24799  reparphti  24847  reparphtiOLD  24848  ovolunlem1  25350  advlog  26507  cxpaddlelem  26605  ang180lem1  26660  ang180lem3  26662  asinlem2  26720  tanatan  26770  ppiub  27056  perfect1  27080  lgsquad2lem1  27236  rplogsumlem1  27336  selberg2lem  27402  logdivbnd  27408  pntrsumo1  27417  pntrsumbnd2  27419  ax5seglem3  28661  ax5seglem5  28663  axbtwnid  28669  axlowdimlem16  28687  axeuclidlem  28692  axcontlem2  28695  crctcshwlkn0lem6  29541  clwwlknonex2lem2  29833  clwwlknonex2  29834  eucrctshift  29968  cvmliftlem7  34773  nndivsub  35833  ltflcei  36970  itg2addnclem3  37035  mettrifi  37119  irrapxlem1  42074  rmspecsqrtnq  42158  jm2.24nn  42212  jm2.18  42241  jm2.23  42249  jm2.27c  42260  monoord2xrv  44704  itgsinexp  45181  2elfz2melfz  46536  sbgoldbwt  46955  sgoldbeven3prm  46961  evengpop3  46976  evengpoap3  46977  zlmodzxzsub  47250  ackval42  47595