Theorem negsubd 11268

Description: Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
negsubd	⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵))

Proof of Theorem negsubd

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		negsub 11199	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   + caddc 10805   − cmin 11135  -cneg 11136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-sub 11137  df-neg 11138

This theorem is referenced by:  mulsub  11348  mulsubaddmulsub  11369  divsubdir  11599  divsubdiv  11621  ofnegsub  11901  icoshftf1o  13135  fzosubel  13374  modsub12d  13576  expaddzlem  13754  binom2sub  13863  discr  13883  cjreb  14762  recj  14763  remullem  14767  imcj  14771  sqreulem  14999  subcn2  15232  lo1sub  15268  iseraltlem2  15322  iseraltlem3  15323  fsumshftm  15421  fsumsub  15428  incexclem  15476  incexc  15477  bpoly3  15696  efmival  15790  cosadd  15802  sinsub  15805  sincossq  15813  moddvds  15902  dvdsadd2b  15943  bitsres  16108  pythagtriplem4  16448  mulgdirlem  18649  mulgmodid  18657  mulgsubdir  18658  cnsubrg  20570  zringlpirlem3  20598  cphipval  24312  pjthlem1  24506  mbfsub  24731  mbfmulc2  24732  itg2monolem1  24820  itgcnlem  24859  iblsub  24891  itgsub  24895  itgmulc2  24903  dvmptsub  25036  dvmptdiv  25043  dvexp3  25047  dvsincos  25050  dvlipcn  25063  ftc2  25113  aaliou3lem6  25413  logdiv2  25677  tanarg  25679  advlogexp  25715  cxpsub  25742  abscxpbnd  25811  relogbdiv  25834  isosctrlem2  25874  angpieqvdlem  25883  quad2  25894  dcubic1lem  25898  dcubic2  25899  dcubic  25901  mcubic  25902  dquartlem2  25907  dquart  25908  quart1lem  25910  quartlem1  25912  quart  25916  asinlem2  25924  cosasin  25959  atanlogsublem  25970  atantan  25978  atantayl2  25993  ftalem5  26131  basellem9  26143  lgseisenlem1  26428  2sqlem4  26474  rpvmasum2  26565  log2sumbnd  26597  chpdifbndlem1  26606  pntpbnd1  26639  axsegconlem9  27196  axeuclidlem  27233  smcnlem  28960  ipval2  28970  ipasslem2  29095  dipsubdir  29111  his2sub  29355  pjhthlem1  29654  circlemeth  32520  logdivsqrle  32530  fwddifnp1  34394  knoppndvlem2  34620  irrdiff  35424  itg2gt0cn  35759  iblsubnc  35765  itgsubnc  35766  itgmulc2nc  35772  ftc1anclem8  35784  ftc2nc  35786  areacirclem1  35792  dffltz  40387  3cubeslem3r  40425  mzpsubmpt  40481  pellexlem6  40572  pell1234qrreccl  40592  pellfund14  40636  rmxyneg  40658  rmxm1  40672  rmym1  40673  congsub  40708  jm2.19lem1  40727  jm2.19lem4  40730  jm2.19  40731  jm2.26lem3  40739  sqrtcval  41138  sineq0ALT  42446  sub2times  42702  fzisoeu  42729  supsubc  42782  sublimc  43083  reclimc  43084  itgsincmulx  43405  itgsbtaddcnst  43413  stoweidlem10  43441  stoweidlem13  43444  stoweidlem22  43453  stoweidlem23  43454  stoweidlem26  43457  stoweidlem42  43473  stoweidlem47  43478  stirlinglem5  43509  dirkertrigeqlem2  43530  fourierdlem26  43564  fourierdlem36  43574  fourierdlem40  43578  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem64  43601  fourierdlem78  43615  fourierdlem92  43629  fourierdlem97  43634  fourierdlem101  43638  fourierdlem107  43644  etransclem17  43682  etransclem46  43711  sigarperm  44263  quad1  44960  requad1  44962  requad2  44963  dignn0flhalflem1  45849  1subrec1sub  45939  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrx2linest2  45978  itscnhlc0yqe  45993  itschlc0yqe  45994  itsclc0yqsol  45998  itsclinecirc0b  46008  itsclquadb  46010