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

Theorem negsub 10673
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 10611 . . . 4 -𝐵 = (0 − 𝐵)
21oveq2i 6935 . . 3 (𝐴 + -𝐵) = (𝐴 + (0 − 𝐵))
32a1i 11 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 + (0 − 𝐵)))
4 0cn 10370 . . 3 0 ∈ ℂ
5 addsubass 10635 . . 3 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴 + (0 − 𝐵)))
64, 5mp3an2 1522 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴 + (0 − 𝐵)))
7 simpl 476 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
87addid1d 10578 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 0) = 𝐴)
98oveq1d 6939 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴𝐵))
103, 6, 93eqtr2d 2820 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2107  (class class class)co 6924  cc 10272  0cc0 10274   + caddc 10277  cmin 10608  -cneg 10609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-po 5276  df-so 5277  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-pnf 10415  df-mnf 10416  df-ltxr 10418  df-sub 10610  df-neg 10611
This theorem is referenced by:  negdi2  10683  negsubdi2  10684  resubcli  10687  resubcl  10689  negsubi  10703  negsubd  10742  submul2  10817  addneg1mul  10819  mulsub  10820  divsubdir  11071  difgtsumgt  11701  elz2  11749  zsubcl  11775  qsubcl  12119  rexsub  12380  fzsubel  12698  ceim1l  12969  modcyc2  13029  negmod  13038  modsumfzodifsn  13066  expsub  13230  binom2sub  13304  seqshft  14236  resub  14278  imsub  14286  cjsub  14300  cjreim  14311  absdiflt  14468  absdifle  14469  abs2dif2  14484  subcn2  14737  bpoly2  15194  bpoly3  15195  efsub  15236  efi4p  15273  sinsub  15304  cossub  15305  demoivreALT  15337  dvdssub  15437  modgcd  15663  gzsubcl  16052  psgnunilem2  18303  cnfldsub  20174  itg1sub  23917  plyremlem  24500  sineq0  24715  logneg2  24802  ang180lem2  24992  asinsin  25074  atanneg  25089  atancj  25092  atanlogadd  25096  atanlogsublem  25097  atanlogsub  25098  2efiatan  25100  tanatan  25101  cosatan  25103  atans2  25113  dvatan  25117  zetacvg  25197  wilthlem1  25250  wilthlem2  25251  basellem8  25270  lgsvalmod  25497  cnnvm  28113  cncph  28250  hvsubdistr2  28483  lnfnsubi  29481  subfacval2  31772  itg2addnclem3  34093  pellexlem6  38368  pell14qrdich  38403  rmxm1  38468  rmym1  38469  addsubeq0  42348  omoeALTV  42631  omeoALTV  42632  emoo  42648  emee  42650  zlmodzxzequap  43313  flsubz  43337
  Copyright terms: Public domain W3C validator