Theorem negcld 11656

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℂcc 11198   -cneg 11542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543  df-neg 11544

This theorem is used by:  negcon1ad  11664  mulsubaddmulsub  11780  recextlem1  11946  mul2lt0rlt0  13224  xov1plusxeqvd  13629  ceim1l  13987  modnegd  14069  expaddzlem  14248  cjreb  15290  sqrtneg  15434  max0add  15477  reusq0  15632  iseraltlem2  15850  iseraltlem3  15851  fsumsub  15954  telfsumo2  15970  incexc  16006  incexc2  16007  fallrisefac  16192  binomrisefac  16208  efne0d  16263  efi4p  16305  oexpneg  16515  bitscmp  16608  bitsf1  16616  pcadd2  17068  gznegcl  17113  mulgdirlem  19315  mulgdir  19316  znunit  21869  cphsqrtcl2  25507  pjthlem1  25758  mbfsub  25983  iblcnlem1  26108  itgcnlem  26110  iblneg  26123  itgneg  26124  iblsub  26142  itgsub  26146  ditgcl  26178  dvrec  26275  dvmptsub  26287  dvrecg  26293  dvmptdiv  26294  dvsincos  26301  rolle  26310  vieta1lem2  26634  vieta1  26635  sinmpi  26816  cosmpi  26817  sinppi  26818  cosppi  26819  tanabsge  26835  efeq1  26856  tanord  26866  logtayl  26988  logtayl2  26990  logccv  26991  cxpneg  27009  cxpmul2z  27019  logreclem  27090  cosangneg2d  27135  isosctrlem2  27147  isosctrlem3  27148  angpieqvdlem  27156  quad2  27167  dcubic1lem  27171  dcubic2  27172  dcubic  27174  mcubic  27175  dquartlem1  27179  dquartlem2  27180  dquart  27181  quartlem1  27185  quartlem2  27186  quartlem3  27187  quartlem4  27188  quart  27189  asinlem  27196  asinlem2  27197  asinneg  27214  sinasin  27217  cosasin  27232  atandmneg  27234  tanatan  27247  atandmtan  27248  atantan  27251  atantayl  27265  zetacvg  27342  dmgmaddnn0  27354  lgamgulmlem2  27357  lgamgulmlem4  27359  lgambdd  27364  lgamucov  27365  ftalem4  27403  ftalem5  27404  ftalem7  27406  basellem5  27412  chpdifbndlem1  27880  padicabvcxp  27959  brbtwn2  29483  ipasslem2  31434  pjhthlem1  31993  quad3d  33341  divnumden2  33407  archirngz  33750  constrrtlc1  34364  constrrtcclem  34366  constrrtcc  34367  constrfin  34378  constrnegcl  34395  iconstr  34398  constrremulcl  34399  2sqr3minply  34412  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  madjusmdetlem4  34462  circlemeth  35269  logdivsqrle  35279  poimirlem29  38568  dvtan  38589  itg2addnclem3  38592  iblsubnc  38600  itgsubnc  38601  itgmulc2nc  38607  ftc1anclem5  38616  ftc1anclem8  38619  dvasin  38623  areacirclem1  38627  lcmineqlem10  43089  lcmineqlem12  43091  posbezout  43151  redvmptabs  43412  dffltz  43671  3cubeslem3r  43698  pell1234qrreccl  43861  pell14qrdich  43876  rmxyneg  43927  acongsym  43983  jm2.26a  44007  jm2.26lem3  44008  expgrowth  45319  binomcxplemdvbinom  45337  binomcxplemnotnn0  45340  sineq0ALT  45919  fzisoeu  46316  fperiodmul  46320  isumneg  46614  climneg  46622  neglimc  46657  sublimc  46662  reclimc  46663  dvcosre  46922  dvcosax  46936  itgsin0pilem1  46960  itgsinexplem1  46964  itgsincmulx  46984  stoweidlem13  47023  stirlinglem5  47088  dirkertrigeqlem3  47110  fourierdlem30  47147  fourierdlem39  47156  fourierdlem40  47157  fourierdlem41  47158  fourierdlem43  47160  fourierdlem47  47163  fourierdlem48  47164  fourierdlem49  47165  fourierdlem73  47189  fourierdlem78  47194  fourierdlem92  47208  fourierdlem101  47217  fourierdlem103  47219  fourierdlem111  47227  sqwvfoura  47238  fouriersw  47241  etransclem17  47261  etransclem18  47262  etransclem23  47267  etransclem46  47290  sigarms  47866  sigaradd  47876  sqrtnegnre  48377  quad1  48718  requad01  48719  requad1  48720  requad2  48721  oexpnegALTV  48775  oexpnegnz  48776  2zrngagrp  49346  altgsumbc  49464  dignn0flhalflem1  49727  line2ylem  49863  itschlc0yqe  49872  itsclc0yqsol  49876  itschlc0xyqsol  49879  dvsec  50856  dvcot  50858  amgmwlem  50987