Theorem negsubd 11571

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  (class class class)co 7408  ℂcc 11094   + caddc 11099   − cmin 11437  -cneg 11438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-ltxr 11244  df-sub 11439  df-neg 11440

This theorem is referenced by:  mulsub  11653  mulsubaddmulsub  11674  divsubdir  11904  divsubdiv  11927  ofnegsub  12212  icoshftf1o  13497  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  16108  efmival  16205  cosadd  16217  sinsub  16220  sincossq  16228  moddvds  16317  dvdsadd2b  16360  bitsres  16527  pythagtriplem4  16875  mulgdirlem  19167  mulgmodid  19175  mulgsubdir  19176  cnsubrg  21542  zringlpirlem3  21579  cphipval  25367  pjthlem1  25561  mbfsub  25786  mbfmulc2  25787  itg2monolem1  25874  itgcnlem  25914  iblsub  25946  itgsub  25950  itgmulc2  25958  dvmptsub  26091  dvmptdiv  26098  dvexp3  26102  dvsincos  26105  dvlipcn  26118  ftc2  26168  aaliou3lem6  26474  logdiv2  26744  tanarg  26746  advlogexp  26782  cxpsub  26809  abscxpbnd  26880  relogbdiv  26906  isosctrlem2  26946  angpieqvdlem  26955  quad2  26966  dcubic1lem  26970  dcubic2  26971  dcubic  26973  mcubic  26974  dquartlem2  26979  dquart  26980  quart1lem  26982  quartlem1  26984  quart  26988  asinlem2  26996  cosasin  27031  atanlogsublem  27042  atantan  27050  atantayl2  27065  ftalem5  27203  basellem9  27215  lgseisenlem1  27501  2sqlem4  27547  rpvmasum2  27638  log2sumbnd  27670  chpdifbndlem1  27679  pntpbnd1  27712  axsegconlem9  29212  axeuclidlem  29249  smcnlem  30986  ipval2  30996  ipasslem2  31121  dipsubdir  31137  his2sub  31381  pjhthlem1  31680  quad3d  33031  constrrtlc1  34063  constrrtcc  34066  constrremulcl  34098  constrimcl  34101  constrreinvcl  34103  constrresqrtcl  34108  2sqr3minply  34111  cos9thpiminplylem1  34113  cos9thpiminplylem2  34114  circlemeth  34968  logdivsqrle  34978  fwddifnp1  36552  knoppndvlem2  36987  irrdiff  37853  itg2gt0cn  38209  iblsubnc  38215  itgsubnc  38216  itgmulc2nc  38222  ftc1anclem8  38234  ftc2nc  38236  areacirclem1  38242  primrootscoprbij  42754  bcle2d  42831  aks6d1c7lem1  42832  dffltz  43253  3cubeslem3r  43305  mzpsubmpt  43361  pellexlem6  43448  pell1234qrreccl  43468  pellfund14  43512  rmxyneg  43534  rmxm1  43548  rmym1  43549  congsub  43584  jm2.19lem1  43603  jm2.19lem4  43606  jm2.19  43607  jm2.26lem3  43615  sqrtcval  44254  sineq0ALT  45532  sub2times  45879  fzisoeu  45906  supsubc  45956  sublimc  46253  reclimc  46254  itgsincmulx  46575  itgsbtaddcnst  46583  stoweidlem10  46611  stoweidlem13  46614  stoweidlem22  46623  stoweidlem23  46624  stoweidlem26  46627  stoweidlem42  46643  stoweidlem47  46648  stirlinglem5  46679  dirkertrigeqlem2  46700  fourierdlem26  46734  fourierdlem36  46744  fourierdlem40  46748  fourierdlem41  46749  fourierdlem48  46755  fourierdlem49  46756  fourierdlem64  46771  fourierdlem78  46785  fourierdlem92  46799  fourierdlem97  46804  fourierdlem101  46808  fourierdlem107  46814  etransclem17  46852  etransclem46  46881  sigarperm  47461  modm2nep1  47993  modm1nep2  47995  modm1nem2  47996  quad1  48269  requad1  48271  requad2  48272  dignn0flhalflem1  49275  1subrec1sub  49365  eenglngeehlnmlem1  49397  eenglngeehlnmlem2  49398  rrx2linest2  49404  itscnhlc0yqe  49419  itschlc0yqe  49420  itsclc0yqsol  49424  itsclinecirc0b  49434  itsclquadb  49436