Theorem negsubd 11338

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   + caddc 10874   − cmin 11205  -cneg 11206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-ltxr 11014  df-sub 11207  df-neg 11208

This theorem is referenced by:  mulsub  11418  mulsubaddmulsub  11439  divsubdir  11669  divsubdiv  11691  ofnegsub  11971  icoshftf1o  13206  fzosubel  13446  modsub12d  13648  expaddzlem  13826  binom2sub  13935  discr  13955  cjreb  14834  recj  14835  remullem  14839  imcj  14843  sqreulem  15071  subcn2  15304  lo1sub  15340  iseraltlem2  15394  iseraltlem3  15395  fsumshftm  15493  fsumsub  15500  incexclem  15548  incexc  15549  bpoly3  15768  efmival  15862  cosadd  15874  sinsub  15877  sincossq  15885  moddvds  15974  dvdsadd2b  16015  bitsres  16180  pythagtriplem4  16520  mulgdirlem  18734  mulgmodid  18742  mulgsubdir  18743  cnsubrg  20658  zringlpirlem3  20686  cphipval  24407  pjthlem1  24601  mbfsub  24826  mbfmulc2  24827  itg2monolem1  24915  itgcnlem  24954  iblsub  24986  itgsub  24990  itgmulc2  24998  dvmptsub  25131  dvmptdiv  25138  dvexp3  25142  dvsincos  25145  dvlipcn  25158  ftc2  25208  aaliou3lem6  25508  logdiv2  25772  tanarg  25774  advlogexp  25810  cxpsub  25837  abscxpbnd  25906  relogbdiv  25929  isosctrlem2  25969  angpieqvdlem  25978  quad2  25989  dcubic1lem  25993  dcubic2  25994  dcubic  25996  mcubic  25997  dquartlem2  26002  dquart  26003  quart1lem  26005  quartlem1  26007  quart  26011  asinlem2  26019  cosasin  26054  atanlogsublem  26065  atantan  26073  atantayl2  26088  ftalem5  26226  basellem9  26238  lgseisenlem1  26523  2sqlem4  26569  rpvmasum2  26660  log2sumbnd  26692  chpdifbndlem1  26701  pntpbnd1  26734  axsegconlem9  27293  axeuclidlem  27330  smcnlem  29059  ipval2  29069  ipasslem2  29194  dipsubdir  29210  his2sub  29454  pjhthlem1  29753  circlemeth  32620  logdivsqrle  32630  fwddifnp1  34467  knoppndvlem2  34693  irrdiff  35497  itg2gt0cn  35832  iblsubnc  35838  itgsubnc  35839  itgmulc2nc  35845  ftc1anclem8  35857  ftc2nc  35859  areacirclem1  35865  dffltz  40471  3cubeslem3r  40509  mzpsubmpt  40565  pellexlem6  40656  pell1234qrreccl  40676  pellfund14  40720  rmxyneg  40742  rmxm1  40756  rmym1  40757  congsub  40792  jm2.19lem1  40811  jm2.19lem4  40814  jm2.19  40815  jm2.26lem3  40823  sqrtcval  41249  sineq0ALT  42557  sub2times  42813  fzisoeu  42839  supsubc  42892  sublimc  43193  reclimc  43194  itgsincmulx  43515  itgsbtaddcnst  43523  stoweidlem10  43551  stoweidlem13  43554  stoweidlem22  43563  stoweidlem23  43564  stoweidlem26  43567  stoweidlem42  43583  stoweidlem47  43588  stirlinglem5  43619  dirkertrigeqlem2  43640  fourierdlem26  43674  fourierdlem36  43684  fourierdlem40  43688  fourierdlem41  43689  fourierdlem48  43695  fourierdlem49  43696  fourierdlem64  43711  fourierdlem78  43725  fourierdlem92  43739  fourierdlem97  43744  fourierdlem101  43748  fourierdlem107  43754  etransclem17  43792  etransclem46  43821  sigarperm  44376  quad1  45072  requad1  45074  requad2  45075  dignn0flhalflem1  45961  1subrec1sub  46051  eenglngeehlnmlem1  46083  eenglngeehlnmlem2  46084  rrx2linest2  46090  itscnhlc0yqe  46105  itschlc0yqe  46106  itsclc0yqsol  46110  itsclinecirc0b  46120  itsclquadb  46122