Theorem npcan 11475

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 11465	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
2		simpr 483	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3	1, 2	addcomd 11422	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵)))
4		pncan3 11474	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
5	4	ancoms 457	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
6	3, 5	eqtrd 2770	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  (class class class)co 7413  ℂcc 11112   + caddc 11117   − cmin 11450

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11256  df-mnf 11257  df-ltxr 11259  df-sub 11452

This theorem is referenced by:  addsubass  11476  npncan  11487  nppcan  11488  nnpcan  11489  subcan2  11491  nnncan  11501  npcand  11581  nn1suc  12240  zlem1lt  12620  zltlem1  12621  peano5uzi  12657  nummac  12728  uzp1  12869  peano2uzr  12893  qbtwnre  13184  fz01en  13535  fzsuc2  13565  fseq1m1p1  13582  predfz  13632  fzoss2  13666  fzoaddel2  13694  fzosplitsnm1  13713  fldiv  13831  modfzo0difsn  13914  seqm1  13991  monoord2  14005  sermono  14006  seqf1olem1  14013  seqf1olem2  14014  seqz  14022  expm1t  14062  expubnd  14148  bcm1k  14281  bcn2  14285  hashfzo  14395  hashbclem  14417  hashf1  14424  seqcoll  14431  swrdfv2  14617  swrdspsleq  14621  swrdlsw  14623  addlenrevpfx  14646  ccatpfx  14657  cshwlen  14755  cshwidxmodr  14760  cshwidxm  14764  swrd2lsw  14909  shftlem  15021  shftfval  15023  seqshft  15038  iserex  15609  serf0  15633  iseralt  15637  sumrblem  15663  fsumm1  15703  mptfzshft  15730  binomlem  15781  binom1dif  15785  isumsplit  15792  climcndslem1  15801  binomrisefac  15992  bpolycl  16002  bpolysum  16003  bpolydiflem  16004  bpoly2  16007  bpoly3  16008  fsumcube  16010  ruclem12  16190  dvdssub2  16250  4sqlem19  16902  vdwapun  16913  vdwapid1  16914  vdwlem5  16924  vdwlem8  16927  vdwnnlem2  16935  ramub1lem2  16966  1259lem4  17073  1259prm  17075  2503prm  17079  4001prm  17084  gsumsgrpccat  18759  sylow1lem1  19509  efgsres  19649  efgredleme  19654  gsummptshft  19847  ablsimpgfindlem1  20020  icccvx  24697  reparphti  24745  reparphtiOLD  24746  ovolunlem1  25248  advlog  26396  cxpaddlelem  26493  ang180lem1  26548  ang180lem3  26550  asinlem2  26608  tanatan  26658  ppiub  26941  perfect1  26965  lgsquad2lem1  27121  rplogsumlem1  27221  selberg2lem  27287  logdivbnd  27293  pntrsumo1  27302  pntrsumbnd2  27304  ax5seglem3  28454  ax5seglem5  28456  axbtwnid  28462  axlowdimlem16  28480  axeuclidlem  28485  axcontlem2  28488  crctcshwlkn0lem6  29334  clwwlknonex2lem2  29626  clwwlknonex2  29627  eucrctshift  29761  cvmliftlem7  34578  nndivsub  35647  ltflcei  36781  itg2addnclem3  36846  mettrifi  36930  irrapxlem1  41864  rmspecsqrtnq  41948  jm2.24nn  42002  jm2.18  42031  jm2.23  42039  jm2.27c  42050  monoord2xrv  44494  itgsinexp  44971  2elfz2melfz  46326  sbgoldbwt  46745  sgoldbeven3prm  46751  evengpop3  46766  evengpoap3  46767  zlmodzxzsub  47126  ackval42  47471