Theorem negsubd 10806

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

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  (class class class)co 6978  ℂcc 10335   + caddc 10340   − cmin 10672  -cneg 10673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-po 5327  df-so 5328  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-er 8091  df-en 8309  df-dom 8310  df-sdom 8311  df-pnf 10478  df-mnf 10479  df-ltxr 10481  df-sub 10674  df-neg 10675

This theorem is referenced by:  mulsub  10886  mulsubaddmulsub  10907  divsubdir  11137  divsubdiv  11159  ofnegsub  11439  icoshftf1o  12679  fzosubel  12914  modsub12d  13114  expaddzlem  13290  binom2sub  13399  discr  13419  cjreb  14346  recj  14347  remullem  14351  imcj  14355  sqreulem  14583  subcn2  14815  lo1sub  14851  iseraltlem2  14903  iseraltlem3  14904  fsumshftm  14999  fsumsub  15006  incexclem  15054  incexc  15055  bpoly3  15275  efmival  15369  cosadd  15381  sinsub  15384  sincossq  15392  moddvds  15481  dvdsadd2b  15519  bitsres  15685  pythagtriplem4  16015  mulgdirlem  18045  mulgmodid  18053  mulgsubdir  18054  cnsubrg  20310  zringlpirlem3  20338  cphipval  23552  pjthlem1  23746  mbfsub  23969  mbfmulc2  23970  itg2monolem1  24057  itgcnlem  24096  iblsub  24128  itgsub  24132  itgmulc2  24140  dvmptsub  24270  dvmptdiv  24277  dvexp3  24281  dvsincos  24284  dvlipcn  24297  ftc2  24347  aaliou3lem6  24643  logdiv2  24904  tanarg  24906  advlogexp  24942  cxpsub  24969  abscxpbnd  25038  relogbdiv  25061  isosctrlem2  25101  angpieqvdlem  25110  quad2  25121  dcubic1lem  25125  dcubic2  25126  dcubic  25128  mcubic  25129  dquartlem2  25134  dquart  25135  quart1lem  25137  quartlem1  25139  quart  25143  asinlem2  25151  cosasin  25186  atanlogsublem  25197  atantan  25205  atantayl2  25220  ftalem5  25359  basellem9  25371  lgseisenlem1  25656  2sqlem4  25702  rpvmasum2  25793  log2sumbnd  25825  chpdifbndlem1  25834  pntpbnd1  25867  axsegconlem9  26417  axeuclidlem  26454  smcnlem  28254  ipval2  28264  ipasslem2  28389  dipsubdir  28405  his2sub  28651  pjhthlem1  28952  circlemeth  31559  logdivsqrle  31569  fwddifnp1  33147  knoppndvlem2  33372  itg2gt0cn  34388  iblsubnc  34394  itgsubnc  34395  itgmulc2nc  34401  ftc1anclem8  34415  ftc2nc  34417  areacirclem1  34423  dffltz  38678  mzpsubmpt  38735  pellexlem6  38827  pell1234qrreccl  38847  pellfund14  38891  rmxyneg  38913  rmxm1  38927  rmym1  38928  congsub  38963  jm2.19lem1  38982  jm2.19lem4  38985  jm2.19  38986  jm2.26lem3  38994  sineq0ALT  40690  sub2times  40970  fzisoeu  40997  supsubc  41051  sublimc  41365  reclimc  41366  itgsincmulx  41690  itgsbtaddcnst  41698  stoweidlem10  41727  stoweidlem13  41730  stoweidlem22  41739  stoweidlem23  41740  stoweidlem26  41743  stoweidlem42  41759  stoweidlem47  41764  stirlinglem5  41795  dirkertrigeqlem2  41816  fourierdlem26  41850  fourierdlem36  41860  fourierdlem40  41864  fourierdlem41  41865  fourierdlem48  41871  fourierdlem49  41872  fourierdlem64  41887  fourierdlem78  41901  fourierdlem92  41915  fourierdlem97  41920  fourierdlem101  41924  fourierdlem107  41930  etransclem17  41968  etransclem46  41997  sigarperm  42549  quad1  43154  requad1  43156  requad2  43157  dignn0flhalflem1  44044  1subrec1sub  44061  eenglngeehlnmlem1  44093  eenglngeehlnmlem2  44094  rrx2linest2  44100  itscnhlc0yqe  44115  itschlc0yqe  44116  itsclc0yqsol  44120  itsclinecirc0b  44130  itsclquadb  44132