Theorem npcan 10749

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1525   ∈ wcel 2083  (class class class)co 7023  ℂcc 10388   + caddc 10393   − cmin 10723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-po 5369  df-so 5370  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-er 8146  df-en 8365  df-dom 8366  df-sdom 8367  df-pnf 10530  df-mnf 10531  df-ltxr 10533  df-sub 10725

This theorem is referenced by:  addsubass  10750  npncan  10761  nppcan  10762  nnpcan  10763  subcan2  10765  nnncan  10775  npcand  10855  nn1suc  11513  zlem1lt  11888  zltlem1  11889  peano5uzi  11925  nummac  11997  uzp1  12132  peano2uzr  12156  qbtwnre  12446  fz01en  12789  fzsuc2  12819  fseq1m1p1  12836  predfz  12886  fzoss2  12919  fzoaddel2  12947  fzosplitsnm1  12966  fldiv  13082  modfzo0difsn  13165  seqm1  13241  monoord2  13255  sermono  13256  seqf1olem1  13263  seqf1olem2  13264  seqz  13272  expm1t  13311  expubnd  13395  bcm1k  13529  bcn2  13533  hashfzo  13642  hashbclem  13662  hashf1  13667  seqcoll  13674  swrdfv2  13863  swrdspsleq  13867  swrdlsw  13869  addlenrevpfx  13892  cshwlen  14001  cshwidxmod  14005  cshwidxmodr  14006  cshwidxm  14010  swrd2lsw  14154  shftlem  14265  shftfval  14267  seqshft  14282  iserex  14851  serf0  14875  iseralt  14879  sumrblem  14905  fsumm1  14943  mptfzshft  14970  binomlem  15021  binom1dif  15025  isumsplit  15032  climcndslem1  15041  binomrisefac  15233  bpolycl  15243  bpolysum  15244  bpolydiflem  15245  bpoly2  15248  bpoly3  15249  fsumcube  15251  ruclem12  15431  dvdssub2  15488  4sqlem19  16132  vdwapun  16143  vdwapid1  16144  vdwlem5  16154  vdwlem8  16157  vdwnnlem2  16165  ramub1lem2  16196  1259lem4  16300  1259prm  16302  2503prm  16306  4001prm  16311  gsumccat  17821  sylow1lem1  18457  efgsres  18595  efgredleme  18600  gsummptshft  18780  icccvx  23241  reparphti  23288  ovolunlem1  23785  advlog  24922  cxpaddlelem  25017  ang180lem1  25072  ang180lem3  25074  asinlem2  25132  tanatan  25182  ppiub  25466  perfect1  25490  lgsquad2lem1  25646  rplogsumlem1  25746  selberg2lem  25812  logdivbnd  25818  pntrsumo1  25827  pntrsumbnd2  25829  ax5seglem3  26404  ax5seglem5  26406  axbtwnid  26412  axlowdimlem16  26430  axeuclidlem  26435  axcontlem2  26438  crctcshwlkn0lem6  27279  clwwlknonex2lem2  27573  clwwlknonex2  27574  eucrctshift  27708  cvmliftlem7  32148  nndivsub  33416  ltflcei  34432  itg2addnclem3  34497  mettrifi  34585  irrapxlem1  38925  rmspecsqrtnq  39009  jm2.24nn  39062  jm2.18  39091  jm2.23  39099  jm2.27c  39110  ablsimpgfindlem1  40186  monoord2xrv  41323  itgsinexp  41803  2elfz2melfz  43056  sbgoldbwt  43446  sgoldbeven3prm  43452  evengpop3  43467  evengpoap3  43468  zlmodzxzsub  43908