Theorem negsubd 11481

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   + caddc 11012   − cmin 11347  -cneg 11348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349  df-neg 11350

This theorem is referenced by:  mulsub  11563  mulsubaddmulsub  11584  divsubdir  11818  divsubdiv  11840  ofnegsub  12126  icoshftf1o  13377  fzosubel  13627  modaddb  13813  modsub12d  13835  expaddzlem  14012  binom2sub  14127  discr  14147  cjreb  15030  recj  15031  remullem  15035  imcj  15039  sqreulem  15267  subcn2  15502  lo1sub  15538  iseraltlem2  15590  iseraltlem3  15591  fsumshftm  15688  fsumsub  15695  incexclem  15743  incexc  15744  bpoly3  15965  efmival  16062  cosadd  16074  sinsub  16077  sincossq  16085  moddvds  16174  dvdsadd2b  16217  bitsres  16384  pythagtriplem4  16731  mulgdirlem  18984  mulgmodid  18992  mulgsubdir  18993  cnsubrg  21334  zringlpirlem3  21371  cphipval  25141  pjthlem1  25335  mbfsub  25561  mbfmulc2  25562  itg2monolem1  25649  itgcnlem  25689  iblsub  25721  itgsub  25725  itgmulc2  25733  dvmptsub  25869  dvmptdiv  25876  dvexp3  25880  dvsincos  25883  dvlipcn  25897  ftc2  25949  aaliou3lem6  26254  logdiv2  26524  tanarg  26526  advlogexp  26562  cxpsub  26589  abscxpbnd  26661  relogbdiv  26687  isosctrlem2  26727  angpieqvdlem  26736  quad2  26747  dcubic1lem  26751  dcubic2  26752  dcubic  26754  mcubic  26755  dquartlem2  26760  dquart  26761  quart1lem  26763  quartlem1  26765  quart  26769  asinlem2  26777  cosasin  26812  atanlogsublem  26823  atantan  26831  atantayl2  26846  ftalem5  26985  basellem9  26997  lgseisenlem1  27284  2sqlem4  27330  rpvmasum2  27421  log2sumbnd  27453  chpdifbndlem1  27462  pntpbnd1  27495  axsegconlem9  28870  axeuclidlem  28907  smcnlem  30641  ipval2  30651  ipasslem2  30776  dipsubdir  30792  his2sub  31036  pjhthlem1  31335  quad3d  32693  constrrtlc1  33699  constrrtcc  33702  constrremulcl  33734  constrimcl  33737  constrreinvcl  33739  constrresqrtcl  33744  2sqr3minply  33747  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  circlemeth  34608  logdivsqrle  34618  fwddifnp1  36139  knoppndvlem2  36487  irrdiff  37300  itg2gt0cn  37655  iblsubnc  37661  itgsubnc  37662  itgmulc2nc  37668  ftc1anclem8  37680  ftc2nc  37682  areacirclem1  37688  primrootscoprbij  42075  bcle2d  42152  aks6d1c7lem1  42153  dffltz  42607  3cubeslem3r  42660  mzpsubmpt  42716  pellexlem6  42807  pell1234qrreccl  42827  pellfund14  42871  rmxyneg  42893  rmxm1  42907  rmym1  42908  congsub  42943  jm2.19lem1  42962  jm2.19lem4  42965  jm2.19  42966  jm2.26lem3  42974  sqrtcval  43614  sineq0ALT  44910  sub2times  45255  fzisoeu  45282  supsubc  45333  sublimc  45633  reclimc  45634  itgsincmulx  45955  itgsbtaddcnst  45963  stoweidlem10  45991  stoweidlem13  45994  stoweidlem22  46003  stoweidlem23  46004  stoweidlem26  46007  stoweidlem42  46023  stoweidlem47  46028  stirlinglem5  46059  dirkertrigeqlem2  46080  fourierdlem26  46114  fourierdlem36  46124  fourierdlem40  46128  fourierdlem41  46129  fourierdlem48  46135  fourierdlem49  46136  fourierdlem64  46151  fourierdlem78  46165  fourierdlem92  46179  fourierdlem97  46184  fourierdlem101  46188  fourierdlem107  46194  etransclem17  46232  etransclem46  46261  sigarperm  46841  modm2nep1  47350  modm1nep2  47352  modm1nem2  47353  quad1  47604  requad1  47606  requad2  47607  dignn0flhalflem1  48600  1subrec1sub  48690  eenglngeehlnmlem1  48722  eenglngeehlnmlem2  48723  rrx2linest2  48729  itscnhlc0yqe  48744  itschlc0yqe  48745  itsclc0yqsol  48749  itsclinecirc0b  48759  itsclquadb  48761