Theorem negcld 10787

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

Syntax hints:   → wi 4   ∈ wcel 2050  ℂcc 10335  -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:  negcon1ad  10795  mulsubaddmulsub  10907  recextlem1  11073  mul2lt0rlt0  12311  xov1plusxeqvd  12703  ceim1l  13033  modnegd  13112  expaddzlem  13290  cjreb  14346  sqrtneg  14491  max0add  14534  reusq0  14686  iseraltlem2  14903  iseraltlem3  14904  fsumsub  15006  telfsumo2  15021  incexc  15055  incexc2  15056  fallrisefac  15242  binomrisefac  15259  efi4p  15353  oexpneg  15557  bitscmp  15650  bitsf1  15658  pcadd2  16085  gznegcl  16130  mulgdirlem  18045  mulgdir  18046  znunit  20415  cphsqrtcl2  23496  pjthlem1  23746  mbfsub  23969  iblcnlem1  24094  itgcnlem  24096  iblneg  24109  itgneg  24110  iblsub  24128  itgsub  24132  ditgcl  24162  dvrec  24258  dvmptsub  24270  dvrecg  24276  dvmptdiv  24277  dvsincos  24284  rolle  24293  vieta1lem2  24606  vieta1  24607  sinmpi  24779  cosmpi  24780  sinppi  24781  cosppi  24782  tanabsge  24798  efeq1  24817  tanord  24826  logtayl  24947  logtayl2  24949  logccv  24950  cxpneg  24968  cxpmul2z  24978  logreclem  25044  cosangneg2d  25089  isosctrlem2  25101  isosctrlem3  25102  angpieqvdlem  25110  quad2  25121  dcubic1lem  25125  dcubic2  25126  dcubic  25128  mcubic  25129  dquartlem1  25133  dquartlem2  25134  dquart  25135  quartlem1  25139  quartlem2  25140  quartlem3  25141  quartlem4  25142  quart  25143  asinlem  25150  asinlem2  25151  asinneg  25168  sinasin  25171  cosasin  25186  atandmneg  25188  tanatan  25201  atandmtan  25202  atantan  25205  atantayl  25219  zetacvg  25297  dmgmaddnn0  25309  lgamgulmlem2  25312  lgamgulmlem4  25314  lgambdd  25319  lgamucov  25320  ftalem4  25358  ftalem5  25359  ftalem7  25361  basellem5  25367  chpdifbndlem1  25834  padicabvcxp  25913  brbtwn2  26397  ipasslem2  28389  pjhthlem1  28952  divnumden2  30283  archirngz  30484  madjusmdetlem4  30737  circlemeth  31559  logdivsqrle  31569  poimirlem29  34362  dvtan  34383  itg2addnclem3  34386  iblsubnc  34394  itgsubnc  34395  itgmulc2nc  34401  ftc1anclem5  34412  ftc1anclem8  34415  dvasin  34419  areacirclem1  34423  dffltz  38678  pell1234qrreccl  38847  pell14qrdich  38862  rmxyneg  38913  acongsym  38969  jm2.26a  38993  jm2.26lem3  38994  expgrowth  40083  binomcxplemdvbinom  40101  binomcxplemnotnn0  40104  sineq0ALT  40690  fzisoeu  40997  fperiodmul  41001  isumneg  41315  climneg  41323  neglimc  41360  sublimc  41365  reclimc  41366  dvcosre  41627  dvcosax  41642  itgsin0pilem1  41666  itgsinexplem1  41670  itgsincmulx  41690  stoweidlem13  41730  stirlinglem5  41795  dirkertrigeqlem3  41817  fourierdlem30  41854  fourierdlem39  41863  fourierdlem40  41864  fourierdlem41  41865  fourierdlem43  41867  fourierdlem47  41870  fourierdlem48  41871  fourierdlem49  41872  fourierdlem73  41896  fourierdlem78  41901  fourierdlem92  41915  fourierdlem101  41924  fourierdlem103  41926  fourierdlem111  41934  sqwvfoura  41945  fouriersw  41948  etransclem17  41968  etransclem18  41969  etransclem23  41974  etransclem46  41997  sigarms  42545  sigaradd  42555  sqrtnegnre  42914  quad1  43154  requad01  43155  requad1  43156  requad2  43157  oexpnegALTV  43211  oexpnegnz  43212  2zrngagrp  43579  altgsumbc  43765  dignn0flhalflem1  44044  line2ylem  44107  itschlc0yqe  44116  itsclc0yqsol  44120  itschlc0xyqsol  44123  amgmwlem  44271