Theorem npcan 11369

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   + caddc 11009   − cmin 11344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-po 5524  df-so 5525  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151  df-sub 11346

This theorem is referenced by:  addsubass  11370  npncan  11382  nppcan  11383  nnpcan  11384  subcan2  11386  nnncan  11396  npcand  11476  nn1suc  12147  zlem1lt  12524  zltlem1  12525  peano5uzi  12562  nummac  12633  uzp1  12773  peano2uzr  12801  qbtwnre  13098  fz01en  13452  fzsuc2  13482  fseq1m1p1  13499  predfz  13553  fzoss2  13587  fzoaddel2  13620  fzosplitsnm1  13640  fldiv  13764  modfzo0difsn  13850  seqm1  13926  monoord2  13940  sermono  13941  seqf1olem1  13948  seqf1olem2  13949  seqz  13957  expm1t  13997  expubnd  14085  bcm1k  14222  bcn2  14226  hashfzo  14336  hashbclem  14359  hashf1  14364  seqcoll  14371  swrdfv2  14569  swrdspsleq  14573  swrdlsw  14575  ccatpfx  14608  cshwlen  14706  cshwidxmodr  14711  cshwidxm  14715  swrd2lsw  14859  shftlem  14975  shftfval  14977  seqshft  14992  iserex  15564  serf0  15588  iseralt  15592  sumrblem  15618  fsumm1  15658  mptfzshft  15685  binomlem  15736  binom1dif  15740  isumsplit  15747  climcndslem1  15756  binomrisefac  15949  bpolycl  15959  bpolysum  15960  bpolydiflem  15961  bpoly2  15964  bpoly3  15965  fsumcube  15967  ruclem12  16150  dvdssub2  16212  4sqlem19  16875  vdwapun  16886  vdwapid1  16887  vdwlem5  16897  vdwlem8  16900  vdwnnlem2  16908  ramub1lem2  16939  1259lem4  17045  1259prm  17047  2503prm  17051  4001prm  17056  gsumsgrpccat  18748  sylow1lem1  19511  efgsres  19651  efgredleme  19656  gsummptshft  19849  ablsimpgfindlem1  20022  icccvx  24876  reparphti  24924  reparphtiOLD  24925  ovolunlem1  25426  advlog  26591  cxpaddlelem  26689  ang180lem1  26747  ang180lem3  26749  asinlem2  26807  tanatan  26857  ppiub  27143  perfect1  27167  lgsquad2lem1  27323  rplogsumlem1  27423  selberg2lem  27489  logdivbnd  27495  pntrsumo1  27504  pntrsumbnd2  27506  ax5seglem3  28910  ax5seglem5  28912  axbtwnid  28918  axlowdimlem16  28936  axeuclidlem  28941  axcontlem2  28944  crctcshwlkn0lem6  29794  clwwlknonex2lem2  30086  clwwlknonex2  30087  eucrctshift  30221  cvmliftlem7  35333  nndivsub  36497  ltflcei  37654  itg2addnclem3  37719  mettrifi  37803  irrapxlem1  42861  rmspecsqrtnq  42945  jm2.24nn  42998  jm2.18  43027  jm2.23  43035  jm2.27c  43046  monoord2xrv  45527  itgsinexp  45999  2elfz2melfz  47355  sbgoldbwt  47814  sgoldbeven3prm  47820  evengpop3  47835  evengpoap3  47836  gpg5nbgrvtx13starlem2  48109  zlmodzxzsub  48397  ackval42  48734