Theorem negcld 11581

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11127  -cneg 11467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-ltxr 11274  df-sub 11468  df-neg 11469

This theorem is referenced by:  negcon1ad  11589  mulsubaddmulsub  11701  recextlem1  11867  mul2lt0rlt0  13111  xov1plusxeqvd  13515  ceim1l  13864  modnegd  13944  expaddzlem  14123  cjreb  15142  sqrtneg  15286  max0add  15329  reusq0  15481  iseraltlem2  15699  iseraltlem3  15700  fsumsub  15804  telfsumo2  15819  incexc  15853  incexc2  15854  fallrisefac  16041  binomrisefac  16058  efne0d  16113  efi4p  16155  oexpneg  16364  bitscmp  16457  bitsf1  16465  pcadd2  16910  gznegcl  16955  mulgdirlem  19088  mulgdir  19089  znunit  21524  cphsqrtcl2  25138  pjthlem1  25389  mbfsub  25615  iblcnlem1  25741  itgcnlem  25743  iblneg  25756  itgneg  25757  iblsub  25775  itgsub  25779  ditgcl  25811  dvrec  25911  dvmptsub  25923  dvrecg  25929  dvmptdiv  25930  dvsincos  25937  rolle  25946  vieta1lem2  26271  vieta1  26272  sinmpi  26448  cosmpi  26449  sinppi  26450  cosppi  26451  tanabsge  26467  efeq1  26489  tanord  26499  logtayl  26621  logtayl2  26623  logccv  26624  cxpneg  26642  cxpmul2z  26652  logreclem  26724  cosangneg2d  26769  isosctrlem2  26781  isosctrlem3  26782  angpieqvdlem  26790  quad2  26801  dcubic1lem  26805  dcubic2  26806  dcubic  26808  mcubic  26809  dquartlem1  26813  dquartlem2  26814  dquart  26815  quartlem1  26819  quartlem2  26820  quartlem3  26821  quartlem4  26822  quart  26823  asinlem  26830  asinlem2  26831  asinneg  26848  sinasin  26851  cosasin  26866  atandmneg  26868  tanatan  26881  atandmtan  26882  atantan  26885  atantayl  26899  zetacvg  26977  dmgmaddnn0  26989  lgamgulmlem2  26992  lgamgulmlem4  26994  lgambdd  26999  lgamucov  27000  ftalem4  27038  ftalem5  27039  ftalem7  27041  basellem5  27047  chpdifbndlem1  27516  padicabvcxp  27595  brbtwn2  28884  ipasslem2  30813  pjhthlem1  31372  quad3d  32727  divnumden2  32794  archirngz  33187  constrrtlc1  33766  constrrtcclem  33768  constrrtcc  33769  constrfin  33780  constrnegcl  33797  iconstr  33800  constrremulcl  33801  2sqr3minply  33814  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  madjusmdetlem4  33861  circlemeth  34672  logdivsqrle  34682  poimirlem29  37673  dvtan  37694  itg2addnclem3  37697  iblsubnc  37705  itgsubnc  37706  itgmulc2nc  37712  ftc1anclem5  37721  ftc1anclem8  37724  dvasin  37728  areacirclem1  37732  lcmineqlem10  42051  lcmineqlem12  42053  posbezout  42113  redvmptabs  42403  dffltz  42657  3cubeslem3r  42710  pell1234qrreccl  42877  pell14qrdich  42892  rmxyneg  42944  acongsym  43000  jm2.26a  43024  jm2.26lem3  43025  expgrowth  44359  binomcxplemdvbinom  44377  binomcxplemnotnn0  44380  sineq0ALT  44961  fzisoeu  45329  fperiodmul  45333  isumneg  45631  climneg  45639  neglimc  45676  sublimc  45681  reclimc  45682  dvcosre  45941  dvcosax  45955  itgsin0pilem1  45979  itgsinexplem1  45983  itgsincmulx  46003  stoweidlem13  46042  stirlinglem5  46107  dirkertrigeqlem3  46129  fourierdlem30  46166  fourierdlem39  46175  fourierdlem40  46176  fourierdlem41  46177  fourierdlem43  46179  fourierdlem47  46182  fourierdlem48  46183  fourierdlem49  46184  fourierdlem73  46208  fourierdlem78  46213  fourierdlem92  46227  fourierdlem101  46236  fourierdlem103  46238  fourierdlem111  46246  sqwvfoura  46257  fouriersw  46260  etransclem17  46280  etransclem18  46281  etransclem23  46286  etransclem46  46309  sigarms  46885  sigaradd  46895  sqrtnegnre  47336  quad1  47634  requad01  47635  requad1  47636  requad2  47637  oexpnegALTV  47691  oexpnegnz  47692  2zrngagrp  48224  altgsumbc  48327  dignn0flhalflem1  48595  line2ylem  48731  itschlc0yqe  48740  itsclc0yqsol  48744  itschlc0xyqsol  48747  amgmwlem  49666