Theorem negcld 11634

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  -cneg 11521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11522  df-neg 11523

This theorem is referenced by:  negcon1ad  11642  mulsubaddmulsub  11754  recextlem1  11920  mul2lt0rlt0  13159  xov1plusxeqvd  13558  ceim1l  13898  modnegd  13977  expaddzlem  14156  cjreb  15172  sqrtneg  15316  max0add  15359  reusq0  15511  iseraltlem2  15731  iseraltlem3  15732  fsumsub  15836  telfsumo2  15851  incexc  15885  incexc2  15886  fallrisefac  16073  binomrisefac  16090  efi4p  16185  oexpneg  16393  bitscmp  16484  bitsf1  16492  pcadd2  16937  gznegcl  16982  mulgdirlem  19145  mulgdir  19146  znunit  21605  cphsqrtcl2  25239  pjthlem1  25490  mbfsub  25716  iblcnlem1  25843  itgcnlem  25845  iblneg  25858  itgneg  25859  iblsub  25877  itgsub  25881  ditgcl  25913  dvrec  26013  dvmptsub  26025  dvrecg  26031  dvmptdiv  26032  dvsincos  26039  rolle  26048  vieta1lem2  26371  vieta1  26372  sinmpi  26547  cosmpi  26548  sinppi  26549  cosppi  26550  tanabsge  26566  efeq1  26588  tanord  26598  logtayl  26720  logtayl2  26722  logccv  26723  cxpneg  26741  cxpmul2z  26751  logreclem  26823  cosangneg2d  26868  isosctrlem2  26880  isosctrlem3  26881  angpieqvdlem  26889  quad2  26900  dcubic1lem  26904  dcubic2  26905  dcubic  26907  mcubic  26908  dquartlem1  26912  dquartlem2  26913  dquart  26914  quartlem1  26918  quartlem2  26919  quartlem3  26920  quartlem4  26921  quart  26922  asinlem  26929  asinlem2  26930  asinneg  26947  sinasin  26950  cosasin  26965  atandmneg  26967  tanatan  26980  atandmtan  26981  atantan  26984  atantayl  26998  zetacvg  27076  dmgmaddnn0  27088  lgamgulmlem2  27091  lgamgulmlem4  27093  lgambdd  27098  lgamucov  27099  ftalem4  27137  ftalem5  27138  ftalem7  27140  basellem5  27146  chpdifbndlem1  27615  padicabvcxp  27694  brbtwn2  28938  ipasslem2  30864  pjhthlem1  31423  quad3d  32757  divnumden2  32819  archirngz  33169  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  constrfin  33736  2sqr3minply  33738  madjusmdetlem4  33776  circlemeth  34617  logdivsqrle  34627  poimirlem29  37609  dvtan  37630  itg2addnclem3  37633  iblsubnc  37641  itgsubnc  37642  itgmulc2nc  37648  ftc1anclem5  37657  ftc1anclem8  37660  dvasin  37664  areacirclem1  37668  lcmineqlem10  41995  lcmineqlem12  41997  posbezout  42057  efne0d  42325  dffltz  42589  3cubeslem3r  42643  pell1234qrreccl  42810  pell14qrdich  42825  rmxyneg  42877  acongsym  42933  jm2.26a  42957  jm2.26lem3  42958  expgrowth  44304  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  sineq0ALT  44908  fzisoeu  45215  fperiodmul  45219  isumneg  45523  climneg  45531  neglimc  45568  sublimc  45573  reclimc  45574  dvcosre  45833  dvcosax  45847  itgsin0pilem1  45871  itgsinexplem1  45875  itgsincmulx  45895  stoweidlem13  45934  stirlinglem5  45999  dirkertrigeqlem3  46021  fourierdlem30  46058  fourierdlem39  46067  fourierdlem40  46068  fourierdlem41  46069  fourierdlem43  46071  fourierdlem47  46074  fourierdlem48  46075  fourierdlem49  46076  fourierdlem73  46100  fourierdlem78  46105  fourierdlem92  46119  fourierdlem101  46128  fourierdlem103  46130  fourierdlem111  46138  sqwvfoura  46149  fouriersw  46152  etransclem17  46172  etransclem18  46173  etransclem23  46178  etransclem46  46201  sigarms  46777  sigaradd  46787  sqrtnegnre  47222  quad1  47494  requad01  47495  requad1  47496  requad2  47497  oexpnegALTV  47551  oexpnegnz  47552  2zrngagrp  47972  altgsumbc  48077  dignn0flhalflem1  48349  line2ylem  48485  itschlc0yqe  48494  itsclc0yqsol  48498  itschlc0xyqsol  48501  amgmwlem  48896