Theorem negcld 11531

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

Syntax hints:   → wi 4   ∈ wcel 2144  ℂcc 11073  -cneg 11417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-po 5557  df-so 5558  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-ltxr 11223  df-sub 11418  df-neg 11419

This theorem is referenced by:  negcon1ad  11539  mulsubaddmulsub  11653  recextlem1  11819  mul2lt0rlt0  13099  xov1plusxeqvd  13504  ceim1l  13859  modnegd  13941  expaddzlem  14120  cjreb  15152  sqrtneg  15296  max0add  15339  reusq0  15494  iseraltlem2  15712  iseraltlem3  15713  fsumsub  15817  telfsumo2  15833  incexc  15869  incexc2  15870  fallrisefac  16057  binomrisefac  16074  efne0d  16129  efi4p  16171  oexpneg  16381  bitscmp  16474  bitsf1  16482  pcadd2  16928  gznegcl  16973  mulgdirlem  19149  mulgdir  19150  znunit  21617  cphsqrtcl2  25250  pjthlem1  25501  mbfsub  25726  iblcnlem1  25852  itgcnlem  25854  iblneg  25867  itgneg  25868  iblsub  25886  itgsub  25890  ditgcl  25922  dvrec  26019  dvmptsub  26031  dvrecg  26037  dvmptdiv  26038  dvsincos  26045  rolle  26054  vieta1lem2  26377  vieta1  26378  sinmpi  26554  cosmpi  26555  sinppi  26556  cosppi  26557  tanabsge  26573  efeq1  26595  tanord  26605  logtayl  26727  logtayl2  26729  logccv  26730  cxpneg  26748  cxpmul2z  26758  logreclem  26829  cosangneg2d  26874  isosctrlem2  26886  isosctrlem3  26887  angpieqvdlem  26895  quad2  26906  dcubic1lem  26910  dcubic2  26911  dcubic  26913  mcubic  26914  dquartlem1  26918  dquartlem2  26919  dquart  26920  quartlem1  26924  quartlem2  26925  quartlem3  26926  quartlem4  26927  quart  26928  asinlem  26935  asinlem2  26936  asinneg  26953  sinasin  26956  cosasin  26971  atandmneg  26973  tanatan  26986  atandmtan  26987  atantan  26990  atantayl  27004  zetacvg  27081  dmgmaddnn0  27093  lgamgulmlem2  27096  lgamgulmlem4  27098  lgambdd  27103  lgamucov  27104  ftalem4  27142  ftalem5  27143  ftalem7  27145  basellem5  27151  chpdifbndlem1  27619  padicabvcxp  27698  brbtwn2  29108  ipasslem2  31037  pjhthlem1  31596  quad3d  32953  divnumden2  33020  archirngz  33371  constrrtlc1  34031  constrrtcclem  34033  constrrtcc  34034  constrfin  34045  constrnegcl  34062  iconstr  34065  constrremulcl  34066  2sqr3minply  34079  cos9thpiminplylem1  34081  cos9thpiminplylem2  34082  madjusmdetlem4  34129  circlemeth  34936  logdivsqrle  34946  poimirlem29  38153  dvtan  38174  itg2addnclem3  38177  iblsubnc  38185  itgsubnc  38186  itgmulc2nc  38192  ftc1anclem5  38201  ftc1anclem8  38204  dvasin  38208  areacirclem1  38212  lcmineqlem10  42660  lcmineqlem12  42662  posbezout  42722  redvmptabs  42974  dffltz  43221  3cubeslem3r  43273  pell1234qrreccl  43436  pell14qrdich  43451  rmxyneg  43502  acongsym  43558  jm2.26a  43582  jm2.26lem3  43583  expgrowth  44916  binomcxplemdvbinom  44934  binomcxplemnotnn0  44937  sineq0ALT  45517  fzisoeu  45884  fperiodmul  45888  isumneg  46183  climneg  46191  neglimc  46226  sublimc  46231  reclimc  46232  dvcosre  46491  dvcosax  46505  itgsin0pilem1  46529  itgsinexplem1  46533  itgsincmulx  46553  stoweidlem13  46592  stirlinglem5  46657  dirkertrigeqlem3  46679  fourierdlem30  46716  fourierdlem39  46725  fourierdlem40  46726  fourierdlem41  46727  fourierdlem43  46729  fourierdlem47  46732  fourierdlem48  46733  fourierdlem49  46734  fourierdlem73  46758  fourierdlem78  46763  fourierdlem92  46777  fourierdlem101  46786  fourierdlem103  46788  fourierdlem111  46796  sqwvfoura  46807  fouriersw  46810  etransclem17  46830  etransclem18  46831  etransclem23  46836  etransclem46  46859  sigarms  47435  sigaradd  47445  sqrtnegnre  47906  quad1  48247  requad01  48248  requad1  48249  requad2  48250  oexpnegALTV  48304  oexpnegnz  48305  2zrngagrp  48876  altgsumbc  48979  dignn0flhalflem1  49242  line2ylem  49378  itschlc0yqe  49387  itsclc0yqsol  49391  itschlc0xyqsol  49394  amgmwlem  50428