Theorem npcan 11489

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   + caddc 11130   − cmin 11464

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-ltxr 11272  df-sub 11466

This theorem is referenced by:  addsubass  11490  npncan  11502  nppcan  11503  nnpcan  11504  subcan2  11506  nnncan  11516  npcand  11596  nn1suc  12260  zlem1lt  12642  zltlem1  12643  peano5uzi  12680  nummac  12751  uzp1  12891  peano2uzr  12917  qbtwnre  13213  fz01en  13567  fzsuc2  13597  fseq1m1p1  13614  predfz  13668  fzoss2  13702  fzoaddel2  13734  fzosplitsnm1  13754  fldiv  13875  modfzo0difsn  13959  seqm1  14035  monoord2  14049  sermono  14050  seqf1olem1  14057  seqf1olem2  14058  seqz  14066  expm1t  14106  expubnd  14194  bcm1k  14331  bcn2  14335  hashfzo  14445  hashbclem  14468  hashf1  14473  seqcoll  14480  swrdfv2  14677  swrdspsleq  14681  swrdlsw  14683  addlenrevpfx  14706  ccatpfx  14717  cshwlen  14815  cshwidxmodr  14820  cshwidxm  14824  swrd2lsw  14969  shftlem  15085  shftfval  15087  seqshft  15102  iserex  15671  serf0  15695  iseralt  15699  sumrblem  15725  fsumm1  15765  mptfzshft  15792  binomlem  15843  binom1dif  15847  isumsplit  15854  climcndslem1  15863  binomrisefac  16056  bpolycl  16066  bpolysum  16067  bpolydiflem  16068  bpoly2  16071  bpoly3  16072  fsumcube  16074  ruclem12  16257  dvdssub2  16318  4sqlem19  16981  vdwapun  16992  vdwapid1  16993  vdwlem5  17003  vdwlem8  17006  vdwnnlem2  17014  ramub1lem2  17045  1259lem4  17151  1259prm  17153  2503prm  17157  4001prm  17162  gsumsgrpccat  18816  sylow1lem1  19577  efgsres  19717  efgredleme  19722  gsummptshft  19915  ablsimpgfindlem1  20088  icccvx  24897  reparphti  24945  reparphtiOLD  24946  ovolunlem1  25448  advlog  26613  cxpaddlelem  26711  ang180lem1  26769  ang180lem3  26771  asinlem2  26829  tanatan  26879  ppiub  27165  perfect1  27189  lgsquad2lem1  27345  rplogsumlem1  27445  selberg2lem  27511  logdivbnd  27517  pntrsumo1  27526  pntrsumbnd2  27528  ax5seglem3  28856  ax5seglem5  28858  axbtwnid  28864  axlowdimlem16  28882  axeuclidlem  28887  axcontlem2  28890  crctcshwlkn0lem6  29743  clwwlknonex2lem2  30035  clwwlknonex2  30036  eucrctshift  30170  cvmliftlem7  35259  nndivsub  36421  ltflcei  37578  itg2addnclem3  37643  mettrifi  37727  irrapxlem1  42792  rmspecsqrtnq  42876  jm2.24nn  42930  jm2.18  42959  jm2.23  42967  jm2.27c  42978  monoord2xrv  45458  itgsinexp  45932  2elfz2melfz  47295  sbgoldbwt  47739  sgoldbeven3prm  47745  evengpop3  47760  evengpoap3  47761  gpg5nbgrvtx13starlem2  48022  zlmodzxzsub  48283  ackval42  48624