Theorem npcan 11467

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 11457	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
2		simpr 489	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3	1, 2	addcomd 11413	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵)))
4		pncan3 11466	. . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
5	4	ancoms 463	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴)
6	3, 5	eqtrd 2798	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   + caddc 11104   − cmin 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11444

This theorem is referenced by:  addsubass  11468  npncan  11480  nppcan  11481  nnpcan  11482  subcan2  11484  nnncan  11494  npcand  11574  nn1suc  12256  zlem1lt  12647  zltlem1  12648  peano5uzi  12686  nummac  12762  uzp1  12900  peano2uzr  12928  qbtwnre  13226  fz01en  13582  fzsuc2  13612  fseq1m1p1  13629  predfz  13683  fzoss2  13718  fzoaddel2  13751  fzosplitsnm1  13771  fldiv  13895  modfzo0difsn  13981  seqm1  14057  monoord2  14071  sermono  14072  seqf1olem1  14079  seqf1olem2  14080  seqz  14088  expm1t  14128  expubnd  14216  bcm1k  14353  bcn2  14357  hashfzo  14468  hashbclem  14491  hashf1  14496  seqcoll  14503  swrdfv2  14701  swrdspsleq  14705  swrdlsw  14707  ccatpfx  14740  cshwlen  14838  cshwidxmodr  14843  cshwidxm  14847  swrd2lsw  14991  shftlem  15107  shftfval  15109  seqshft  15124  iserex  15710  serf0  15734  iseralt  15738  sumrblem  15764  fsumm1  15804  mptfzshft  15831  binomlem  15885  binom1dif  15889  isumsplit  15896  climcndslem1  15905  binomrisefac  16097  bpolycl  16107  bpolysum  16108  bpolydiflem  16109  bpoly2  16112  bpoly3  16113  fsumcube  16115  ruclem12  16298  dvdssub2  16360  4sqlem19  17024  vdwapun  17035  vdwapid1  17036  vdwlem5  17046  vdwlem8  17049  vdwnnlem2  17057  ramub1lem2  17088  1259lem4  17195  1259prm  17197  2503prm  17201  4001prm  17206  gsumsgrpccat  18900  sylow1lem1  19669  efgsres  19809  efgredleme  19814  gsummptshft  20007  ablsimpgfindlem1  20180  icccvx  25090  reparphti  25137  ovolunlem1  25637  advlog  26797  cxpaddlelem  26894  ang180lem1  26952  ang180lem3  26954  asinlem2  27012  tanatan  27062  ppiub  27346  perfect1  27370  lgsquad2lem1  27526  rplogsumlem1  27626  selberg2lem  27692  logdivbnd  27698  pntrsumo1  27707  pntrsumbnd2  27709  ax5seglem3  29259  ax5seglem5  29261  axbtwnid  29267  axlowdimlem16  29285  axeuclidlem  29290  axcontlem2  29293  crctcshwlkn0lem6  30142  clwwlknonex2lem2  30437  clwwlknonex2  30438  eucrctshift  30572  cvmliftlem7  35761  nndivsub  36946  ltflcei  38237  itg2addnclem3  38302  mettrifi  38386  irrapxlem1  43529  rmspecsqrtnq  43613  jm2.24nn  43666  jm2.18  43695  jm2.23  43703  jm2.27c  43714  monoord2xrv  46177  itgsinexp  46649  2elfz2melfz  48032  sbgoldbwt  48519  sgoldbeven3prm  48525  evengpop3  48540  evengpoap3  48541  gpg5nbgrvtx13starlem2  48814  zlmodzxzsub  49117  ackval42  49453