Theorem renegcld 11767

Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
renegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
renegcld	⊢ (𝜑 → -𝐴 ∈ ℝ)

Proof of Theorem renegcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		renegcl 11645	. 2 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → -𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11223   -cneg 11566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-ltxr 11372  df-sub 11567  df-neg 11568

This theorem is used by:  ltord2  11869  leord2  11870  eqord2  11871  possumd  11965  recgt0  12187  riotaneg  12320  negiso  12321  nn0negleid  12682  difgtsumgt  12683  nnnegz  12720  neglt  13164  prodge0rd  13253  modsub12d  14095  monoord2  14200  discr1  14407  discr  14408  sgnmul  15286  recj  15317  reneg  15318  imcj  15325  imneg  15326  abslt  15508  absle  15509  o1lo1  15730  o1lo12  15731  icco1  15733  rlimrege0  15772  lo1sub  15824  iseraltlem2  15876  infcvgaux1i  16052  absefib  16392  efieq1re  16393  moddvds  16459  bitscmp  16634  bitsinv1lem  16637  mulgnegnn  19320  cnsubrg  21760  xrhmeo  25294  pjthlem1  25785  ivth2  25803  ovolshft  25859  shftmbl  25886  volsup2  25953  volivth  25955  mbfmulc2lem  25995  mbfposr  26000  mbfposb  26001  ismbf3d  26002  mbfmulc2  26011  mbfinf  26013  mbfi1fseqlem4  26066  mbfi1fseqlem5  26067  mbfi1fseqlem6  26068  mbfi1flimlem  26070  itg2monolem1  26098  iblposlem  26139  iblre  26141  itgreval  26144  itgneg  26151  i1fibl  26155  itgitg1  26156  itgle  26157  ibladd  26168  itgaddlem2  26171  iblabslem  26175  itgmulc2lem2  26180  itgmulc2  26181  bddiblnc  26189  dvferm2lem  26333  dvferm2  26334  rolle  26337  dvivth  26357  lhop2  26362  dvfsumge  26369  dvfsumlem2  26374  dvfsum2  26381  coseq0negpitopi  26859  tanabsge  26862  tanord  26893  tanregt0  26894  abslogimle  26928  logcj  26961  argimgt0  26967  logdiv2  26972  logcnlem3  26999  logccv  27018  abscxpbnd  27108  logreclem  27117  asinlem3a  27225  asinneg  27241  atanlogsublem  27270  atantan  27278  atans2  27286  birthdaylem3  27308  cxplim  27326  amgmlem  27344  emcllem7  27356  zetacvg  27369  eldmgm  27376  lgamgulmlem2  27384  lgsneg  27675  lgsdilem  27678  lgseisenlem1  27729  pntpbnd1  27940  pntibndlem2  27945  padicabvcxp  27986  ostth3  27992  axsegconlem9  29530  nvabs  31301  pjhthlem1  32020  xlt2addrd  33418  expgt0b  33475  oexpled  33494  ccfldextdgrr  34371  constrnegcl  34462  iconstr  34465  constrremulcl  34466  constrmulcl  34470  constrresqrtcl  34476  cos9thpiminplylem1  34481  xrge0iifcnv  34632  xrge0iifiso  34634  xrge0iifhom  34636  dya2ub  34969  signsply0  35247  fdvneggt  35296  fdvnegge  35298  climlec3  36676  poimirlem29  38758  itg2gt0cn  38784  ibladdnc  38786  itgaddnclem2  38788  iblabsnclem  38792  itgmulc2nclem2  38796  itgmulc2nc  38797  ftc1anclem5  38806  dvasin  38813  areacirclem1  38817  areacirclem4  38820  areacirclem5  38821  areacirc  38822  posbezout  43341  bcle2d  43420  aks6d1c7lem1  43421  oexpreposd  43570  3cubeslem4  43890  pellexlem6  44032  pell1234qrdich  44059  acongeq  44181  sqrtcval  44831  radcnvrat  45488  binomcxplemdvbinom  45527  binomcxplemnotnn0  45530  infnsuprnmpt  46465  fperiodmul  46523  supsubc  46568  ltmulneg  46606  rexabslelem  46631  supminfrnmpt  46658  leneg2d  46661  leneg3d  46670  supminfxr  46677  climliminflimsupd  47014  liminfreuzlem  47015  liminfltlem  47017  stoweidlem1  47214  stoweidlem7  47220  stoweidlem13  47226  stoweidlem23  47236  stoweidlem34  47247  stoweidlem42  47255  stoweidlem47  47260  stirlinglem6  47292  stirlinglem10  47296  fourierdlem24  47344  fourierdlem39  47359  fourierdlem40  47360  fourierdlem43  47363  fourierdlem44  47364  fourierdlem46  47365  fourierdlem48  47367  fourierdlem49  47368  fourierdlem58  47377  fourierdlem62  47381  fourierdlem72  47391  fourierdlem78  47397  fourierdlem83  47402  fourierdlem85  47404  fourierdlem88  47407  fourierdlem92  47411  fourierdlem97  47416  fourierdlem103  47422  fourierdlem104  47423  fourierdlem109  47428  fourierdlem111  47430  fourierdlem112  47431  sqwvfoura  47441  etransclem23  47470  etransclem46  47493  hoicvr  47761  hoicvrrex  47769  smfinflem  48030  smfliminflem  48043  finfdm  48059  smfinfdmmbllem  48061  sigaradd  48079  squeezedltsq  48115  sqrtnegnre  48580  proththd  48902  requad01  48922  requad1  48923  requad2  48924  dignn0flhalflem1  49930  eenglngeehlnmlem1  50053  eenglngeehlnmlem2  50054  line2ylem  50066  itscnhlc0yqe  50074  itsclquadb  50091  itscnhlinecirc02p  50100  amgmwlem  51265