Theorem npcan 10946

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 10936	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
2		simpr 488	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3	1, 2	addcomd 10893	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵)))
4		pncan3 10945	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
5	4	ancoms 462	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
6	3, 5	eqtrd 2793	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  (class class class)co 7156  ℂcc 10586   + caddc 10591   − cmin 10921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-po 5447  df-so 5448  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8305  df-en 8541  df-dom 8542  df-sdom 8543  df-pnf 10728  df-mnf 10729  df-ltxr 10731  df-sub 10923

This theorem is referenced by:  addsubass  10947  npncan  10958  nppcan  10959  nnpcan  10960  subcan2  10962  nnncan  10972  npcand  11052  nn1suc  11709  zlem1lt  12086  zltlem1  12087  peano5uzi  12123  nummac  12195  uzp1  12332  peano2uzr  12356  qbtwnre  12646  fz01en  12997  fzsuc2  13027  fseq1m1p1  13044  predfz  13094  fzoss2  13127  fzoaddel2  13155  fzosplitsnm1  13174  fldiv  13290  modfzo0difsn  13373  seqm1  13450  monoord2  13464  sermono  13465  seqf1olem1  13472  seqf1olem2  13473  seqz  13481  expm1t  13520  expubnd  13604  bcm1k  13738  bcn2  13742  hashfzo  13853  hashbclem  13873  hashf1  13880  seqcoll  13887  swrdfv2  14083  swrdspsleq  14087  swrdlsw  14089  addlenrevpfx  14112  ccatpfx  14123  cshwlen  14221  cshwidxmodr  14226  cshwidxm  14230  swrd2lsw  14374  shftlem  14488  shftfval  14490  seqshft  14505  iserex  15074  serf0  15098  iseralt  15102  sumrblem  15129  fsumm1  15167  mptfzshft  15194  binomlem  15245  binom1dif  15249  isumsplit  15256  climcndslem1  15265  binomrisefac  15457  bpolycl  15467  bpolysum  15468  bpolydiflem  15469  bpoly2  15472  bpoly3  15473  fsumcube  15475  ruclem12  15655  dvdssub2  15715  4sqlem19  16368  vdwapun  16379  vdwapid1  16380  vdwlem5  16390  vdwlem8  16393  vdwnnlem2  16401  ramub1lem2  16432  1259lem4  16539  1259prm  16541  2503prm  16545  4001prm  16550  gsumsgrpccat  18084  gsumccatOLD  18085  sylow1lem1  18804  efgsres  18945  efgredleme  18950  gsummptshft  19138  ablsimpgfindlem1  19311  icccvx  23665  reparphti  23712  ovolunlem1  24211  advlog  25358  cxpaddlelem  25453  ang180lem1  25508  ang180lem3  25510  asinlem2  25568  tanatan  25618  ppiub  25901  perfect1  25925  lgsquad2lem1  26081  rplogsumlem1  26181  selberg2lem  26247  logdivbnd  26253  pntrsumo1  26262  pntrsumbnd2  26264  ax5seglem3  26838  ax5seglem5  26840  axbtwnid  26846  axlowdimlem16  26864  axeuclidlem  26869  axcontlem2  26872  crctcshwlkn0lem6  27714  clwwlknonex2lem2  28006  clwwlknonex2  28007  eucrctshift  28141  cvmliftlem7  32782  nndivsub  34230  ltflcei  35360  itg2addnclem3  35425  mettrifi  35510  irrapxlem1  40181  rmspecsqrtnq  40265  jm2.24nn  40318  jm2.18  40347  jm2.23  40355  jm2.27c  40366  monoord2xrv  42534  itgsinexp  43008  2elfz2melfz  44302  sbgoldbwt  44721  sgoldbeven3prm  44727  evengpop3  44742  evengpoap3  44743  zlmodzxzsub  45188  ackval42  45534