Theorem negcld 11680

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11222   -cneg 11566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-ltxr 11372  df-sub 11567  df-neg 11568

This theorem is used by:  negcon1ad  11688  mulsubaddmulsub  11804  recextlem1  11970  mul2lt0rlt0  13248  xov1plusxeqvd  13653  ceim1l  14011  modnegd  14093  expaddzlem  14272  cjreb  15316  sqrtneg  15460  max0add  15503  reusq0  15658  iseraltlem2  15876  iseraltlem3  15877  fsumsub  15980  telfsumo2  15996  incexc  16032  incexc2  16033  fallrisefac  16218  binomrisefac  16234  efne0d  16289  efi4p  16331  oexpneg  16541  bitscmp  16634  bitsf1  16642  pcadd2  17094  gznegcl  17139  mulgdirlem  19341  mulgdir  19342  znunit  21896  cphsqrtcl2  25534  pjthlem1  25785  mbfsub  26010  iblcnlem1  26135  itgcnlem  26137  iblneg  26150  itgneg  26151  iblsub  26169  itgsub  26173  ditgcl  26205  dvrec  26302  dvmptsub  26314  dvrecg  26320  dvmptdiv  26321  dvsincos  26328  rolle  26337  vieta1lem2  26661  vieta1  26662  sinmpi  26843  cosmpi  26844  sinppi  26845  cosppi  26846  tanabsge  26862  efeq1  26883  tanord  26893  logtayl  27015  logtayl2  27017  logccv  27018  cxpneg  27036  cxpmul2z  27046  logreclem  27117  cosangneg2d  27162  isosctrlem2  27174  isosctrlem3  27175  angpieqvdlem  27183  quad2  27194  dcubic1lem  27198  dcubic2  27199  dcubic  27201  mcubic  27202  dquartlem1  27206  dquartlem2  27207  dquart  27208  quartlem1  27212  quartlem2  27213  quartlem3  27214  quartlem4  27215  quart  27216  asinlem  27223  asinlem2  27224  asinneg  27241  sinasin  27244  cosasin  27259  atandmneg  27261  tanatan  27274  atandmtan  27275  atantan  27278  atantayl  27292  zetacvg  27369  dmgmaddnn0  27381  lgamgulmlem2  27384  lgamgulmlem4  27386  lgambdd  27391  lgamucov  27392  ftalem4  27430  ftalem5  27431  ftalem7  27433  basellem5  27439  chpdifbndlem1  27907  padicabvcxp  27986  brbtwn2  29510  ipasslem2  31461  pjhthlem1  32020  quad3d  33408  divnumden2  33474  archirngz  33817  constrrtlc1  34431  constrrtcclem  34433  constrrtcc  34434  constrfin  34445  constrnegcl  34462  iconstr  34465  constrremulcl  34466  2sqr3minply  34479  cos9thpiminplylem1  34481  cos9thpiminplylem2  34482  madjusmdetlem4  34529  circlemeth  35336  logdivsqrle  35346  poimirlem29  38758  dvtan  38779  itg2addnclem3  38782  iblsubnc  38790  itgsubnc  38791  itgmulc2nc  38797  ftc1anclem5  38806  ftc1anclem8  38809  dvasin  38813  areacirclem1  38817  lcmineqlem10  43279  lcmineqlem12  43281  posbezout  43341  redvmptabs  43602  dffltz  43861  3cubeslem3r  43888  pell1234qrreccl  44052  pell14qrdich  44067  rmxyneg  44118  acongsym  44174  jm2.26a  44198  jm2.26lem3  44199  expgrowth  45509  binomcxplemdvbinom  45527  binomcxplemnotnn0  45530  sineq0ALT  46108  fzisoeu  46519  fperiodmul  46523  isumneg  46817  climneg  46825  neglimc  46860  sublimc  46865  reclimc  46866  dvcosre  47125  dvcosax  47139  itgsin0pilem1  47163  itgsinexplem1  47167  itgsincmulx  47187  stoweidlem13  47226  stirlinglem5  47291  dirkertrigeqlem3  47313  fourierdlem30  47350  fourierdlem39  47359  fourierdlem40  47360  fourierdlem41  47361  fourierdlem43  47363  fourierdlem47  47366  fourierdlem48  47367  fourierdlem49  47368  fourierdlem73  47392  fourierdlem78  47397  fourierdlem92  47411  fourierdlem101  47420  fourierdlem103  47422  fourierdlem111  47430  sqwvfoura  47441  fouriersw  47444  etransclem17  47464  etransclem18  47465  etransclem23  47470  etransclem46  47493  sigarms  48069  sigaradd  48079  sqrtnegnre  48580  quad1  48921  requad01  48922  requad1  48923  requad2  48924  oexpnegALTV  48978  oexpnegnz  48979  2zrngagrp  49549  altgsumbc  49667  dignn0flhalflem1  49930  line2ylem  50066  itschlc0yqe  50075  itsclc0yqsol  50079  itschlc0xyqsol  50082  dvsec  51134  dvcot  51136  amgmwlem  51265