Theorem npcan 11437

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078   − cmin 11412

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414

This theorem is referenced by:  addsubass  11438  npncan  11450  nppcan  11451  nnpcan  11452  subcan2  11454  nnncan  11464  npcand  11544  nn1suc  12215  zlem1lt  12592  zltlem1  12593  peano5uzi  12630  nummac  12701  uzp1  12841  peano2uzr  12869  qbtwnre  13166  fz01en  13520  fzsuc2  13550  fseq1m1p1  13567  predfz  13621  fzoss2  13655  fzoaddel2  13688  fzosplitsnm1  13708  fldiv  13829  modfzo0difsn  13915  seqm1  13991  monoord2  14005  sermono  14006  seqf1olem1  14013  seqf1olem2  14014  seqz  14022  expm1t  14062  expubnd  14150  bcm1k  14287  bcn2  14291  hashfzo  14401  hashbclem  14424  hashf1  14429  seqcoll  14436  swrdfv2  14633  swrdspsleq  14637  swrdlsw  14639  addlenrevpfx  14662  ccatpfx  14673  cshwlen  14771  cshwidxmodr  14776  cshwidxm  14780  swrd2lsw  14925  shftlem  15041  shftfval  15043  seqshft  15058  iserex  15630  serf0  15654  iseralt  15658  sumrblem  15684  fsumm1  15724  mptfzshft  15751  binomlem  15802  binom1dif  15806  isumsplit  15813  climcndslem1  15822  binomrisefac  16015  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  bpoly2  16030  bpoly3  16031  fsumcube  16033  ruclem12  16216  dvdssub2  16278  4sqlem19  16941  vdwapun  16952  vdwapid1  16953  vdwlem5  16963  vdwlem8  16966  vdwnnlem2  16974  ramub1lem2  17005  1259lem4  17111  1259prm  17113  2503prm  17117  4001prm  17122  gsumsgrpccat  18774  sylow1lem1  19535  efgsres  19675  efgredleme  19680  gsummptshft  19873  ablsimpgfindlem1  20046  icccvx  24855  reparphti  24903  reparphtiOLD  24904  ovolunlem1  25405  advlog  26570  cxpaddlelem  26668  ang180lem1  26726  ang180lem3  26728  asinlem2  26786  tanatan  26836  ppiub  27122  perfect1  27146  lgsquad2lem1  27302  rplogsumlem1  27402  selberg2lem  27468  logdivbnd  27474  pntrsumo1  27483  pntrsumbnd2  27485  ax5seglem3  28865  ax5seglem5  28867  axbtwnid  28873  axlowdimlem16  28891  axeuclidlem  28896  axcontlem2  28899  crctcshwlkn0lem6  29752  clwwlknonex2lem2  30044  clwwlknonex2  30045  eucrctshift  30179  cvmliftlem7  35285  nndivsub  36452  ltflcei  37609  itg2addnclem3  37674  mettrifi  37758  irrapxlem1  42817  rmspecsqrtnq  42901  jm2.24nn  42955  jm2.18  42984  jm2.23  42992  jm2.27c  43003  monoord2xrv  45486  itgsinexp  45960  2elfz2melfz  47323  sbgoldbwt  47782  sgoldbeven3prm  47788  evengpop3  47803  evengpoap3  47804  gpg5nbgrvtx13starlem2  48067  zlmodzxzsub  48352  ackval42  48689