Theorem negcld 10978

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℂcc 10529  -cneg 10865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-po 5469  df-so 5470  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-ltxr 10674  df-sub 10866  df-neg 10867

This theorem is referenced by:  negcon1ad  10986  mulsubaddmulsub  11098  recextlem1  11264  mul2lt0rlt0  12485  xov1plusxeqvd  12878  ceim1l  13209  modnegd  13288  expaddzlem  13466  cjreb  14476  sqrtneg  14621  max0add  14664  reusq0  14816  iseraltlem2  15033  iseraltlem3  15034  fsumsub  15137  telfsumo2  15152  incexc  15186  incexc2  15187  fallrisefac  15373  binomrisefac  15390  efi4p  15484  oexpneg  15688  bitscmp  15781  bitsf1  15789  pcadd2  16220  gznegcl  16265  mulgdirlem  18252  mulgdir  18253  znunit  20704  cphsqrtcl2  23784  pjthlem1  24034  mbfsub  24257  iblcnlem1  24382  itgcnlem  24384  iblneg  24397  itgneg  24398  iblsub  24416  itgsub  24420  ditgcl  24450  dvrec  24546  dvmptsub  24558  dvrecg  24564  dvmptdiv  24565  dvsincos  24572  rolle  24581  vieta1lem2  24894  vieta1  24895  sinmpi  25067  cosmpi  25068  sinppi  25069  cosppi  25070  tanabsge  25086  efeq1  25107  tanord  25116  logtayl  25237  logtayl2  25239  logccv  25240  cxpneg  25258  cxpmul2z  25268  logreclem  25334  cosangneg2d  25379  isosctrlem2  25391  isosctrlem3  25392  angpieqvdlem  25400  quad2  25411  dcubic1lem  25415  dcubic2  25416  dcubic  25418  mcubic  25419  dquartlem1  25423  dquartlem2  25424  dquart  25425  quartlem1  25429  quartlem2  25430  quartlem3  25431  quartlem4  25432  quart  25433  asinlem  25440  asinlem2  25441  asinneg  25458  sinasin  25461  cosasin  25476  atandmneg  25478  tanatan  25491  atandmtan  25492  atantan  25495  atantayl  25509  zetacvg  25586  dmgmaddnn0  25598  lgamgulmlem2  25601  lgamgulmlem4  25603  lgambdd  25608  lgamucov  25609  ftalem4  25647  ftalem5  25648  ftalem7  25650  basellem5  25656  chpdifbndlem1  26123  padicabvcxp  26202  brbtwn2  26685  ipasslem2  28603  pjhthlem1  29162  divnumden2  30528  archirngz  30813  madjusmdetlem4  31090  circlemeth  31906  logdivsqrle  31916  poimirlem29  34915  dvtan  34936  itg2addnclem3  34939  iblsubnc  34947  itgsubnc  34948  itgmulc2nc  34954  ftc1anclem5  34965  ftc1anclem8  34968  dvasin  34972  areacirclem1  34976  dffltz  39264  3cubeslem3r  39277  pell1234qrreccl  39444  pell14qrdich  39459  rmxyneg  39510  acongsym  39566  jm2.26a  39590  jm2.26lem3  39591  expgrowth  40660  binomcxplemdvbinom  40678  binomcxplemnotnn0  40681  sineq0ALT  41264  fzisoeu  41559  fperiodmul  41563  isumneg  41875  climneg  41883  neglimc  41920  sublimc  41925  reclimc  41926  dvcosre  42188  dvcosax  42203  itgsin0pilem1  42227  itgsinexplem1  42231  itgsincmulx  42251  stoweidlem13  42291  stirlinglem5  42356  dirkertrigeqlem3  42378  fourierdlem30  42415  fourierdlem39  42424  fourierdlem40  42425  fourierdlem41  42426  fourierdlem43  42428  fourierdlem47  42431  fourierdlem48  42432  fourierdlem49  42433  fourierdlem73  42457  fourierdlem78  42462  fourierdlem92  42476  fourierdlem101  42485  fourierdlem103  42487  fourierdlem111  42495  sqwvfoura  42506  fouriersw  42509  etransclem17  42529  etransclem18  42530  etransclem23  42535  etransclem46  42558  sigarms  43106  sigaradd  43116  sqrtnegnre  43500  quad1  43778  requad01  43779  requad1  43780  requad2  43781  oexpnegALTV  43835  oexpnegnz  43836  2zrngagrp  44207  altgsumbc  44393  dignn0flhalflem1  44668  line2ylem  44731  itschlc0yqe  44740  itsclc0yqsol  44744  itschlc0xyqsol  44747  amgmwlem  44896