Theorem negcld 11583

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11125  -cneg 11469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275  df-sub 11470  df-neg 11471

This theorem is used by:  negcon1ad  11591  mulsubaddmulsub  11705  recextlem1  11871  mul2lt0rlt0  13148  xov1plusxeqvd  13553  ceim1l  13910  modnegd  13992  expaddzlem  14171  cjreb  15212  sqrtneg  15356  max0add  15399  reusq0  15554  iseraltlem2  15772  iseraltlem3  15773  fsumsub  15876  telfsumo2  15892  incexc  15928  incexc2  15929  fallrisefac  16116  binomrisefac  16132  efne0d  16187  efi4p  16229  oexpneg  16439  bitscmp  16532  bitsf1  16540  pcadd2  16986  gznegcl  17031  mulgdirlem  19232  mulgdir  19233  znunit  21780  cphsqrtcl2  25418  pjthlem1  25669  mbfsub  25894  iblcnlem1  26020  itgcnlem  26022  iblneg  26035  itgneg  26036  iblsub  26054  itgsub  26058  ditgcl  26090  dvrec  26187  dvmptsub  26199  dvrecg  26205  dvmptdiv  26206  dvsincos  26213  rolle  26222  vieta1lem2  26545  vieta1  26546  sinmpi  26725  cosmpi  26726  sinppi  26727  cosppi  26728  tanabsge  26744  efeq1  26766  tanord  26776  logtayl  26898  logtayl2  26900  logccv  26901  cxpneg  26919  cxpmul2z  26929  logreclem  27000  cosangneg2d  27045  isosctrlem2  27057  isosctrlem3  27058  angpieqvdlem  27066  quad2  27077  dcubic1lem  27081  dcubic2  27082  dcubic  27084  mcubic  27085  dquartlem1  27089  dquartlem2  27090  dquart  27091  quartlem1  27095  quartlem2  27096  quartlem3  27097  quartlem4  27098  quart  27099  asinlem  27106  asinlem2  27107  asinneg  27124  sinasin  27127  cosasin  27142  atandmneg  27144  tanatan  27157  atandmtan  27158  atantan  27161  atantayl  27175  zetacvg  27252  dmgmaddnn0  27264  lgamgulmlem2  27267  lgamgulmlem4  27269  lgambdd  27274  lgamucov  27275  ftalem4  27313  ftalem5  27314  ftalem7  27316  basellem5  27322  chpdifbndlem1  27790  padicabvcxp  27869  brbtwn2  29363  ipasslem2  31314  pjhthlem1  31873  quad3d  33222  divnumden2  33288  archirngz  33631  constrrtlc1  34244  constrrtcclem  34246  constrrtcc  34247  constrfin  34258  constrnegcl  34275  iconstr  34278  constrremulcl  34279  2sqr3minply  34292  cos9thpiminplylem1  34294  cos9thpiminplylem2  34295  madjusmdetlem4  34342  circlemeth  35150  logdivsqrle  35160  poimirlem29  38400  dvtan  38421  itg2addnclem3  38424  iblsubnc  38432  itgsubnc  38433  itgmulc2nc  38439  ftc1anclem5  38448  ftc1anclem8  38451  dvasin  38455  areacirclem1  38459  lcmineqlem10  42906  lcmineqlem12  42908  posbezout  42968  redvmptabs  43237  dffltz  43482  3cubeslem3r  43534  pell1234qrreccl  43697  pell14qrdich  43712  rmxyneg  43763  acongsym  43819  jm2.26a  43843  jm2.26lem3  43844  expgrowth  45161  binomcxplemdvbinom  45179  binomcxplemnotnn0  45182  sineq0ALT  45761  fzisoeu  46135  fperiodmul  46139  isumneg  46434  climneg  46442  neglimc  46477  sublimc  46482  reclimc  46483  dvcosre  46742  dvcosax  46756  itgsin0pilem1  46780  itgsinexplem1  46784  itgsincmulx  46804  stoweidlem13  46843  stirlinglem5  46908  dirkertrigeqlem3  46930  fourierdlem30  46967  fourierdlem39  46976  fourierdlem40  46977  fourierdlem41  46978  fourierdlem43  46980  fourierdlem47  46983  fourierdlem48  46984  fourierdlem49  46985  fourierdlem73  47009  fourierdlem78  47014  fourierdlem92  47028  fourierdlem101  47037  fourierdlem103  47039  fourierdlem111  47047  sqwvfoura  47058  fouriersw  47061  etransclem17  47081  etransclem18  47082  etransclem23  47087  etransclem46  47110  sigarms  47686  sigaradd  47696  sqrtnegnre  48197  quad1  48538  requad01  48539  requad1  48540  requad2  48541  oexpnegALTV  48595  oexpnegnz  48596  2zrngagrp  49166  altgsumbc  49284  dignn0flhalflem1  49547  line2ylem  49683  itschlc0yqe  49692  itsclc0yqsol  49696  itschlc0xyqsol  49699  dvsec  50691  dvcot  50693  amgmwlem  50822