Theorem negsubd 11653

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187   − cmin 11520  -cneg 11521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11522  df-neg 11523

This theorem is referenced by:  mulsub  11733  mulsubaddmulsub  11754  divsubdir  11988  divsubdiv  12010  ofnegsub  12291  icoshftf1o  13534  fzosubel  13775  modsub12d  13979  expaddzlem  14156  binom2sub  14269  discr  14289  cjreb  15172  recj  15173  remullem  15177  imcj  15181  sqreulem  15408  subcn2  15641  lo1sub  15677  iseraltlem2  15731  iseraltlem3  15732  fsumshftm  15829  fsumsub  15836  incexclem  15884  incexc  15885  bpoly3  16106  efmival  16201  cosadd  16213  sinsub  16216  sincossq  16224  moddvds  16313  dvdsadd2b  16354  bitsres  16519  pythagtriplem4  16866  mulgdirlem  19145  mulgmodid  19153  mulgsubdir  19154  cnsubrg  21468  zringlpirlem3  21498  cphipval  25296  pjthlem1  25490  mbfsub  25716  mbfmulc2  25717  itg2monolem1  25805  itgcnlem  25845  iblsub  25877  itgsub  25881  itgmulc2  25889  dvmptsub  26025  dvmptdiv  26032  dvexp3  26036  dvsincos  26039  dvlipcn  26053  ftc2  26105  aaliou3lem6  26408  logdiv2  26677  tanarg  26679  advlogexp  26715  cxpsub  26742  abscxpbnd  26814  relogbdiv  26840  isosctrlem2  26880  angpieqvdlem  26889  quad2  26900  dcubic1lem  26904  dcubic2  26905  dcubic  26907  mcubic  26908  dquartlem2  26913  dquart  26914  quart1lem  26916  quartlem1  26918  quart  26922  asinlem2  26930  cosasin  26965  atanlogsublem  26976  atantan  26984  atantayl2  26999  ftalem5  27138  basellem9  27150  lgseisenlem1  27437  2sqlem4  27483  rpvmasum2  27574  log2sumbnd  27606  chpdifbndlem1  27615  pntpbnd1  27648  axsegconlem9  28958  axeuclidlem  28995  smcnlem  30729  ipval2  30739  ipasslem2  30864  dipsubdir  30880  his2sub  31124  pjhthlem1  31423  quad3d  32757  constrrtlc1  33723  constrrtcc  33726  2sqr3minply  33738  circlemeth  34617  logdivsqrle  34627  fwddifnp1  36129  knoppndvlem2  36479  irrdiff  37292  itg2gt0cn  37635  iblsubnc  37641  itgsubnc  37642  itgmulc2nc  37648  ftc1anclem8  37660  ftc2nc  37662  areacirclem1  37668  primrootscoprbij  42059  bcle2d  42136  aks6d1c7lem1  42137  dffltz  42589  3cubeslem3r  42643  mzpsubmpt  42699  pellexlem6  42790  pell1234qrreccl  42810  pellfund14  42854  rmxyneg  42877  rmxm1  42891  rmym1  42892  congsub  42927  jm2.19lem1  42946  jm2.19lem4  42949  jm2.19  42950  jm2.26lem3  42958  sqrtcval  43603  sineq0ALT  44908  sub2times  45187  fzisoeu  45215  supsubc  45268  sublimc  45573  reclimc  45574  itgsincmulx  45895  itgsbtaddcnst  45903  stoweidlem10  45931  stoweidlem13  45934  stoweidlem22  45943  stoweidlem23  45944  stoweidlem26  45947  stoweidlem42  45963  stoweidlem47  45968  stirlinglem5  45999  dirkertrigeqlem2  46020  fourierdlem26  46054  fourierdlem36  46064  fourierdlem40  46068  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem64  46091  fourierdlem78  46105  fourierdlem92  46119  fourierdlem97  46124  fourierdlem101  46128  fourierdlem107  46134  etransclem17  46172  etransclem46  46201  sigarperm  46781  quad1  47494  requad1  47496  requad2  47497  dignn0flhalflem1  48349  1subrec1sub  48439  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2linest2  48478  itscnhlc0yqe  48493  itschlc0yqe  48494  itsclc0yqsol  48498  itsclinecirc0b  48508  itsclquadb  48510