Theorem negsubd 11616

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7414  ℂcc 11145   + caddc 11150   − cmin 11483  -cneg 11484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7736  ax-resscn 11204  ax-1cn 11205  ax-icn 11206  ax-addcl 11207  ax-addrcl 11208  ax-mulcl 11209  ax-mulrcl 11210  ax-mulcom 11211  ax-addass 11212  ax-mulass 11213  ax-distr 11214  ax-i2m1 11215  ax-1ne0 11216  ax-1rid 11217  ax-rnegex 11218  ax-rrecex 11219  ax-cnre 11220  ax-pre-lttri 11221  ax-pre-lttrn 11222  ax-pre-ltadd 11223

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3366  df-rab 3421  df-v 3465  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-br 5145  df-opab 5207  df-mpt 5228  df-id 5571  df-po 5585  df-so 5586  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11289  df-mnf 11290  df-ltxr 11292  df-sub 11485  df-neg 11486

This theorem is referenced by:  mulsub  11696  mulsubaddmulsub  11717  divsubdir  11951  divsubdiv  11973  ofnegsub  12254  icoshftf1o  13497  fzosubel  13737  modsub12d  13940  expaddzlem  14117  binom2sub  14230  discr  14250  cjreb  15121  recj  15122  remullem  15126  imcj  15130  sqreulem  15357  subcn2  15590  lo1sub  15626  iseraltlem2  15680  iseraltlem3  15681  fsumshftm  15778  fsumsub  15785  incexclem  15833  incexc  15834  bpoly3  16053  efmival  16148  cosadd  16160  sinsub  16163  sincossq  16171  moddvds  16260  dvdsadd2b  16301  bitsres  16466  pythagtriplem4  16814  mulgdirlem  19093  mulgmodid  19101  mulgsubdir  19102  cnsubrg  21418  zringlpirlem3  21448  cphipval  25257  pjthlem1  25451  mbfsub  25677  mbfmulc2  25678  itg2monolem1  25766  itgcnlem  25805  iblsub  25837  itgsub  25841  itgmulc2  25849  dvmptsub  25985  dvmptdiv  25992  dvexp3  25996  dvsincos  25999  dvlipcn  26013  ftc2  26065  aaliou3lem6  26371  logdiv2  26639  tanarg  26641  advlogexp  26677  cxpsub  26704  abscxpbnd  26776  relogbdiv  26802  isosctrlem2  26842  angpieqvdlem  26851  quad2  26862  dcubic1lem  26866  dcubic2  26867  dcubic  26869  mcubic  26870  dquartlem2  26875  dquart  26876  quart1lem  26878  quartlem1  26880  quart  26884  asinlem2  26892  cosasin  26927  atanlogsublem  26938  atantan  26946  atantayl2  26961  ftalem5  27100  basellem9  27112  lgseisenlem1  27399  2sqlem4  27445  rpvmasum2  27536  log2sumbnd  27568  chpdifbndlem1  27577  pntpbnd1  27610  axsegconlem9  28854  axeuclidlem  28891  smcnlem  30625  ipval2  30635  ipasslem2  30760  dipsubdir  30776  his2sub  31020  pjhthlem1  31319  quad3d  32655  constrrtlc1  33603  constrrtcc  33606  2sqr3minply  33618  circlemeth  34497  logdivsqrle  34507  fwddifnp1  36000  knoppndvlem2  36227  irrdiff  37044  itg2gt0cn  37387  iblsubnc  37393  itgsubnc  37394  itgmulc2nc  37400  ftc1anclem8  37412  ftc2nc  37414  areacirclem1  37420  primrootscoprbij  41812  bcle2d  41889  aks6d1c7lem1  41890  dffltz  42322  3cubeslem3r  42379  mzpsubmpt  42435  pellexlem6  42526  pell1234qrreccl  42546  pellfund14  42590  rmxyneg  42613  rmxm1  42627  rmym1  42628  congsub  42663  jm2.19lem1  42682  jm2.19lem4  42685  jm2.19  42686  jm2.26lem3  42694  sqrtcval  43343  sineq0ALT  44648  sub2times  44921  fzisoeu  44949  supsubc  45002  sublimc  45307  reclimc  45308  itgsincmulx  45629  itgsbtaddcnst  45637  stoweidlem10  45665  stoweidlem13  45668  stoweidlem22  45677  stoweidlem23  45678  stoweidlem26  45681  stoweidlem42  45697  stoweidlem47  45702  stirlinglem5  45733  dirkertrigeqlem2  45754  fourierdlem26  45788  fourierdlem36  45798  fourierdlem40  45802  fourierdlem41  45803  fourierdlem48  45809  fourierdlem49  45810  fourierdlem64  45825  fourierdlem78  45839  fourierdlem92  45853  fourierdlem97  45858  fourierdlem101  45862  fourierdlem107  45868  etransclem17  45906  etransclem46  45935  sigarperm  46515  quad1  47226  requad1  47228  requad2  47229  dignn0flhalflem1  48037  1subrec1sub  48127  eenglngeehlnmlem1  48159  eenglngeehlnmlem2  48160  rrx2linest2  48166  itscnhlc0yqe  48181  itschlc0yqe  48182  itsclc0yqsol  48186  itsclinecirc0b  48196  itsclquadb  48198