Theorem negsubd 11473

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7341  ℂcc 10999   + caddc 11004   − cmin 11339  -cneg 11340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-po 5519  df-so 5520  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-ltxr 11146  df-sub 11341  df-neg 11342

This theorem is referenced by:  mulsub  11555  mulsubaddmulsub  11576  divsubdir  11810  divsubdiv  11832  ofnegsub  12118  icoshftf1o  13369  fzosubel  13619  modaddb  13808  modsub12d  13830  expaddzlem  14007  binom2sub  14122  discr  14142  cjreb  15025  recj  15026  remullem  15030  imcj  15034  sqreulem  15262  subcn2  15497  lo1sub  15533  iseraltlem2  15585  iseraltlem3  15586  fsumshftm  15683  fsumsub  15690  incexclem  15738  incexc  15739  bpoly3  15960  efmival  16057  cosadd  16069  sinsub  16072  sincossq  16080  moddvds  16169  dvdsadd2b  16212  bitsres  16379  pythagtriplem4  16726  mulgdirlem  19013  mulgmodid  19021  mulgsubdir  19022  cnsubrg  21359  zringlpirlem3  21396  cphipval  25165  pjthlem1  25359  mbfsub  25585  mbfmulc2  25586  itg2monolem1  25673  itgcnlem  25713  iblsub  25745  itgsub  25749  itgmulc2  25757  dvmptsub  25893  dvmptdiv  25900  dvexp3  25904  dvsincos  25907  dvlipcn  25921  ftc2  25973  aaliou3lem6  26278  logdiv2  26548  tanarg  26550  advlogexp  26586  cxpsub  26613  abscxpbnd  26685  relogbdiv  26711  isosctrlem2  26751  angpieqvdlem  26760  quad2  26771  dcubic1lem  26775  dcubic2  26776  dcubic  26778  mcubic  26779  dquartlem2  26784  dquart  26785  quart1lem  26787  quartlem1  26789  quart  26793  asinlem2  26801  cosasin  26836  atanlogsublem  26847  atantan  26855  atantayl2  26870  ftalem5  27009  basellem9  27021  lgseisenlem1  27308  2sqlem4  27354  rpvmasum2  27445  log2sumbnd  27477  chpdifbndlem1  27486  pntpbnd1  27519  axsegconlem9  28898  axeuclidlem  28935  smcnlem  30669  ipval2  30679  ipasslem2  30804  dipsubdir  30820  his2sub  31064  pjhthlem1  31363  quad3d  32725  constrrtlc1  33737  constrrtcc  33740  constrremulcl  33772  constrimcl  33775  constrreinvcl  33777  constrresqrtcl  33782  2sqr3minply  33785  cos9thpiminplylem1  33787  cos9thpiminplylem2  33788  circlemeth  34645  logdivsqrle  34655  fwddifnp1  36199  knoppndvlem2  36547  irrdiff  37360  itg2gt0cn  37715  iblsubnc  37721  itgsubnc  37722  itgmulc2nc  37728  ftc1anclem8  37740  ftc2nc  37742  areacirclem1  37748  primrootscoprbij  42135  bcle2d  42212  aks6d1c7lem1  42213  dffltz  42667  3cubeslem3r  42720  mzpsubmpt  42776  pellexlem6  42867  pell1234qrreccl  42887  pellfund14  42931  rmxyneg  42953  rmxm1  42967  rmym1  42968  congsub  43003  jm2.19lem1  43022  jm2.19lem4  43025  jm2.19  43026  jm2.26lem3  43034  sqrtcval  43674  sineq0ALT  44969  sub2times  45314  fzisoeu  45341  supsubc  45392  sublimc  45690  reclimc  45691  itgsincmulx  46012  itgsbtaddcnst  46020  stoweidlem10  46048  stoweidlem13  46051  stoweidlem22  46060  stoweidlem23  46061  stoweidlem26  46064  stoweidlem42  46080  stoweidlem47  46085  stirlinglem5  46116  dirkertrigeqlem2  46137  fourierdlem26  46171  fourierdlem36  46181  fourierdlem40  46185  fourierdlem41  46186  fourierdlem48  46192  fourierdlem49  46193  fourierdlem64  46208  fourierdlem78  46222  fourierdlem92  46236  fourierdlem97  46241  fourierdlem101  46245  fourierdlem107  46251  etransclem17  46289  etransclem46  46318  sigarperm  46898  modm2nep1  47397  modm1nep2  47399  modm1nem2  47400  quad1  47651  requad1  47653  requad2  47654  dignn0flhalflem1  48647  1subrec1sub  48737  eenglngeehlnmlem1  48769  eenglngeehlnmlem2  48770  rrx2linest2  48776  itscnhlc0yqe  48791  itschlc0yqe  48792  itsclc0yqsol  48796  itsclinecirc0b  48806  itsclquadb  48808