Theorem negcld 11527

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  -cneg 11413

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  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 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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414  df-neg 11415

This theorem is referenced by:  negcon1ad  11535  mulsubaddmulsub  11649  recextlem1  11815  mul2lt0rlt0  13062  xov1plusxeqvd  13466  ceim1l  13816  modnegd  13898  expaddzlem  14077  cjreb  15096  sqrtneg  15240  max0add  15283  reusq0  15438  iseraltlem2  15656  iseraltlem3  15657  fsumsub  15761  telfsumo2  15776  incexc  15810  incexc2  15811  fallrisefac  15998  binomrisefac  16015  efne0d  16070  efi4p  16112  oexpneg  16322  bitscmp  16415  bitsf1  16423  pcadd2  16868  gznegcl  16913  mulgdirlem  19044  mulgdir  19045  znunit  21480  cphsqrtcl2  25093  pjthlem1  25344  mbfsub  25570  iblcnlem1  25696  itgcnlem  25698  iblneg  25711  itgneg  25712  iblsub  25730  itgsub  25734  ditgcl  25766  dvrec  25866  dvmptsub  25878  dvrecg  25884  dvmptdiv  25885  dvsincos  25892  rolle  25901  vieta1lem2  26226  vieta1  26227  sinmpi  26403  cosmpi  26404  sinppi  26405  cosppi  26406  tanabsge  26422  efeq1  26444  tanord  26454  logtayl  26576  logtayl2  26578  logccv  26579  cxpneg  26597  cxpmul2z  26607  logreclem  26679  cosangneg2d  26724  isosctrlem2  26736  isosctrlem3  26737  angpieqvdlem  26745  quad2  26756  dcubic1lem  26760  dcubic2  26761  dcubic  26763  mcubic  26764  dquartlem1  26768  dquartlem2  26769  dquart  26770  quartlem1  26774  quartlem2  26775  quartlem3  26776  quartlem4  26777  quart  26778  asinlem  26785  asinlem2  26786  asinneg  26803  sinasin  26806  cosasin  26821  atandmneg  26823  tanatan  26836  atandmtan  26837  atantan  26840  atantayl  26854  zetacvg  26932  dmgmaddnn0  26944  lgamgulmlem2  26947  lgamgulmlem4  26949  lgambdd  26954  lgamucov  26955  ftalem4  26993  ftalem5  26994  ftalem7  26996  basellem5  27002  chpdifbndlem1  27471  padicabvcxp  27550  brbtwn2  28839  ipasslem2  30768  pjhthlem1  31327  quad3d  32680  divnumden2  32747  archirngz  33150  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  constrfin  33743  constrnegcl  33760  iconstr  33763  constrremulcl  33764  2sqr3minply  33777  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  madjusmdetlem4  33827  circlemeth  34638  logdivsqrle  34648  poimirlem29  37650  dvtan  37671  itg2addnclem3  37674  iblsubnc  37682  itgsubnc  37683  itgmulc2nc  37689  ftc1anclem5  37698  ftc1anclem8  37701  dvasin  37705  areacirclem1  37709  lcmineqlem10  42033  lcmineqlem12  42035  posbezout  42095  redvmptabs  42355  dffltz  42629  3cubeslem3r  42682  pell1234qrreccl  42849  pell14qrdich  42864  rmxyneg  42916  acongsym  42972  jm2.26a  42996  jm2.26lem3  42997  expgrowth  44331  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  sineq0ALT  44933  fzisoeu  45305  fperiodmul  45309  isumneg  45607  climneg  45615  neglimc  45652  sublimc  45657  reclimc  45658  dvcosre  45917  dvcosax  45931  itgsin0pilem1  45955  itgsinexplem1  45959  itgsincmulx  45979  stoweidlem13  46018  stirlinglem5  46083  dirkertrigeqlem3  46105  fourierdlem30  46142  fourierdlem39  46151  fourierdlem40  46152  fourierdlem41  46153  fourierdlem43  46155  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem73  46184  fourierdlem78  46189  fourierdlem92  46203  fourierdlem101  46212  fourierdlem103  46214  fourierdlem111  46222  sqwvfoura  46233  fouriersw  46236  etransclem17  46256  etransclem18  46257  etransclem23  46262  etransclem46  46285  sigarms  46861  sigaradd  46871  sqrtnegnre  47312  quad1  47625  requad01  47626  requad1  47627  requad2  47628  oexpnegALTV  47682  oexpnegnz  47683  2zrngagrp  48241  altgsumbc  48344  dignn0flhalflem1  48608  line2ylem  48744  itschlc0yqe  48753  itsclc0yqsol  48757  itschlc0xyqsol  48760  amgmwlem  49795