Theorem negcld 11487

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

Syntax hints:   → wi 4   ∈ wcel 2121  ℂcc 11031  -cneg 11373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  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 11176  df-mnf 11177  df-ltxr 11179  df-sub 11374  df-neg 11375

This theorem is referenced by:  negcon1ad  11495  mulsubaddmulsub  11609  recextlem1  11775  mul2lt0rlt0  13041  xov1plusxeqvd  13446  ceim1l  13801  modnegd  13883  expaddzlem  14062  cjreb  15080  sqrtneg  15224  max0add  15267  reusq0  15422  iseraltlem2  15640  iseraltlem3  15641  fsumsub  15745  telfsumo2  15761  incexc  15797  incexc2  15798  fallrisefac  15985  binomrisefac  16002  efne0d  16057  efi4p  16099  oexpneg  16309  bitscmp  16402  bitsf1  16410  pcadd2  16856  gznegcl  16901  mulgdirlem  19076  mulgdir  19077  znunit  21542  cphsqrtcl2  25175  pjthlem1  25426  mbfsub  25651  iblcnlem1  25777  itgcnlem  25779  iblneg  25792  itgneg  25793  iblsub  25811  itgsub  25815  ditgcl  25847  dvrec  25944  dvmptsub  25956  dvrecg  25962  dvmptdiv  25963  dvsincos  25970  rolle  25979  vieta1lem2  26299  vieta1  26300  sinmpi  26473  cosmpi  26474  sinppi  26475  cosppi  26476  tanabsge  26492  efeq1  26514  tanord  26524  logtayl  26646  logtayl2  26648  logccv  26649  cxpneg  26667  cxpmul2z  26677  logreclem  26748  cosangneg2d  26793  isosctrlem2  26805  isosctrlem3  26806  angpieqvdlem  26814  quad2  26825  dcubic1lem  26829  dcubic2  26830  dcubic  26832  mcubic  26833  dquartlem1  26837  dquartlem2  26838  dquart  26839  quartlem1  26843  quartlem2  26844  quartlem3  26845  quartlem4  26846  quart  26847  asinlem  26854  asinlem2  26855  asinneg  26872  sinasin  26875  cosasin  26890  atandmneg  26892  tanatan  26905  atandmtan  26906  atantan  26909  atantayl  26923  zetacvg  27000  dmgmaddnn0  27012  lgamgulmlem2  27015  lgamgulmlem4  27017  lgambdd  27022  lgamucov  27023  ftalem4  27061  ftalem5  27062  ftalem7  27064  basellem5  27070  chpdifbndlem1  27538  padicabvcxp  27617  brbtwn2  28996  ipasslem2  30925  pjhthlem1  31484  quad3d  32845  divnumden2  32912  archirngz  33274  constrrtlc1  33928  constrrtcclem  33930  constrrtcc  33931  constrfin  33942  constrnegcl  33959  iconstr  33962  constrremulcl  33963  2sqr3minply  33976  cos9thpiminplylem1  33978  cos9thpiminplylem2  33979  madjusmdetlem4  34026  circlemeth  34836  logdivsqrle  34846  poimirlem29  38031  dvtan  38052  itg2addnclem3  38055  iblsubnc  38063  itgsubnc  38064  itgmulc2nc  38070  ftc1anclem5  38079  ftc1anclem8  38082  dvasin  38086  areacirclem1  38090  lcmineqlem10  42538  lcmineqlem12  42540  posbezout  42600  redvmptabs  42852  dffltz  43099  3cubeslem3r  43151  pell1234qrreccl  43314  pell14qrdich  43329  rmxyneg  43380  acongsym  43436  jm2.26a  43460  jm2.26lem3  43461  expgrowth  44794  binomcxplemdvbinom  44812  binomcxplemnotnn0  44815  sineq0ALT  45395  fzisoeu  45762  fperiodmul  45766  isumneg  46061  climneg  46069  neglimc  46104  sublimc  46109  reclimc  46110  dvcosre  46369  dvcosax  46383  itgsin0pilem1  46407  itgsinexplem1  46411  itgsincmulx  46431  stoweidlem13  46470  stirlinglem5  46535  dirkertrigeqlem3  46557  fourierdlem30  46594  fourierdlem39  46603  fourierdlem40  46604  fourierdlem41  46605  fourierdlem43  46607  fourierdlem47  46610  fourierdlem48  46611  fourierdlem49  46612  fourierdlem73  46636  fourierdlem78  46641  fourierdlem92  46655  fourierdlem101  46664  fourierdlem103  46666  fourierdlem111  46674  sqwvfoura  46685  fouriersw  46688  etransclem17  46708  etransclem18  46709  etransclem23  46714  etransclem46  46737  sigarms  47313  sigaradd  47323  sqrtnegnre  47784  quad1  48125  requad01  48126  requad1  48127  requad2  48128  oexpnegALTV  48182  oexpnegnz  48183  2zrngagrp  48754  altgsumbc  48857  dignn0flhalflem1  49120  line2ylem  49256  itschlc0yqe  49265  itsclc0yqsol  49269  itschlc0xyqsol  49272  amgmwlem  50306