Theorem negsubd 11590

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7419  ℂcc 11113   + caddc 11118   − cmin 11456  -cneg 11457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-ltxr 11263  df-sub 11458  df-neg 11459

This theorem is used by:  mulsub  11672  mulsubaddmulsub  11693  divsubdir  11923  divsubdiv  11946  ofnegsub  12231  icoshftf1o  13517  fzosubel  13770  modaddb  13960  modsub12d  13982  expaddzlem  14159  binom2sub  14274  discr  14294  cjreb  15198  recj  15199  remullem  15203  imcj  15207  sqreulem  15435  subcn2  15670  lo1sub  15706  iseraltlem2  15758  iseraltlem3  15759  fsumshftm  15855  fsumsub  15862  incexclem  15913  incexc  15914  bpoly3  16134  efmival  16231  cosadd  16243  sinsub  16246  sincossq  16254  moddvds  16343  dvdsadd2b  16386  bitsres  16553  pythagtriplem4  16901  mulgdirlem  19215  mulgmodid  19223  mulgsubdir  19224  cnsubrg  21627  zringlpirlem3  21664  cphipval  25453  pjthlem1  25647  mbfsub  25872  mbfmulc2  25873  itg2monolem1  25960  itgcnlem  26000  iblsub  26032  itgsub  26036  itgmulc2  26044  dvmptsub  26177  dvmptdiv  26184  dvexp3  26188  dvsincos  26191  dvlipcn  26204  ftc2  26254  aaliou3lem6  26562  logdiv2  26833  tanarg  26835  advlogexp  26871  cxpsub  26898  abscxpbnd  26969  relogbdiv  26995  isosctrlem2  27035  angpieqvdlem  27044  quad2  27055  dcubic1lem  27059  dcubic2  27060  dcubic  27062  mcubic  27063  dquartlem2  27068  dquart  27069  quart1lem  27071  quartlem1  27073  quart  27077  asinlem2  27085  cosasin  27120  atanlogsublem  27131  atantan  27139  atantayl2  27154  ftalem5  27292  basellem9  27304  lgseisenlem1  27590  2sqlem4  27636  rpvmasum2  27727  log2sumbnd  27759  chpdifbndlem1  27768  pntpbnd1  27801  axsegconlem9  29330  axeuclidlem  29367  smcnlem  31120  ipval2  31130  ipasslem2  31255  dipsubdir  31271  his2sub  31515  pjhthlem1  31814  quad3d  33164  constrrtlc1  34186  constrrtcc  34189  constrremulcl  34221  constrimcl  34224  constrreinvcl  34226  constrresqrtcl  34231  2sqr3minply  34234  cos9thpiminplylem1  34236  cos9thpiminplylem2  34237  circlemeth  35092  logdivsqrle  35102  fwddifnp1  36694  knoppndvlem2  37159  irrdiff  38027  itg2gt0cn  38383  iblsubnc  38389  itgsubnc  38390  itgmulc2nc  38396  ftc1anclem8  38408  ftc2nc  38410  areacirclem1  38416  primrootscoprbij  42927  bcle2d  43004  aks6d1c7lem1  43005  dffltz  43424  3cubeslem3r  43476  mzpsubmpt  43532  pellexlem6  43619  pell1234qrreccl  43639  pellfund14  43683  rmxyneg  43705  rmxm1  43719  rmym1  43720  congsub  43755  jm2.19lem1  43774  jm2.19lem4  43777  jm2.19  43778  jm2.26lem3  43786  sqrtcval  44425  sineq0ALT  45703  sub2times  46050  fzisoeu  46077  supsubc  46127  sublimc  46424  reclimc  46425  itgsincmulx  46746  itgsbtaddcnst  46754  stoweidlem10  46782  stoweidlem13  46785  stoweidlem22  46794  stoweidlem23  46795  stoweidlem26  46798  stoweidlem42  46814  stoweidlem47  46819  stirlinglem5  46850  dirkertrigeqlem2  46871  fourierdlem26  46905  fourierdlem36  46915  fourierdlem40  46919  fourierdlem41  46920  fourierdlem48  46926  fourierdlem49  46927  fourierdlem64  46942  fourierdlem78  46956  fourierdlem92  46970  fourierdlem97  46975  fourierdlem101  46979  fourierdlem107  46985  etransclem17  47023  etransclem46  47052  sigarperm  47632  modm2nep1  48167  modm1nep2  48169  modm1nem2  48170  quad1  48443  requad1  48445  requad2  48446  dignn0flhalflem1  49452  1subrec1sub  49542  eenglngeehlnmlem1  49574  eenglngeehlnmlem2  49575  rrx2linest2  49581  itscnhlc0yqe  49596  itschlc0yqe  49597  itsclc0yqsol  49601  itsclinecirc0b  49611  itsclquadb  49613