Theorem negsubd 11489

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11015   + caddc 11020   − cmin 11355  -cneg 11356

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-ltxr 11162  df-sub 11357  df-neg 11358

This theorem is referenced by:  mulsub  11571  mulsubaddmulsub  11592  divsubdir  11826  divsubdiv  11848  ofnegsub  12134  icoshftf1o  13381  fzosubel  13631  modaddb  13820  modsub12d  13842  expaddzlem  14019  binom2sub  14134  discr  14154  cjreb  15037  recj  15038  remullem  15042  imcj  15046  sqreulem  15274  subcn2  15509  lo1sub  15545  iseraltlem2  15597  iseraltlem3  15598  fsumshftm  15695  fsumsub  15702  incexclem  15750  incexc  15751  bpoly3  15972  efmival  16069  cosadd  16081  sinsub  16084  sincossq  16092  moddvds  16181  dvdsadd2b  16224  bitsres  16391  pythagtriplem4  16738  mulgdirlem  19026  mulgmodid  19034  mulgsubdir  19035  cnsubrg  21373  zringlpirlem3  21410  cphipval  25190  pjthlem1  25384  mbfsub  25610  mbfmulc2  25611  itg2monolem1  25698  itgcnlem  25738  iblsub  25770  itgsub  25774  itgmulc2  25782  dvmptsub  25918  dvmptdiv  25925  dvexp3  25929  dvsincos  25932  dvlipcn  25946  ftc2  25998  aaliou3lem6  26303  logdiv2  26573  tanarg  26575  advlogexp  26611  cxpsub  26638  abscxpbnd  26710  relogbdiv  26736  isosctrlem2  26776  angpieqvdlem  26785  quad2  26796  dcubic1lem  26800  dcubic2  26801  dcubic  26803  mcubic  26804  dquartlem2  26809  dquart  26810  quart1lem  26812  quartlem1  26814  quart  26818  asinlem2  26826  cosasin  26861  atanlogsublem  26872  atantan  26880  atantayl2  26895  ftalem5  27034  basellem9  27046  lgseisenlem1  27333  2sqlem4  27379  rpvmasum2  27470  log2sumbnd  27502  chpdifbndlem1  27511  pntpbnd1  27544  axsegconlem9  28924  axeuclidlem  28961  smcnlem  30698  ipval2  30708  ipasslem2  30833  dipsubdir  30849  his2sub  31093  pjhthlem1  31392  quad3d  32757  constrrtlc1  33817  constrrtcc  33820  constrremulcl  33852  constrimcl  33855  constrreinvcl  33857  constrresqrtcl  33862  2sqr3minply  33865  cos9thpiminplylem1  33867  cos9thpiminplylem2  33868  circlemeth  34725  logdivsqrle  34735  fwddifnp1  36281  knoppndvlem2  36629  irrdiff  37443  itg2gt0cn  37788  iblsubnc  37794  itgsubnc  37795  itgmulc2nc  37801  ftc1anclem8  37813  ftc2nc  37815  areacirclem1  37821  primrootscoprbij  42268  bcle2d  42345  aks6d1c7lem1  42346  dffltz  42792  3cubeslem3r  42844  mzpsubmpt  42900  pellexlem6  42991  pell1234qrreccl  43011  pellfund14  43055  rmxyneg  43077  rmxm1  43091  rmym1  43092  congsub  43127  jm2.19lem1  43146  jm2.19lem4  43149  jm2.19  43150  jm2.26lem3  43158  sqrtcval  43798  sineq0ALT  45093  sub2times  45437  fzisoeu  45464  supsubc  45514  sublimc  45812  reclimc  45813  itgsincmulx  46134  itgsbtaddcnst  46142  stoweidlem10  46170  stoweidlem13  46173  stoweidlem22  46182  stoweidlem23  46183  stoweidlem26  46186  stoweidlem42  46202  stoweidlem47  46207  stirlinglem5  46238  dirkertrigeqlem2  46259  fourierdlem26  46293  fourierdlem36  46303  fourierdlem40  46307  fourierdlem41  46308  fourierdlem48  46314  fourierdlem49  46315  fourierdlem64  46330  fourierdlem78  46344  fourierdlem92  46358  fourierdlem97  46363  fourierdlem101  46367  fourierdlem107  46373  etransclem17  46411  etransclem46  46440  sigarperm  47020  modm2nep1  47528  modm1nep2  47530  modm1nem2  47531  quad1  47782  requad1  47784  requad2  47785  dignn0flhalflem1  48777  1subrec1sub  48867  eenglngeehlnmlem1  48899  eenglngeehlnmlem2  48900  rrx2linest2  48906  itscnhlc0yqe  48921  itschlc0yqe  48922  itsclc0yqsol  48926  itsclinecirc0b  48936  itsclquadb  48938