Theorem negcld 11492

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  -cneg 11378

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379  df-neg 11380

This theorem is referenced by:  negcon1ad  11500  mulsubaddmulsub  11614  recextlem1  11780  mul2lt0rlt0  13046  xov1plusxeqvd  13451  ceim1l  13806  modnegd  13888  expaddzlem  14067  cjreb  15085  sqrtneg  15229  max0add  15272  reusq0  15427  iseraltlem2  15645  iseraltlem3  15646  fsumsub  15750  telfsumo2  15766  incexc  15802  incexc2  15803  fallrisefac  15990  binomrisefac  16007  efne0d  16062  efi4p  16104  oexpneg  16314  bitscmp  16407  bitsf1  16415  pcadd2  16861  gznegcl  16906  mulgdirlem  19081  mulgdir  19082  znunit  21543  cphsqrtcl2  25153  pjthlem1  25404  mbfsub  25629  iblcnlem1  25755  itgcnlem  25757  iblneg  25770  itgneg  25771  iblsub  25789  itgsub  25793  ditgcl  25825  dvrec  25922  dvmptsub  25934  dvrecg  25940  dvmptdiv  25941  dvsincos  25948  rolle  25957  vieta1lem2  26277  vieta1  26278  sinmpi  26451  cosmpi  26452  sinppi  26453  cosppi  26454  tanabsge  26470  efeq1  26492  tanord  26502  logtayl  26624  logtayl2  26626  logccv  26627  cxpneg  26645  cxpmul2z  26655  logreclem  26726  cosangneg2d  26771  isosctrlem2  26783  isosctrlem3  26784  angpieqvdlem  26792  quad2  26803  dcubic1lem  26807  dcubic2  26808  dcubic  26810  mcubic  26811  dquartlem1  26815  dquartlem2  26816  dquart  26817  quartlem1  26821  quartlem2  26822  quartlem3  26823  quartlem4  26824  quart  26825  asinlem  26832  asinlem2  26833  asinneg  26850  sinasin  26853  cosasin  26868  atandmneg  26870  tanatan  26883  atandmtan  26884  atantan  26887  atantayl  26901  zetacvg  26978  dmgmaddnn0  26990  lgamgulmlem2  26993  lgamgulmlem4  26995  lgambdd  27000  lgamucov  27001  ftalem4  27039  ftalem5  27040  ftalem7  27042  basellem5  27048  chpdifbndlem1  27516  padicabvcxp  27595  brbtwn2  28974  ipasslem2  30903  pjhthlem1  31462  quad3d  32822  divnumden2  32889  archirngz  33250  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  constrfin  33890  constrnegcl  33907  iconstr  33910  constrremulcl  33911  2sqr3minply  33924  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  madjusmdetlem4  33974  circlemeth  34784  logdivsqrle  34794  poimirlem29  37970  dvtan  37991  itg2addnclem3  37994  iblsubnc  38002  itgsubnc  38003  itgmulc2nc  38009  ftc1anclem5  38018  ftc1anclem8  38021  dvasin  38025  areacirclem1  38029  lcmineqlem10  42477  lcmineqlem12  42479  posbezout  42539  redvmptabs  42792  dffltz  43067  3cubeslem3r  43119  pell1234qrreccl  43282  pell14qrdich  43297  rmxyneg  43348  acongsym  43404  jm2.26a  43428  jm2.26lem3  43429  expgrowth  44762  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  sineq0ALT  45363  fzisoeu  45733  fperiodmul  45737  isumneg  46032  climneg  46040  neglimc  46075  sublimc  46080  reclimc  46081  dvcosre  46340  dvcosax  46354  itgsin0pilem1  46378  itgsinexplem1  46382  itgsincmulx  46402  stoweidlem13  46441  stirlinglem5  46506  dirkertrigeqlem3  46528  fourierdlem30  46565  fourierdlem39  46574  fourierdlem40  46575  fourierdlem41  46576  fourierdlem43  46578  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem73  46607  fourierdlem78  46612  fourierdlem92  46626  fourierdlem101  46635  fourierdlem103  46637  fourierdlem111  46645  sqwvfoura  46656  fouriersw  46659  etransclem17  46679  etransclem18  46680  etransclem23  46685  etransclem46  46708  sigarms  47284  sigaradd  47294  sqrtnegnre  47755  quad1  48096  requad01  48097  requad1  48098  requad2  48099  oexpnegALTV  48153  oexpnegnz  48154  2zrngagrp  48725  altgsumbc  48828  dignn0flhalflem1  49091  line2ylem  49227  itschlc0yqe  49236  itsclc0yqsol  49240  itschlc0xyqsol  49243  amgmwlem  50277