Theorem negcld 11604

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  -cneg 11490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491  df-neg 11492

This theorem is referenced by:  negcon1ad  11612  mulsubaddmulsub  11724  recextlem1  11890  mul2lt0rlt0  13134  xov1plusxeqvd  13534  ceim1l  13883  modnegd  13963  expaddzlem  14142  cjreb  15158  sqrtneg  15302  max0add  15345  reusq0  15497  iseraltlem2  15715  iseraltlem3  15716  fsumsub  15820  telfsumo2  15835  incexc  15869  incexc2  15870  fallrisefac  16057  binomrisefac  16074  efi4p  16169  oexpneg  16378  bitscmp  16471  bitsf1  16479  pcadd2  16923  gznegcl  16968  mulgdirlem  19135  mulgdir  19136  znunit  21599  cphsqrtcl2  25233  pjthlem1  25484  mbfsub  25710  iblcnlem1  25837  itgcnlem  25839  iblneg  25852  itgneg  25853  iblsub  25871  itgsub  25875  ditgcl  25907  dvrec  26007  dvmptsub  26019  dvrecg  26025  dvmptdiv  26026  dvsincos  26033  rolle  26042  vieta1lem2  26367  vieta1  26368  sinmpi  26543  cosmpi  26544  sinppi  26545  cosppi  26546  tanabsge  26562  efeq1  26584  tanord  26594  logtayl  26716  logtayl2  26718  logccv  26719  cxpneg  26737  cxpmul2z  26747  logreclem  26819  cosangneg2d  26864  isosctrlem2  26876  isosctrlem3  26877  angpieqvdlem  26885  quad2  26896  dcubic1lem  26900  dcubic2  26901  dcubic  26903  mcubic  26904  dquartlem1  26908  dquartlem2  26909  dquart  26910  quartlem1  26914  quartlem2  26915  quartlem3  26916  quartlem4  26917  quart  26918  asinlem  26925  asinlem2  26926  asinneg  26943  sinasin  26946  cosasin  26961  atandmneg  26963  tanatan  26976  atandmtan  26977  atantan  26980  atantayl  26994  zetacvg  27072  dmgmaddnn0  27084  lgamgulmlem2  27087  lgamgulmlem4  27089  lgambdd  27094  lgamucov  27095  ftalem4  27133  ftalem5  27134  ftalem7  27136  basellem5  27142  chpdifbndlem1  27611  padicabvcxp  27690  brbtwn2  28934  ipasslem2  30860  pjhthlem1  31419  quad3d  32760  divnumden2  32821  archirngz  33178  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  constrfin  33750  2sqr3minply  33752  madjusmdetlem4  33790  circlemeth  34633  logdivsqrle  34643  poimirlem29  37635  dvtan  37656  itg2addnclem3  37659  iblsubnc  37667  itgsubnc  37668  itgmulc2nc  37674  ftc1anclem5  37683  ftc1anclem8  37686  dvasin  37690  areacirclem1  37694  lcmineqlem10  42019  lcmineqlem12  42021  posbezout  42081  efne0d  42351  redvmptabs  42368  dffltz  42620  3cubeslem3r  42674  pell1234qrreccl  42841  pell14qrdich  42856  rmxyneg  42908  acongsym  42964  jm2.26a  42988  jm2.26lem3  42989  expgrowth  44330  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  sineq0ALT  44934  fzisoeu  45250  fperiodmul  45254  isumneg  45557  climneg  45565  neglimc  45602  sublimc  45607  reclimc  45608  dvcosre  45867  dvcosax  45881  itgsin0pilem1  45905  itgsinexplem1  45909  itgsincmulx  45929  stoweidlem13  45968  stirlinglem5  46033  dirkertrigeqlem3  46055  fourierdlem30  46092  fourierdlem39  46101  fourierdlem40  46102  fourierdlem41  46103  fourierdlem43  46105  fourierdlem47  46108  fourierdlem48  46109  fourierdlem49  46110  fourierdlem73  46134  fourierdlem78  46139  fourierdlem92  46153  fourierdlem101  46162  fourierdlem103  46164  fourierdlem111  46172  sqwvfoura  46183  fouriersw  46186  etransclem17  46206  etransclem18  46207  etransclem23  46212  etransclem46  46235  sigarms  46811  sigaradd  46821  sqrtnegnre  47256  quad1  47544  requad01  47545  requad1  47546  requad2  47547  oexpnegALTV  47601  oexpnegnz  47602  2zrngagrp  48092  altgsumbc  48196  dignn0flhalflem1  48464  line2ylem  48600  itschlc0yqe  48609  itsclc0yqsol  48613  itschlc0xyqsol  48616  amgmwlem  49032