Theorem negsubd 11570

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   + caddc 11098   − cmin 11436  -cneg 11437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-ltxr 11243  df-sub 11438  df-neg 11439

This theorem is referenced by:  mulsub  11652  mulsubaddmulsub  11673  divsubdir  11903  divsubdiv  11926  ofnegsub  12211  icoshftf1o  13496  fzosubel  13749  modaddb  13938  modsub12d  13960  expaddzlem  14137  binom2sub  14252  discr  14272  cjreb  15170  recj  15171  remullem  15175  imcj  15179  sqreulem  15407  subcn2  15642  lo1sub  15678  iseraltlem2  15730  iseraltlem3  15731  fsumshftm  15828  fsumsub  15835  incexclem  15886  incexc  15887  bpoly3  16107  efmival  16204  cosadd  16216  sinsub  16219  sincossq  16227  moddvds  16316  dvdsadd2b  16359  bitsres  16526  pythagtriplem4  16874  mulgdirlem  19166  mulgmodid  19174  mulgsubdir  19175  cnsubrg  21577  zringlpirlem3  21614  cphipval  25402  pjthlem1  25596  mbfsub  25821  mbfmulc2  25822  itg2monolem1  25909  itgcnlem  25949  iblsub  25981  itgsub  25985  itgmulc2  25993  dvmptsub  26126  dvmptdiv  26133  dvexp3  26137  dvsincos  26140  dvlipcn  26153  ftc2  26203  aaliou3lem6  26511  logdiv2  26782  tanarg  26784  advlogexp  26820  cxpsub  26847  abscxpbnd  26918  relogbdiv  26944  isosctrlem2  26984  angpieqvdlem  26993  quad2  27004  dcubic1lem  27008  dcubic2  27009  dcubic  27011  mcubic  27012  dquartlem2  27017  dquart  27018  quart1lem  27020  quartlem1  27022  quart  27026  asinlem2  27034  cosasin  27069  atanlogsublem  27080  atantan  27088  atantayl2  27103  ftalem5  27241  basellem9  27253  lgseisenlem1  27539  2sqlem4  27585  rpvmasum2  27676  log2sumbnd  27708  chpdifbndlem1  27717  pntpbnd1  27750  axsegconlem9  29275  axeuclidlem  29312  smcnlem  31049  ipval2  31059  ipasslem2  31184  dipsubdir  31200  his2sub  31444  pjhthlem1  31743  quad3d  33094  constrrtlc1  34122  constrrtcc  34125  constrremulcl  34157  constrimcl  34160  constrreinvcl  34162  constrresqrtcl  34167  2sqr3minply  34170  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  circlemeth  35027  logdivsqrle  35037  fwddifnp1  36657  knoppndvlem2  37102  irrdiff  37970  itg2gt0cn  38326  iblsubnc  38332  itgsubnc  38333  itgmulc2nc  38339  ftc1anclem8  38351  ftc2nc  38353  areacirclem1  38359  primrootscoprbij  42869  bcle2d  42946  aks6d1c7lem1  42947  dffltz  43366  3cubeslem3r  43418  mzpsubmpt  43474  pellexlem6  43561  pell1234qrreccl  43581  pellfund14  43625  rmxyneg  43647  rmxm1  43661  rmym1  43662  congsub  43697  jm2.19lem1  43716  jm2.19lem4  43719  jm2.19  43720  jm2.26lem3  43728  sqrtcval  44367  sineq0ALT  45645  sub2times  45992  fzisoeu  46019  supsubc  46069  sublimc  46366  reclimc  46367  itgsincmulx  46688  itgsbtaddcnst  46696  stoweidlem10  46724  stoweidlem13  46727  stoweidlem22  46736  stoweidlem23  46737  stoweidlem26  46740  stoweidlem42  46756  stoweidlem47  46761  stirlinglem5  46792  dirkertrigeqlem2  46813  fourierdlem26  46847  fourierdlem36  46857  fourierdlem40  46861  fourierdlem41  46862  fourierdlem48  46868  fourierdlem49  46869  fourierdlem64  46884  fourierdlem78  46898  fourierdlem92  46912  fourierdlem97  46917  fourierdlem101  46921  fourierdlem107  46927  etransclem17  46965  etransclem46  46994  sigarperm  47574  modm2nep1  48109  modm1nep2  48111  modm1nem2  48112  quad1  48385  requad1  48387  requad2  48388  dignn0flhalflem1  49395  1subrec1sub  49485  eenglngeehlnmlem1  49517  eenglngeehlnmlem2  49518  rrx2linest2  49524  itscnhlc0yqe  49539  itschlc0yqe  49540  itsclc0yqsol  49544  itsclinecirc0b  49554  itsclquadb  49556