Theorem negsubd 11510

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 11441	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041   − cmin 11376  -cneg 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378  df-neg 11379

This theorem is referenced by:  mulsub  11592  mulsubaddmulsub  11613  divsubdir  11847  divsubdiv  11869  ofnegsub  12155  icoshftf1o  13402  fzosubel  13652  modaddb  13841  modsub12d  13863  expaddzlem  14040  binom2sub  14155  discr  14175  cjreb  15058  recj  15059  remullem  15063  imcj  15067  sqreulem  15295  subcn2  15530  lo1sub  15566  iseraltlem2  15618  iseraltlem3  15619  fsumshftm  15716  fsumsub  15723  incexclem  15771  incexc  15772  bpoly3  15993  efmival  16090  cosadd  16102  sinsub  16105  sincossq  16113  moddvds  16202  dvdsadd2b  16245  bitsres  16412  pythagtriplem4  16759  mulgdirlem  19047  mulgmodid  19055  mulgsubdir  19056  cnsubrg  21394  zringlpirlem3  21431  cphipval  25211  pjthlem1  25405  mbfsub  25631  mbfmulc2  25632  itg2monolem1  25719  itgcnlem  25759  iblsub  25791  itgsub  25795  itgmulc2  25803  dvmptsub  25939  dvmptdiv  25946  dvexp3  25950  dvsincos  25953  dvlipcn  25967  ftc2  26019  aaliou3lem6  26324  logdiv2  26594  tanarg  26596  advlogexp  26632  cxpsub  26659  abscxpbnd  26731  relogbdiv  26757  isosctrlem2  26797  angpieqvdlem  26806  quad2  26817  dcubic1lem  26821  dcubic2  26822  dcubic  26824  mcubic  26825  dquartlem2  26830  dquart  26831  quart1lem  26833  quartlem1  26835  quart  26839  asinlem2  26847  cosasin  26882  atanlogsublem  26893  atantan  26901  atantayl2  26916  ftalem5  27055  basellem9  27067  lgseisenlem1  27354  2sqlem4  27400  rpvmasum2  27491  log2sumbnd  27523  chpdifbndlem1  27532  pntpbnd1  27565  axsegconlem9  29010  axeuclidlem  29047  smcnlem  30785  ipval2  30795  ipasslem2  30920  dipsubdir  30936  his2sub  31180  pjhthlem1  31479  quad3d  32840  constrrtlc1  33910  constrrtcc  33913  constrremulcl  33945  constrimcl  33948  constrreinvcl  33950  constrresqrtcl  33955  2sqr3minply  33958  cos9thpiminplylem1  33960  cos9thpiminplylem2  33961  circlemeth  34818  logdivsqrle  34828  fwddifnp1  36381  knoppndvlem2  36735  irrdiff  37581  itg2gt0cn  37926  iblsubnc  37932  itgsubnc  37933  itgmulc2nc  37939  ftc1anclem8  37951  ftc2nc  37953  areacirclem1  37959  primrootscoprbij  42472  bcle2d  42549  aks6d1c7lem1  42550  dffltz  42992  3cubeslem3r  43044  mzpsubmpt  43100  pellexlem6  43191  pell1234qrreccl  43211  pellfund14  43255  rmxyneg  43277  rmxm1  43291  rmym1  43292  congsub  43327  jm2.19lem1  43346  jm2.19lem4  43349  jm2.19  43350  jm2.26lem3  43358  sqrtcval  43997  sineq0ALT  45292  sub2times  45635  fzisoeu  45662  supsubc  45712  sublimc  46010  reclimc  46011  itgsincmulx  46332  itgsbtaddcnst  46340  stoweidlem10  46368  stoweidlem13  46371  stoweidlem22  46380  stoweidlem23  46381  stoweidlem26  46384  stoweidlem42  46400  stoweidlem47  46405  stirlinglem5  46436  dirkertrigeqlem2  46457  fourierdlem26  46491  fourierdlem36  46501  fourierdlem40  46505  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem64  46528  fourierdlem78  46542  fourierdlem92  46556  fourierdlem97  46561  fourierdlem101  46565  fourierdlem107  46571  etransclem17  46609  etransclem46  46638  sigarperm  47218  modm2nep1  47726  modm1nep2  47728  modm1nem2  47729  quad1  47980  requad1  47982  requad2  47983  dignn0flhalflem1  48975  1subrec1sub  49065  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098  rrx2linest2  49104  itscnhlc0yqe  49119  itschlc0yqe  49120  itsclc0yqsol  49124  itsclinecirc0b  49134  itsclquadb  49136