MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  negsub Structured version   Visualization version   GIF version

Theorem negsub 10177
Description: Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
negsub ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴𝐵))

Proof of Theorem negsub
StepHypRef Expression
1 df-neg 10117 . . . 4 -𝐵 = (0 − 𝐵)
21oveq2i 6535 . . 3 (𝐴 + -𝐵) = (𝐴 + (0 − 𝐵))
32a1i 11 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 + (0 − 𝐵)))
4 0cn 9885 . . 3 0 ∈ ℂ
5 addsubass 10139 . . 3 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴 + (0 − 𝐵)))
64, 5mp3an2 1403 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴 + (0 − 𝐵)))
7 simpl 471 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
87addid1d 10084 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 0) = 𝐴)
98oveq1d 6539 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴𝐵))
103, 6, 93eqtr2d 2646 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  (class class class)co 6524  cc 9787  0cc0 9789   + caddc 9792  cmin 10114  -cneg 10115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-po 4946  df-so 4947  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-er 7603  df-en 7816  df-dom 7817  df-sdom 7818  df-pnf 9929  df-mnf 9930  df-ltxr 9932  df-sub 10116  df-neg 10117
This theorem is referenced by:  negdi2  10187  negsubdi2  10188  resubcli  10191  resubcl  10193  negsubi  10207  negsubd  10246  submul2  10318  mulsub  10320  divsubdir  10567  difgtsumgt  11190  elz2  11224  zsubcl  11249  qsubcl  11636  rexsub  11894  fzsubel  12200  ceim1l  12460  modcyc2  12520  negmod  12529  modsumfzodifsn  12557  expsub  12722  binom2sub  12795  seqshft  13616  resub  13658  imsub  13666  cjsub  13680  cjreim  13691  absdiflt  13848  absdifle  13849  abs2dif2  13864  subcn2  14116  bpoly2  14570  bpoly3  14571  efsub  14612  efi4p  14649  sinsub  14680  cossub  14681  demoivreALT  14713  dvdssub  14807  modgcd  15034  gzsubcl  15425  psgnunilem2  17681  cnfldsub  19536  itg1sub  23196  plyremlem  23777  sineq0  23991  logneg2  24079  ang180lem2  24254  asinsin  24333  atanneg  24348  atancj  24351  atanlogadd  24355  atanlogsublem  24356  atanlogsub  24357  2efiatan  24359  tanatan  24360  cosatan  24362  atans2  24372  dvatan  24376  zetacvg  24455  wilthlem1  24508  wilthlem2  24509  basellem8  24528  lgsvalmod  24755  vcsubdirOLD  26574  cnnvm  26715  cncph  26861  hvsubdistr2  27094  lnfnsubi  28092  subfacval2  30226  itg2addnclem3  32433  pellexlem6  36216  pell14qrdich  36251  rmxm1  36317  rmym1  36318  omoeALTV  39936  omeoALTV  39937  emoo  39953  emee  39955  zlmodzxzequap  42081  flsubz  42105
  Copyright terms: Public domain W3C validator