Theorem negcld 11493

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11038  -cneg 11379

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-ltxr 11185  df-sub 11380  df-neg 11381

This theorem is referenced by:  negcon1ad  11501  mulsubaddmulsub  11615  recextlem1  11781  mul2lt0rlt0  13023  xov1plusxeqvd  13428  ceim1l  13781  modnegd  13863  expaddzlem  14042  cjreb  15060  sqrtneg  15204  max0add  15247  reusq0  15402  iseraltlem2  15620  iseraltlem3  15621  fsumsub  15725  telfsumo2  15740  incexc  15774  incexc2  15775  fallrisefac  15962  binomrisefac  15979  efne0d  16034  efi4p  16076  oexpneg  16286  bitscmp  16379  bitsf1  16387  pcadd2  16832  gznegcl  16877  mulgdirlem  19052  mulgdir  19053  znunit  21535  cphsqrtcl2  25159  pjthlem1  25410  mbfsub  25636  iblcnlem1  25762  itgcnlem  25764  iblneg  25777  itgneg  25778  iblsub  25796  itgsub  25800  ditgcl  25832  dvrec  25932  dvmptsub  25944  dvrecg  25950  dvmptdiv  25951  dvsincos  25958  rolle  25967  vieta1lem2  26292  vieta1  26293  sinmpi  26469  cosmpi  26470  sinppi  26471  cosppi  26472  tanabsge  26488  efeq1  26510  tanord  26520  logtayl  26642  logtayl2  26644  logccv  26645  cxpneg  26663  cxpmul2z  26673  logreclem  26745  cosangneg2d  26790  isosctrlem2  26802  isosctrlem3  26803  angpieqvdlem  26811  quad2  26822  dcubic1lem  26826  dcubic2  26827  dcubic  26829  mcubic  26830  dquartlem1  26834  dquartlem2  26835  dquart  26836  quartlem1  26840  quartlem2  26841  quartlem3  26842  quartlem4  26843  quart  26844  asinlem  26851  asinlem2  26852  asinneg  26869  sinasin  26872  cosasin  26887  atandmneg  26889  tanatan  26902  atandmtan  26903  atantan  26906  atantayl  26920  zetacvg  26998  dmgmaddnn0  27010  lgamgulmlem2  27013  lgamgulmlem4  27015  lgambdd  27020  lgamucov  27021  ftalem4  27059  ftalem5  27060  ftalem7  27062  basellem5  27068  chpdifbndlem1  27537  padicabvcxp  27616  brbtwn2  28996  ipasslem2  30926  pjhthlem1  31485  quad3d  32846  divnumden2  32913  archirngz  33289  constrrtlc1  33916  constrrtcclem  33918  constrrtcc  33919  constrfin  33930  constrnegcl  33947  iconstr  33950  constrremulcl  33951  2sqr3minply  33964  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  madjusmdetlem4  34014  circlemeth  34824  logdivsqrle  34834  poimirlem29  37929  dvtan  37950  itg2addnclem3  37953  iblsubnc  37961  itgsubnc  37962  itgmulc2nc  37968  ftc1anclem5  37977  ftc1anclem8  37980  dvasin  37984  areacirclem1  37988  lcmineqlem10  42437  lcmineqlem12  42439  posbezout  42499  redvmptabs  42759  dffltz  43021  3cubeslem3r  43073  pell1234qrreccl  43240  pell14qrdich  43255  rmxyneg  43306  acongsym  43362  jm2.26a  43386  jm2.26lem3  43387  expgrowth  44720  binomcxplemdvbinom  44738  binomcxplemnotnn0  44741  sineq0ALT  45321  fzisoeu  45691  fperiodmul  45695  isumneg  45991  climneg  45999  neglimc  46034  sublimc  46039  reclimc  46040  dvcosre  46299  dvcosax  46313  itgsin0pilem1  46337  itgsinexplem1  46341  itgsincmulx  46361  stoweidlem13  46400  stirlinglem5  46465  dirkertrigeqlem3  46487  fourierdlem30  46524  fourierdlem39  46533  fourierdlem40  46534  fourierdlem41  46535  fourierdlem43  46537  fourierdlem47  46540  fourierdlem48  46541  fourierdlem49  46542  fourierdlem73  46566  fourierdlem78  46571  fourierdlem92  46585  fourierdlem101  46594  fourierdlem103  46596  fourierdlem111  46604  sqwvfoura  46615  fouriersw  46618  etransclem17  46638  etransclem18  46639  etransclem23  46644  etransclem46  46667  sigarms  47243  sigaradd  47253  sqrtnegnre  47696  quad1  48009  requad01  48010  requad1  48011  requad2  48012  oexpnegALTV  48066  oexpnegnz  48067  2zrngagrp  48638  altgsumbc  48741  dignn0flhalflem1  49004  line2ylem  49140  itschlc0yqe  49149  itsclc0yqsol  49153  itschlc0xyqsol  49156  amgmwlem  50190