Theorem negsubd 11623

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155   − cmin 11489  -cneg 11490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491  df-neg 11492

This theorem is referenced by:  mulsub  11703  mulsubaddmulsub  11724  divsubdir  11958  divsubdiv  11980  ofnegsub  12261  icoshftf1o  13510  fzosubel  13759  modsub12d  13965  expaddzlem  14142  binom2sub  14255  discr  14275  cjreb  15158  recj  15159  remullem  15163  imcj  15167  sqreulem  15394  subcn2  15627  lo1sub  15663  iseraltlem2  15715  iseraltlem3  15716  fsumshftm  15813  fsumsub  15820  incexclem  15868  incexc  15869  bpoly3  16090  efmival  16185  cosadd  16197  sinsub  16200  sincossq  16208  moddvds  16297  dvdsadd2b  16339  bitsres  16506  pythagtriplem4  16852  mulgdirlem  19135  mulgmodid  19143  mulgsubdir  19144  cnsubrg  21462  zringlpirlem3  21492  cphipval  25290  pjthlem1  25484  mbfsub  25710  mbfmulc2  25711  itg2monolem1  25799  itgcnlem  25839  iblsub  25871  itgsub  25875  itgmulc2  25883  dvmptsub  26019  dvmptdiv  26026  dvexp3  26030  dvsincos  26033  dvlipcn  26047  ftc2  26099  aaliou3lem6  26404  logdiv2  26673  tanarg  26675  advlogexp  26711  cxpsub  26738  abscxpbnd  26810  relogbdiv  26836  isosctrlem2  26876  angpieqvdlem  26885  quad2  26896  dcubic1lem  26900  dcubic2  26901  dcubic  26903  mcubic  26904  dquartlem2  26909  dquart  26910  quart1lem  26912  quartlem1  26914  quart  26918  asinlem2  26926  cosasin  26961  atanlogsublem  26972  atantan  26980  atantayl2  26995  ftalem5  27134  basellem9  27146  lgseisenlem1  27433  2sqlem4  27479  rpvmasum2  27570  log2sumbnd  27602  chpdifbndlem1  27611  pntpbnd1  27644  axsegconlem9  28954  axeuclidlem  28991  smcnlem  30725  ipval2  30735  ipasslem2  30860  dipsubdir  30876  his2sub  31120  pjhthlem1  31419  quad3d  32760  constrrtlc1  33737  constrrtcc  33740  2sqr3minply  33752  circlemeth  34633  logdivsqrle  34643  fwddifnp1  36146  knoppndvlem2  36495  irrdiff  37308  itg2gt0cn  37661  iblsubnc  37667  itgsubnc  37668  itgmulc2nc  37674  ftc1anclem8  37686  ftc2nc  37688  areacirclem1  37694  primrootscoprbij  42083  bcle2d  42160  aks6d1c7lem1  42161  dffltz  42620  3cubeslem3r  42674  mzpsubmpt  42730  pellexlem6  42821  pell1234qrreccl  42841  pellfund14  42885  rmxyneg  42908  rmxm1  42922  rmym1  42923  congsub  42958  jm2.19lem1  42977  jm2.19lem4  42980  jm2.19  42981  jm2.26lem3  42989  sqrtcval  43630  sineq0ALT  44934  sub2times  45222  fzisoeu  45250  supsubc  45302  sublimc  45607  reclimc  45608  itgsincmulx  45929  itgsbtaddcnst  45937  stoweidlem10  45965  stoweidlem13  45968  stoweidlem22  45977  stoweidlem23  45978  stoweidlem26  45981  stoweidlem42  45997  stoweidlem47  46002  stirlinglem5  46033  dirkertrigeqlem2  46054  fourierdlem26  46088  fourierdlem36  46098  fourierdlem40  46102  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem64  46125  fourierdlem78  46139  fourierdlem92  46153  fourierdlem97  46158  fourierdlem101  46162  fourierdlem107  46168  etransclem17  46206  etransclem46  46235  sigarperm  46815  quad1  47544  requad1  47546  requad2  47547  dignn0flhalflem1  48464  1subrec1sub  48554  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrx2linest2  48593  itscnhlc0yqe  48608  itschlc0yqe  48609  itsclc0yqsol  48613  itsclinecirc0b  48623  itsclquadb  48625