Theorem npcan 11430

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071   − cmin 11405

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 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407

This theorem is referenced by:  addsubass  11431  npncan  11443  nppcan  11444  nnpcan  11445  subcan2  11447  nnncan  11457  npcand  11537  nn1suc  12208  zlem1lt  12585  zltlem1  12586  peano5uzi  12623  nummac  12694  uzp1  12834  peano2uzr  12862  qbtwnre  13159  fz01en  13513  fzsuc2  13543  fseq1m1p1  13560  predfz  13614  fzoss2  13648  fzoaddel2  13681  fzosplitsnm1  13701  fldiv  13822  modfzo0difsn  13908  seqm1  13984  monoord2  13998  sermono  13999  seqf1olem1  14006  seqf1olem2  14007  seqz  14015  expm1t  14055  expubnd  14143  bcm1k  14280  bcn2  14284  hashfzo  14394  hashbclem  14417  hashf1  14422  seqcoll  14429  swrdfv2  14626  swrdspsleq  14630  swrdlsw  14632  addlenrevpfx  14655  ccatpfx  14666  cshwlen  14764  cshwidxmodr  14769  cshwidxm  14773  swrd2lsw  14918  shftlem  15034  shftfval  15036  seqshft  15051  iserex  15623  serf0  15647  iseralt  15651  sumrblem  15677  fsumm1  15717  mptfzshft  15744  binomlem  15795  binom1dif  15799  isumsplit  15806  climcndslem1  15815  binomrisefac  16008  bpolycl  16018  bpolysum  16019  bpolydiflem  16020  bpoly2  16023  bpoly3  16024  fsumcube  16026  ruclem12  16209  dvdssub2  16271  4sqlem19  16934  vdwapun  16945  vdwapid1  16946  vdwlem5  16956  vdwlem8  16959  vdwnnlem2  16967  ramub1lem2  16998  1259lem4  17104  1259prm  17106  2503prm  17110  4001prm  17115  gsumsgrpccat  18767  sylow1lem1  19528  efgsres  19668  efgredleme  19673  gsummptshft  19866  ablsimpgfindlem1  20039  icccvx  24848  reparphti  24896  reparphtiOLD  24897  ovolunlem1  25398  advlog  26563  cxpaddlelem  26661  ang180lem1  26719  ang180lem3  26721  asinlem2  26779  tanatan  26829  ppiub  27115  perfect1  27139  lgsquad2lem1  27295  rplogsumlem1  27395  selberg2lem  27461  logdivbnd  27467  pntrsumo1  27476  pntrsumbnd2  27478  ax5seglem3  28858  ax5seglem5  28860  axbtwnid  28866  axlowdimlem16  28884  axeuclidlem  28889  axcontlem2  28892  crctcshwlkn0lem6  29745  clwwlknonex2lem2  30037  clwwlknonex2  30038  eucrctshift  30172  cvmliftlem7  35278  nndivsub  36445  ltflcei  37602  itg2addnclem3  37667  mettrifi  37751  irrapxlem1  42810  rmspecsqrtnq  42894  jm2.24nn  42948  jm2.18  42977  jm2.23  42985  jm2.27c  42996  monoord2xrv  45479  itgsinexp  45953  2elfz2melfz  47319  sbgoldbwt  47778  sgoldbeven3prm  47784  evengpop3  47799  evengpoap3  47800  gpg5nbgrvtx13starlem2  48063  zlmodzxzsub  48348  ackval42  48685