Theorem npcan 11394

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 11384	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
2		simpr 485	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3	1, 2	addcomd 11340	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵)))
4		pncan3 11393	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
5	4	ancoms 459	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
6	3, 5	eqtrd 2774	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  (class class class)co 7357  ℂcc 11028   + caddc 11033   − cmin 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5155  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7314  df-ov 7360  df-oprab 7361  df-mpo 7362  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11173  df-mnf 11174  df-ltxr 11176  df-sub 11371

This theorem is referenced by:  addsubass  11395  npncan  11407  nppcan  11408  nnpcan  11409  subcan2  11411  nnncan  11421  npcand  11501  nn1suc  12188  zlem1lt  12571  zltlem1  12572  peano5uzi  12610  nummac  12681  uzp1  12817  peano2uzr  12845  qbtwnre  13143  fz01en  13498  fzsuc2  13528  fseq1m1p1  13545  predfz  13599  fzoss2  13634  fzoaddel2  13667  fzosplitsnm1  13687  fldiv  13811  modfzo0difsn  13897  seqm1  13973  monoord2  13987  sermono  13988  seqf1olem1  13995  seqf1olem2  13996  seqz  14004  expm1t  14044  expubnd  14132  bcm1k  14269  bcn2  14273  hashfzo  14383  hashbclem  14406  hashf1  14411  seqcoll  14418  swrdfv2  14616  swrdspsleq  14620  swrdlsw  14622  ccatpfx  14655  cshwlen  14753  cshwidxmodr  14758  cshwidxm  14762  swrd2lsw  14906  shftlem  15022  shftfval  15024  seqshft  15039  iserex  15611  serf0  15635  iseralt  15639  sumrblem  15665  fsumm1  15705  mptfzshft  15732  binomlem  15786  binom1dif  15790  isumsplit  15797  climcndslem1  15806  binomrisefac  15999  bpolycl  16009  bpolysum  16010  bpolydiflem  16011  bpoly2  16014  bpoly3  16015  fsumcube  16017  ruclem12  16200  dvdssub2  16262  4sqlem19  16926  vdwapun  16937  vdwapid1  16938  vdwlem5  16948  vdwlem8  16951  vdwnnlem2  16959  ramub1lem2  16990  1259lem4  17096  1259prm  17098  2503prm  17102  4001prm  17107  gsumsgrpccat  18800  sylow1lem1  19565  efgsres  19705  efgredleme  19710  gsummptshft  19903  ablsimpgfindlem1  20076  icccvx  24936  reparphti  24983  ovolunlem1  25483  advlog  26637  cxpaddlelem  26734  ang180lem1  26792  ang180lem3  26794  asinlem2  26852  tanatan  26902  ppiub  27186  perfect1  27210  lgsquad2lem1  27366  rplogsumlem1  27466  selberg2lem  27532  logdivbnd  27538  pntrsumo1  27547  pntrsumbnd2  27549  ax5seglem3  29019  ax5seglem5  29021  axbtwnid  29027  axlowdimlem16  29045  axeuclidlem  29050  axcontlem2  29053  crctcshwlkn0lem6  29902  clwwlknonex2lem2  30197  clwwlknonex2  30198  eucrctshift  30332  cvmliftlem7  35528  nndivsub  36694  ltflcei  37984  itg2addnclem3  38049  mettrifi  38133  irrapxlem1  43276  rmspecsqrtnq  43360  jm2.24nn  43413  jm2.18  43442  jm2.23  43450  jm2.27c  43461  monoord2xrv  45934  itgsinexp  46406  2elfz2melfz  47789  sbgoldbwt  48276  sgoldbeven3prm  48282  evengpop3  48297  evengpoap3  48298  gpg5nbgrvtx13starlem2  48571  zlmodzxzsub  48859  ackval42  49195