Theorem negsubd 11714

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   + caddc 11242   − cmin 11580   -cneg 11581

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-ltxr 11387  df-sub 11582  df-neg 11583

This theorem is used by:  mulsub  11798  mulsubaddmulsub  11820  divsubdir  12050  divsubdiv  12073  ofnegsub  12358  icoshftf1o  13645  fzosubel  13899  modaddb  14089  modsub12d  14111  expaddzlem  14288  binom2sub  14405  discr  14425  cjreb  15333  recj  15334  remullem  15338  imcj  15342  sqreulem  15571  subcn2  15806  lo1sub  15842  iseraltlem2  15894  iseraltlem3  15895  fsumshftm  15991  fsumsub  15998  incexclem  16049  incexc  16050  bpoly3  16268  efmival  16365  cosadd  16377  sinsub  16380  sincossq  16388  moddvds  16477  dvdsadd2b  16520  bitsres  16687  pythagtriplem4  17041  mulgdirlem  19365  mulgmodid  19373  mulgsubdir  19374  cnsubrg  21787  zringlpirlem3  21825  cphipval  25619  pjthlem1  25813  mbfsub  26038  mbfmulc2  26039  itg2monolem1  26126  itgcnlem  26165  iblsub  26197  itgsub  26201  itgmulc2  26209  dvmptsub  26342  dvmptdiv  26349  dvexp3  26353  dvsincos  26356  dvlipcn  26369  ftc2  26419  aaliou3lem6  26732  logdiv2  27002  tanarg  27004  advlogexp  27040  cxpsub  27067  abscxpbnd  27138  relogbdiv  27164  isosctrlem2  27204  angpieqvdlem  27213  quad2  27224  dcubic1lem  27228  dcubic2  27229  dcubic  27231  mcubic  27232  dquartlem2  27237  dquart  27238  quart1lem  27240  quartlem1  27242  quart  27246  asinlem2  27254  cosasin  27289  atanlogsublem  27300  atantan  27308  atantayl2  27323  ftalem5  27461  basellem9  27473  lgseisenlem1  27759  2sqlem4  27805  rpvmasum2  27896  log2sumbnd  27928  chpdifbndlem1  27937  pntpbnd1  27970  axsegconlem9  29560  axeuclidlem  29597  smcnlem  31356  ipval2  31366  ipasslem2  31491  dipsubdir  31507  his2sub  31751  pjhthlem1  32050  quad3d  33437  constrrtlc1  34475  constrrtcc  34478  constrremulcl  34510  constrimcl  34513  constrreinvcl  34515  constrresqrtcl  34520  2sqr3minply  34523  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  circlemeth  35380  logdivsqrle  35390  fwddifnp1  37145  knoppndvlem2  37594  irrdiff  38515  itg2gt0cn  38861  iblsubnc  38867  itgsubnc  38868  itgmulc2nc  38874  ftc1anclem8  38886  ftc2nc  38888  areacirclem1  38894  primrootscoprbij  43418  bcle2d  43495  aks6d1c7lem1  43496  dffltz  43936  3cubeslem3r  43963  mzpsubmpt  44020  pellexlem6  44107  pell1234qrreccl  44127  pellfund14  44171  rmxyneg  44193  rmxm1  44207  rmym1  44208  congsub  44243  jm2.19lem1  44262  jm2.19lem4  44265  jm2.19  44266  jm2.26lem3  44274  sqrtcval  44902  sineq0ALT  46179  sub2times  46562  fzisoeu  46589  supsubc  46638  sublimc  46935  reclimc  46936  itgsincmulx  47257  itgsbtaddcnst  47265  stoweidlem10  47293  stoweidlem13  47296  stoweidlem22  47305  stoweidlem23  47306  stoweidlem26  47309  stoweidlem42  47325  stoweidlem47  47330  stirlinglem5  47361  dirkertrigeqlem2  47382  fourierdlem26  47416  fourierdlem36  47426  fourierdlem40  47430  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  fourierdlem64  47453  fourierdlem78  47467  fourierdlem92  47481  fourierdlem97  47486  fourierdlem101  47490  fourierdlem107  47496  etransclem17  47534  etransclem46  47563  sigarperm  48143  modm2nep1  48715  modm1nep2  48717  modm1nem2  48718  quad1  48991  requad1  48993  requad2  48994  lazsubcl  49739  dignn0flhalflem1  50058  1subrec1sub  50148  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  rrx2linest2  50187  itscnhlc0yqe  50202  itschlc0yqe  50203  itsclc0yqsol  50207  itsclinecirc0b  50217  itsclquadb  50219  sinhsub  51256  coshsub  51257