Theorem negcld 11483

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 11384	. 2 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11028  -cneg 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-neg 11371

This theorem is referenced by:  negcon1ad  11491  mulsubaddmulsub  11605  recextlem1  11771  mul2lt0rlt0  13013  xov1plusxeqvd  13418  ceim1l  13771  modnegd  13853  expaddzlem  14032  cjreb  15050  sqrtneg  15194  max0add  15237  reusq0  15392  iseraltlem2  15610  iseraltlem3  15611  fsumsub  15715  telfsumo2  15730  incexc  15764  incexc2  15765  fallrisefac  15952  binomrisefac  15969  efne0d  16024  efi4p  16066  oexpneg  16276  bitscmp  16369  bitsf1  16377  pcadd2  16822  gznegcl  16867  mulgdirlem  19039  mulgdir  19040  znunit  21522  cphsqrtcl2  25146  pjthlem1  25397  mbfsub  25623  iblcnlem1  25749  itgcnlem  25751  iblneg  25764  itgneg  25765  iblsub  25783  itgsub  25787  ditgcl  25819  dvrec  25919  dvmptsub  25931  dvrecg  25937  dvmptdiv  25938  dvsincos  25945  rolle  25954  vieta1lem2  26279  vieta1  26280  sinmpi  26456  cosmpi  26457  sinppi  26458  cosppi  26459  tanabsge  26475  efeq1  26497  tanord  26507  logtayl  26629  logtayl2  26631  logccv  26632  cxpneg  26650  cxpmul2z  26660  logreclem  26732  cosangneg2d  26777  isosctrlem2  26789  isosctrlem3  26790  angpieqvdlem  26798  quad2  26809  dcubic1lem  26813  dcubic2  26814  dcubic  26816  mcubic  26817  dquartlem1  26821  dquartlem2  26822  dquart  26823  quartlem1  26827  quartlem2  26828  quartlem3  26829  quartlem4  26830  quart  26831  asinlem  26838  asinlem2  26839  asinneg  26856  sinasin  26859  cosasin  26874  atandmneg  26876  tanatan  26889  atandmtan  26890  atantan  26893  atantayl  26907  zetacvg  26985  dmgmaddnn0  26997  lgamgulmlem2  27000  lgamgulmlem4  27002  lgambdd  27007  lgamucov  27008  ftalem4  27046  ftalem5  27047  ftalem7  27049  basellem5  27055  chpdifbndlem1  27524  padicabvcxp  27603  brbtwn2  28982  ipasslem2  30911  pjhthlem1  31470  quad3d  32831  divnumden2  32898  archirngz  33273  constrrtlc1  33891  constrrtcclem  33893  constrrtcc  33894  constrfin  33905  constrnegcl  33922  iconstr  33925  constrremulcl  33926  2sqr3minply  33939  cos9thpiminplylem1  33941  cos9thpiminplylem2  33942  madjusmdetlem4  33989  circlemeth  34799  logdivsqrle  34809  poimirlem29  37852  dvtan  37873  itg2addnclem3  37876  iblsubnc  37884  itgsubnc  37885  itgmulc2nc  37891  ftc1anclem5  37900  ftc1anclem8  37903  dvasin  37907  areacirclem1  37911  lcmineqlem10  42360  lcmineqlem12  42362  posbezout  42422  redvmptabs  42682  dffltz  42944  3cubeslem3r  42996  pell1234qrreccl  43163  pell14qrdich  43178  rmxyneg  43229  acongsym  43285  jm2.26a  43309  jm2.26lem3  43310  expgrowth  44643  binomcxplemdvbinom  44661  binomcxplemnotnn0  44664  sineq0ALT  45244  fzisoeu  45615  fperiodmul  45619  isumneg  45915  climneg  45923  neglimc  45958  sublimc  45963  reclimc  45964  dvcosre  46223  dvcosax  46237  itgsin0pilem1  46261  itgsinexplem1  46265  itgsincmulx  46285  stoweidlem13  46324  stirlinglem5  46389  dirkertrigeqlem3  46411  fourierdlem30  46448  fourierdlem39  46457  fourierdlem40  46458  fourierdlem41  46459  fourierdlem43  46461  fourierdlem47  46464  fourierdlem48  46465  fourierdlem49  46466  fourierdlem73  46490  fourierdlem78  46495  fourierdlem92  46509  fourierdlem101  46518  fourierdlem103  46520  fourierdlem111  46528  sqwvfoura  46539  fouriersw  46542  etransclem17  46562  etransclem18  46563  etransclem23  46568  etransclem46  46591  sigarms  47167  sigaradd  47177  sqrtnegnre  47620  quad1  47933  requad01  47934  requad1  47935  requad2  47936  oexpnegALTV  47990  oexpnegnz  47991  2zrngagrp  48562  altgsumbc  48665  dignn0flhalflem1  48928  line2ylem  49064  itschlc0yqe  49073  itsclc0yqsol  49077  itschlc0xyqsol  49080  amgmwlem  50114