Theorem negsubd 11539

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071   − cmin 11405  -cneg 11406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407  df-neg 11408

This theorem is referenced by:  mulsub  11621  mulsubaddmulsub  11642  divsubdir  11876  divsubdiv  11898  ofnegsub  12184  icoshftf1o  13435  fzosubel  13685  modaddb  13871  modsub12d  13893  expaddzlem  14070  binom2sub  14185  discr  14205  cjreb  15089  recj  15090  remullem  15094  imcj  15098  sqreulem  15326  subcn2  15561  lo1sub  15597  iseraltlem2  15649  iseraltlem3  15650  fsumshftm  15747  fsumsub  15754  incexclem  15802  incexc  15803  bpoly3  16024  efmival  16121  cosadd  16133  sinsub  16136  sincossq  16144  moddvds  16233  dvdsadd2b  16276  bitsres  16443  pythagtriplem4  16790  mulgdirlem  19037  mulgmodid  19045  mulgsubdir  19046  cnsubrg  21344  zringlpirlem3  21374  cphipval  25143  pjthlem1  25337  mbfsub  25563  mbfmulc2  25564  itg2monolem1  25651  itgcnlem  25691  iblsub  25723  itgsub  25727  itgmulc2  25735  dvmptsub  25871  dvmptdiv  25878  dvexp3  25882  dvsincos  25885  dvlipcn  25899  ftc2  25951  aaliou3lem6  26256  logdiv2  26526  tanarg  26528  advlogexp  26564  cxpsub  26591  abscxpbnd  26663  relogbdiv  26689  isosctrlem2  26729  angpieqvdlem  26738  quad2  26749  dcubic1lem  26753  dcubic2  26754  dcubic  26756  mcubic  26757  dquartlem2  26762  dquart  26763  quart1lem  26765  quartlem1  26767  quart  26771  asinlem2  26779  cosasin  26814  atanlogsublem  26825  atantan  26833  atantayl2  26848  ftalem5  26987  basellem9  26999  lgseisenlem1  27286  2sqlem4  27332  rpvmasum2  27423  log2sumbnd  27455  chpdifbndlem1  27464  pntpbnd1  27497  axsegconlem9  28852  axeuclidlem  28889  smcnlem  30626  ipval2  30636  ipasslem2  30761  dipsubdir  30777  his2sub  31021  pjhthlem1  31320  quad3d  32673  constrrtlc1  33722  constrrtcc  33725  constrremulcl  33757  constrimcl  33760  constrreinvcl  33762  constrresqrtcl  33767  2sqr3minply  33770  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  circlemeth  34631  logdivsqrle  34641  fwddifnp1  36153  knoppndvlem2  36501  irrdiff  37314  itg2gt0cn  37669  iblsubnc  37675  itgsubnc  37676  itgmulc2nc  37682  ftc1anclem8  37694  ftc2nc  37696  areacirclem1  37702  primrootscoprbij  42090  bcle2d  42167  aks6d1c7lem1  42168  dffltz  42622  3cubeslem3r  42675  mzpsubmpt  42731  pellexlem6  42822  pell1234qrreccl  42842  pellfund14  42886  rmxyneg  42909  rmxm1  42923  rmym1  42924  congsub  42959  jm2.19lem1  42978  jm2.19lem4  42981  jm2.19  42982  jm2.26lem3  42990  sqrtcval  43630  sineq0ALT  44926  sub2times  45271  fzisoeu  45298  supsubc  45349  sublimc  45650  reclimc  45651  itgsincmulx  45972  itgsbtaddcnst  45980  stoweidlem10  46008  stoweidlem13  46011  stoweidlem22  46020  stoweidlem23  46021  stoweidlem26  46024  stoweidlem42  46040  stoweidlem47  46045  stirlinglem5  46076  dirkertrigeqlem2  46097  fourierdlem26  46131  fourierdlem36  46141  fourierdlem40  46145  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem64  46168  fourierdlem78  46182  fourierdlem92  46196  fourierdlem97  46201  fourierdlem101  46205  fourierdlem107  46211  etransclem17  46249  etransclem46  46278  sigarperm  46858  modm2nep1  47367  modm1nep2  47369  modm1nem2  47370  quad1  47621  requad1  47623  requad2  47624  dignn0flhalflem1  48604  1subrec1sub  48694  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2linest2  48733  itscnhlc0yqe  48748  itschlc0yqe  48749  itsclc0yqsol  48753  itsclinecirc0b  48763  itsclquadb  48765