Theorem negcld 11496

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  -cneg 11382

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189  df-sub 11383  df-neg 11384

This theorem is referenced by:  negcon1ad  11504  mulsubaddmulsub  11618  recextlem1  11784  mul2lt0rlt0  13031  xov1plusxeqvd  13435  ceim1l  13785  modnegd  13867  expaddzlem  14046  cjreb  15065  sqrtneg  15209  max0add  15252  reusq0  15407  iseraltlem2  15625  iseraltlem3  15626  fsumsub  15730  telfsumo2  15745  incexc  15779  incexc2  15780  fallrisefac  15967  binomrisefac  15984  efne0d  16039  efi4p  16081  oexpneg  16291  bitscmp  16384  bitsf1  16392  pcadd2  16837  gznegcl  16882  mulgdirlem  19019  mulgdir  19020  znunit  21505  cphsqrtcl2  25119  pjthlem1  25370  mbfsub  25596  iblcnlem1  25722  itgcnlem  25724  iblneg  25737  itgneg  25738  iblsub  25756  itgsub  25760  ditgcl  25792  dvrec  25892  dvmptsub  25904  dvrecg  25910  dvmptdiv  25911  dvsincos  25918  rolle  25927  vieta1lem2  26252  vieta1  26253  sinmpi  26429  cosmpi  26430  sinppi  26431  cosppi  26432  tanabsge  26448  efeq1  26470  tanord  26480  logtayl  26602  logtayl2  26604  logccv  26605  cxpneg  26623  cxpmul2z  26633  logreclem  26705  cosangneg2d  26750  isosctrlem2  26762  isosctrlem3  26763  angpieqvdlem  26771  quad2  26782  dcubic1lem  26786  dcubic2  26787  dcubic  26789  mcubic  26790  dquartlem1  26794  dquartlem2  26795  dquart  26796  quartlem1  26800  quartlem2  26801  quartlem3  26802  quartlem4  26803  quart  26804  asinlem  26811  asinlem2  26812  asinneg  26829  sinasin  26832  cosasin  26847  atandmneg  26849  tanatan  26862  atandmtan  26863  atantan  26866  atantayl  26880  zetacvg  26958  dmgmaddnn0  26970  lgamgulmlem2  26973  lgamgulmlem4  26975  lgambdd  26980  lgamucov  26981  ftalem4  27019  ftalem5  27020  ftalem7  27022  basellem5  27028  chpdifbndlem1  27497  padicabvcxp  27576  brbtwn2  28885  ipasslem2  30811  pjhthlem1  31370  quad3d  32723  divnumden2  32790  archirngz  33158  constrrtlc1  33715  constrrtcclem  33717  constrrtcc  33718  constrfin  33729  constrnegcl  33746  iconstr  33749  constrremulcl  33750  2sqr3minply  33763  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  madjusmdetlem4  33813  circlemeth  34624  logdivsqrle  34634  poimirlem29  37636  dvtan  37657  itg2addnclem3  37660  iblsubnc  37668  itgsubnc  37669  itgmulc2nc  37675  ftc1anclem5  37684  ftc1anclem8  37687  dvasin  37691  areacirclem1  37695  lcmineqlem10  42019  lcmineqlem12  42021  posbezout  42081  redvmptabs  42341  dffltz  42615  3cubeslem3r  42668  pell1234qrreccl  42835  pell14qrdich  42850  rmxyneg  42902  acongsym  42958  jm2.26a  42982  jm2.26lem3  42983  expgrowth  44317  binomcxplemdvbinom  44335  binomcxplemnotnn0  44338  sineq0ALT  44919  fzisoeu  45291  fperiodmul  45295  isumneg  45593  climneg  45601  neglimc  45638  sublimc  45643  reclimc  45644  dvcosre  45903  dvcosax  45917  itgsin0pilem1  45941  itgsinexplem1  45945  itgsincmulx  45965  stoweidlem13  46004  stirlinglem5  46069  dirkertrigeqlem3  46091  fourierdlem30  46128  fourierdlem39  46137  fourierdlem40  46138  fourierdlem41  46139  fourierdlem43  46141  fourierdlem47  46144  fourierdlem48  46145  fourierdlem49  46146  fourierdlem73  46170  fourierdlem78  46175  fourierdlem92  46189  fourierdlem101  46198  fourierdlem103  46200  fourierdlem111  46208  sqwvfoura  46219  fouriersw  46222  etransclem17  46242  etransclem18  46243  etransclem23  46248  etransclem46  46271  sigarms  46847  sigaradd  46857  sqrtnegnre  47301  quad1  47614  requad01  47615  requad1  47616  requad2  47617  oexpnegALTV  47671  oexpnegnz  47672  2zrngagrp  48230  altgsumbc  48333  dignn0flhalflem1  48597  line2ylem  48733  itschlc0yqe  48742  itsclc0yqsol  48746  itschlc0xyqsol  48749  amgmwlem  49784