Theorem negcld 11554

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11104  -cneg 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442  df-neg 11443

This theorem is referenced by:  negcon1ad  11562  mulsubaddmulsub  11674  recextlem1  11840  mul2lt0rlt0  13072  xov1plusxeqvd  13471  ceim1l  13808  modnegd  13887  expaddzlem  14067  cjreb  15066  sqrtneg  15210  max0add  15253  reusq0  15405  iseraltlem2  15625  iseraltlem3  15626  fsumsub  15730  telfsumo2  15745  incexc  15779  incexc2  15780  fallrisefac  15965  binomrisefac  15982  efi4p  16076  oexpneg  16284  bitscmp  16375  bitsf1  16383  pcadd2  16819  gznegcl  16864  mulgdirlem  18979  mulgdir  18980  znunit  21110  cphsqrtcl2  24694  pjthlem1  24945  mbfsub  25170  iblcnlem1  25296  itgcnlem  25298  iblneg  25311  itgneg  25312  iblsub  25330  itgsub  25334  ditgcl  25366  dvrec  25463  dvmptsub  25475  dvrecg  25481  dvmptdiv  25482  dvsincos  25489  rolle  25498  vieta1lem2  25815  vieta1  25816  sinmpi  25988  cosmpi  25989  sinppi  25990  cosppi  25991  tanabsge  26007  efeq1  26028  tanord  26038  logtayl  26159  logtayl2  26161  logccv  26162  cxpneg  26180  cxpmul2z  26190  logreclem  26256  cosangneg2d  26301  isosctrlem2  26313  isosctrlem3  26314  angpieqvdlem  26322  quad2  26333  dcubic1lem  26337  dcubic2  26338  dcubic  26340  mcubic  26341  dquartlem1  26345  dquartlem2  26346  dquart  26347  quartlem1  26351  quartlem2  26352  quartlem3  26353  quartlem4  26354  quart  26355  asinlem  26362  asinlem2  26363  asinneg  26380  sinasin  26383  cosasin  26398  atandmneg  26400  tanatan  26413  atandmtan  26414  atantan  26417  atantayl  26431  zetacvg  26508  dmgmaddnn0  26520  lgamgulmlem2  26523  lgamgulmlem4  26525  lgambdd  26530  lgamucov  26531  ftalem4  26569  ftalem5  26570  ftalem7  26572  basellem5  26578  chpdifbndlem1  27045  padicabvcxp  27124  brbtwn2  28152  ipasslem2  30072  pjhthlem1  30631  divnumden2  32011  archirngz  32322  madjusmdetlem4  32798  circlemeth  33640  logdivsqrle  33650  poimirlem29  36505  dvtan  36526  itg2addnclem3  36529  iblsubnc  36537  itgsubnc  36538  itgmulc2nc  36544  ftc1anclem5  36553  ftc1anclem8  36556  dvasin  36560  areacirclem1  36564  lcmineqlem10  40891  lcmineqlem12  40893  dffltz  41372  3cubeslem3r  41410  pell1234qrreccl  41577  pell14qrdich  41592  rmxyneg  41644  acongsym  41700  jm2.26a  41724  jm2.26lem3  41725  expgrowth  43079  binomcxplemdvbinom  43097  binomcxplemnotnn0  43100  sineq0ALT  43683  fzisoeu  43996  fperiodmul  44000  isumneg  44304  climneg  44312  neglimc  44349  sublimc  44354  reclimc  44355  dvcosre  44614  dvcosax  44628  itgsin0pilem1  44652  itgsinexplem1  44656  itgsincmulx  44676  stoweidlem13  44715  stirlinglem5  44780  dirkertrigeqlem3  44802  fourierdlem30  44839  fourierdlem39  44848  fourierdlem40  44849  fourierdlem41  44850  fourierdlem43  44852  fourierdlem47  44855  fourierdlem48  44856  fourierdlem49  44857  fourierdlem73  44881  fourierdlem78  44886  fourierdlem92  44900  fourierdlem101  44909  fourierdlem103  44911  fourierdlem111  44919  sqwvfoura  44930  fouriersw  44933  etransclem17  44953  etransclem18  44954  etransclem23  44959  etransclem46  44982  sigarms  45558  sigaradd  45568  sqrtnegnre  46001  quad1  46274  requad01  46275  requad1  46276  requad2  46277  oexpnegALTV  46331  oexpnegnz  46332  2zrngagrp  46794  altgsumbc  46981  dignn0flhalflem1  47254  line2ylem  47390  itschlc0yqe  47399  itsclc0yqsol  47403  itschlc0xyqsol  47406  amgmwlem  47802