Theorem negcld 11607

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  -cneg 11493

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300  df-sub 11494  df-neg 11495

This theorem is referenced by:  negcon1ad  11615  mulsubaddmulsub  11727  recextlem1  11893  mul2lt0rlt0  13137  xov1plusxeqvd  13538  ceim1l  13887  modnegd  13967  expaddzlem  14146  cjreb  15162  sqrtneg  15306  max0add  15349  reusq0  15501  iseraltlem2  15719  iseraltlem3  15720  fsumsub  15824  telfsumo2  15839  incexc  15873  incexc2  15874  fallrisefac  16061  binomrisefac  16078  efi4p  16173  oexpneg  16382  bitscmp  16475  bitsf1  16483  pcadd2  16928  gznegcl  16973  mulgdirlem  19123  mulgdir  19124  znunit  21582  cphsqrtcl2  25220  pjthlem1  25471  mbfsub  25697  iblcnlem1  25823  itgcnlem  25825  iblneg  25838  itgneg  25839  iblsub  25857  itgsub  25861  ditgcl  25893  dvrec  25993  dvmptsub  26005  dvrecg  26011  dvmptdiv  26012  dvsincos  26019  rolle  26028  vieta1lem2  26353  vieta1  26354  sinmpi  26529  cosmpi  26530  sinppi  26531  cosppi  26532  tanabsge  26548  efeq1  26570  tanord  26580  logtayl  26702  logtayl2  26704  logccv  26705  cxpneg  26723  cxpmul2z  26733  logreclem  26805  cosangneg2d  26850  isosctrlem2  26862  isosctrlem3  26863  angpieqvdlem  26871  quad2  26882  dcubic1lem  26886  dcubic2  26887  dcubic  26889  mcubic  26890  dquartlem1  26894  dquartlem2  26895  dquart  26896  quartlem1  26900  quartlem2  26901  quartlem3  26902  quartlem4  26903  quart  26904  asinlem  26911  asinlem2  26912  asinneg  26929  sinasin  26932  cosasin  26947  atandmneg  26949  tanatan  26962  atandmtan  26963  atantan  26966  atantayl  26980  zetacvg  27058  dmgmaddnn0  27070  lgamgulmlem2  27073  lgamgulmlem4  27075  lgambdd  27080  lgamucov  27081  ftalem4  27119  ftalem5  27120  ftalem7  27122  basellem5  27128  chpdifbndlem1  27597  padicabvcxp  27676  brbtwn2  28920  ipasslem2  30851  pjhthlem1  31410  quad3d  32754  divnumden2  32817  archirngz  33196  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  constrfin  33787  2sqr3minply  33791  madjusmdetlem4  33829  circlemeth  34655  logdivsqrle  34665  poimirlem29  37656  dvtan  37677  itg2addnclem3  37680  iblsubnc  37688  itgsubnc  37689  itgmulc2nc  37695  ftc1anclem5  37704  ftc1anclem8  37707  dvasin  37711  areacirclem1  37715  lcmineqlem10  42039  lcmineqlem12  42041  posbezout  42101  efne0d  42373  redvmptabs  42390  dffltz  42644  3cubeslem3r  42698  pell1234qrreccl  42865  pell14qrdich  42880  rmxyneg  42932  acongsym  42988  jm2.26a  43012  jm2.26lem3  43013  expgrowth  44354  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  sineq0ALT  44957  fzisoeu  45312  fperiodmul  45316  isumneg  45617  climneg  45625  neglimc  45662  sublimc  45667  reclimc  45668  dvcosre  45927  dvcosax  45941  itgsin0pilem1  45965  itgsinexplem1  45969  itgsincmulx  45989  stoweidlem13  46028  stirlinglem5  46093  dirkertrigeqlem3  46115  fourierdlem30  46152  fourierdlem39  46161  fourierdlem40  46162  fourierdlem41  46163  fourierdlem43  46165  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem73  46194  fourierdlem78  46199  fourierdlem92  46213  fourierdlem101  46222  fourierdlem103  46224  fourierdlem111  46232  sqwvfoura  46243  fouriersw  46246  etransclem17  46266  etransclem18  46267  etransclem23  46272  etransclem46  46295  sigarms  46871  sigaradd  46881  sqrtnegnre  47319  quad1  47607  requad01  47608  requad1  47609  requad2  47610  oexpnegALTV  47664  oexpnegnz  47665  2zrngagrp  48165  altgsumbc  48268  dignn0flhalflem1  48536  line2ylem  48672  itschlc0yqe  48681  itsclc0yqsol  48685  itschlc0xyqsol  48688  amgmwlem  49321