Theorem renegcld 11568

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11029  -cneg 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-neg 11371

This theorem is referenced by:  ltord2  11670  leord2  11671  eqord2  11672  possumd  11766  recgt0  11991  riotaneg  12125  negiso  12126  nn0negleid  12457  difgtsumgt  12458  nnnegz  12495  neglt  12929  prodge0rd  13018  modsub12d  13855  monoord2  13960  discr1  14166  discr  14167  recj  15051  reneg  15052  imcj  15059  imneg  15060  abslt  15242  absle  15243  o1lo1  15464  o1lo12  15465  icco1  15467  rlimrege0  15506  lo1sub  15558  iseraltlem2  15610  infcvgaux1i  15784  absefib  16127  efieq1re  16128  moddvds  16194  bitscmp  16369  bitsinv1lem  16372  mulgnegnn  19018  cnsubrg  21386  xrhmeo  24904  pjthlem1  25397  ivth2  25416  ovolshft  25472  shftmbl  25499  volsup2  25566  volivth  25568  mbfmulc2lem  25608  mbfposr  25613  mbfposb  25614  ismbf3d  25615  mbfmulc2  25624  mbfinf  25626  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  mbfi1fseqlem6  25681  mbfi1flimlem  25683  itg2monolem1  25711  iblposlem  25753  iblre  25755  itgreval  25758  itgneg  25765  i1fibl  25769  itgitg1  25770  itgle  25771  ibladd  25782  itgaddlem2  25785  iblabslem  25789  itgmulc2lem2  25794  itgmulc2  25795  bddiblnc  25803  dvferm2lem  25950  dvferm2  25951  rolle  25954  dvivth  25975  lhop2  25980  dvfsumge  25988  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsum2  26001  coseq0negpitopi  26472  tanabsge  26475  tanord  26507  tanregt0  26508  abslogimle  26542  logcj  26575  argimgt0  26581  logdiv2  26586  logcnlem3  26613  logccv  26632  abscxpbnd  26723  logreclem  26732  asinlem3a  26840  asinneg  26856  atanlogsublem  26885  atantan  26893  atans2  26901  birthdaylem3  26923  cxplim  26942  amgmlem  26960  emcllem7  26972  zetacvg  26985  eldmgm  26992  lgamgulmlem2  27000  lgsneg  27292  lgsdilem  27295  lgseisenlem1  27346  pntpbnd1  27557  pntibndlem2  27562  padicabvcxp  27603  ostth3  27609  axsegconlem9  29002  nvabs  30751  pjhthlem1  31470  xlt2addrd  32841  expgt0b  32899  sgnmul  32918  oexpled  32930  ccfldextdgrr  33831  constrnegcl  33922  iconstr  33925  constrremulcl  33926  constrmulcl  33930  constrresqrtcl  33936  cos9thpiminplylem1  33941  xrge0iifcnv  34092  xrge0iifiso  34094  xrge0iifhom  34096  dya2ub  34429  signsply0  34710  fdvneggt  34759  fdvnegge  34761  climlec3  35930  poimirlem29  37852  itg2gt0cn  37878  ibladdnc  37880  itgaddnclem2  37882  iblabsnclem  37886  itgmulc2nclem2  37890  itgmulc2nc  37891  ftc1anclem5  37900  dvasin  37907  areacirclem1  37911  areacirclem4  37914  areacirclem5  37915  areacirc  37916  posbezout  42422  bcle2d  42501  aks6d1c7lem1  42502  oexpreposd  42644  3cubeslem4  42998  pellexlem6  43143  pell1234qrdich  43170  acongeq  43292  sqrtcval  43949  radcnvrat  44622  binomcxplemdvbinom  44661  binomcxplemnotnn0  44664  infnsuprnmpt  45561  fperiodmul  45619  supsubc  45665  ltmulneg  45703  rexabslelem  45729  supminfrnmpt  45756  leneg2d  45759  leneg3d  45768  supminfxr  45775  climliminflimsupd  46112  liminfreuzlem  46113  liminfltlem  46115  stoweidlem1  46312  stoweidlem7  46318  stoweidlem13  46324  stoweidlem23  46334  stoweidlem34  46345  stoweidlem42  46353  stoweidlem47  46358  stirlinglem6  46390  stirlinglem10  46394  fourierdlem24  46442  fourierdlem39  46457  fourierdlem40  46458  fourierdlem43  46461  fourierdlem44  46462  fourierdlem46  46463  fourierdlem48  46465  fourierdlem49  46466  fourierdlem58  46475  fourierdlem62  46479  fourierdlem72  46489  fourierdlem78  46495  fourierdlem83  46500  fourierdlem85  46502  fourierdlem88  46505  fourierdlem92  46509  fourierdlem97  46514  fourierdlem103  46520  fourierdlem104  46521  fourierdlem109  46526  fourierdlem111  46528  fourierdlem112  46529  sqwvfoura  46539  etransclem23  46568  etransclem46  46591  hoicvr  46859  hoicvrrex  46867  smfinflem  47128  smfliminflem  47141  finfdm  47157  smfinfdmmbllem  47159  sigaradd  47177  squeezedltsq  47199  sqrtnegnre  47620  proththd  47927  requad01  47934  requad1  47935  requad2  47936  dignn0flhalflem1  48928  eenglngeehlnmlem1  49050  eenglngeehlnmlem2  49051  line2ylem  49064  itscnhlc0yqe  49072  itsclquadb  49089  itscnhlinecirc02p  49098  amgmwlem  50114