Theorem negcld 11558

Description: Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
negcld	⊢ (𝜑 → -𝐴 ∈ ℂ)

Proof of Theorem negcld

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		negcl 11460	. 2 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  -cneg 11445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-ltxr 11253  df-sub 11446  df-neg 11447

This theorem is referenced by:  negcon1ad  11566  mulsubaddmulsub  11678  recextlem1  11844  mul2lt0rlt0  13076  xov1plusxeqvd  13475  ceim1l  13812  modnegd  13891  expaddzlem  14071  cjreb  15070  sqrtneg  15214  max0add  15257  reusq0  15409  iseraltlem2  15629  iseraltlem3  15630  fsumsub  15734  telfsumo2  15749  incexc  15783  incexc2  15784  fallrisefac  15969  binomrisefac  15986  efi4p  16080  oexpneg  16288  bitscmp  16379  bitsf1  16387  pcadd2  16823  gznegcl  16868  mulgdirlem  18985  mulgdir  18986  znunit  21119  cphsqrtcl2  24703  pjthlem1  24954  mbfsub  25179  iblcnlem1  25305  itgcnlem  25307  iblneg  25320  itgneg  25321  iblsub  25339  itgsub  25343  ditgcl  25375  dvrec  25472  dvmptsub  25484  dvrecg  25490  dvmptdiv  25491  dvsincos  25498  rolle  25507  vieta1lem2  25824  vieta1  25825  sinmpi  25997  cosmpi  25998  sinppi  25999  cosppi  26000  tanabsge  26016  efeq1  26037  tanord  26047  logtayl  26168  logtayl2  26170  logccv  26171  cxpneg  26189  cxpmul2z  26199  logreclem  26267  cosangneg2d  26312  isosctrlem2  26324  isosctrlem3  26325  angpieqvdlem  26333  quad2  26344  dcubic1lem  26348  dcubic2  26349  dcubic  26351  mcubic  26352  dquartlem1  26356  dquartlem2  26357  dquart  26358  quartlem1  26362  quartlem2  26363  quartlem3  26364  quartlem4  26365  quart  26366  asinlem  26373  asinlem2  26374  asinneg  26391  sinasin  26394  cosasin  26409  atandmneg  26411  tanatan  26424  atandmtan  26425  atantan  26428  atantayl  26442  zetacvg  26519  dmgmaddnn0  26531  lgamgulmlem2  26534  lgamgulmlem4  26536  lgambdd  26541  lgamucov  26542  ftalem4  26580  ftalem5  26581  ftalem7  26583  basellem5  26589  chpdifbndlem1  27056  padicabvcxp  27135  brbtwn2  28194  ipasslem2  30116  pjhthlem1  30675  divnumden2  32055  archirngz  32366  madjusmdetlem4  32841  circlemeth  33683  logdivsqrle  33693  poimirlem29  36565  dvtan  36586  itg2addnclem3  36589  iblsubnc  36597  itgsubnc  36598  itgmulc2nc  36604  ftc1anclem5  36613  ftc1anclem8  36616  dvasin  36620  areacirclem1  36624  lcmineqlem10  40951  lcmineqlem12  40953  dffltz  41424  3cubeslem3r  41473  pell1234qrreccl  41640  pell14qrdich  41655  rmxyneg  41707  acongsym  41763  jm2.26a  41787  jm2.26lem3  41788  expgrowth  43142  binomcxplemdvbinom  43160  binomcxplemnotnn0  43163  sineq0ALT  43746  fzisoeu  44058  fperiodmul  44062  isumneg  44366  climneg  44374  neglimc  44411  sublimc  44416  reclimc  44417  dvcosre  44676  dvcosax  44690  itgsin0pilem1  44714  itgsinexplem1  44718  itgsincmulx  44738  stoweidlem13  44777  stirlinglem5  44842  dirkertrigeqlem3  44864  fourierdlem30  44901  fourierdlem39  44910  fourierdlem40  44911  fourierdlem41  44912  fourierdlem43  44914  fourierdlem47  44917  fourierdlem48  44918  fourierdlem49  44919  fourierdlem73  44943  fourierdlem78  44948  fourierdlem92  44962  fourierdlem101  44971  fourierdlem103  44973  fourierdlem111  44981  sqwvfoura  44992  fouriersw  44995  etransclem17  45015  etransclem18  45016  etransclem23  45021  etransclem46  45044  sigarms  45620  sigaradd  45630  sqrtnegnre  46063  quad1  46336  requad01  46337  requad1  46338  requad2  46339  oexpnegALTV  46393  oexpnegnz  46394  2zrngagrp  46889  altgsumbc  47076  dignn0flhalflem1  47349  line2ylem  47485  itschlc0yqe  47494  itsclc0yqsol  47498  itschlc0xyqsol  47501  amgmwlem  47897