Theorem renegcld 11687

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  -cneg 11490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491  df-neg 11492

This theorem is referenced by:  ltord2  11789  leord2  11790  eqord2  11791  possumd  11885  recgt0  12110  riotaneg  12244  negiso  12245  nn0negleid  12575  difgtsumgt  12576  nnnegz  12613  prodge0rd  13139  modsub12d  13965  monoord2  14070  discr1  14274  discr  14275  recj  15159  reneg  15160  imcj  15167  imneg  15168  abslt  15349  absle  15350  o1lo1  15569  o1lo12  15570  icco1  15572  rlimrege0  15611  lo1sub  15663  iseraltlem2  15715  infcvgaux1i  15889  absefib  16230  efieq1re  16231  moddvds  16297  bitscmp  16471  bitsinv1lem  16474  mulgnegnn  19114  cnsubrg  21462  xrhmeo  24990  pjthlem1  25484  ivth2  25503  ovolshft  25559  shftmbl  25586  volsup2  25653  volivth  25655  mbfmulc2lem  25695  mbfposr  25700  mbfposb  25701  ismbf3d  25702  mbfmulc2  25711  mbfinf  25713  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  mbfi1flimlem  25771  itg2monolem1  25799  iblposlem  25841  iblre  25843  itgreval  25846  itgneg  25853  i1fibl  25857  itgitg1  25858  itgle  25859  ibladd  25870  itgaddlem2  25873  iblabslem  25877  itgmulc2lem2  25882  itgmulc2  25883  bddiblnc  25891  dvferm2lem  26038  dvferm2  26039  rolle  26042  dvivth  26063  lhop2  26068  dvfsumge  26076  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsum2  26089  coseq0negpitopi  26559  tanabsge  26562  tanord  26594  tanregt0  26595  abslogimle  26629  logcj  26662  argimgt0  26668  logdiv2  26673  logcnlem3  26700  logccv  26719  abscxpbnd  26810  logreclem  26819  asinlem3a  26927  asinneg  26943  atanlogsublem  26972  atantan  26980  atans2  26988  birthdaylem3  27010  cxplim  27029  amgmlem  27047  emcllem7  27059  zetacvg  27072  eldmgm  27079  lgamgulmlem2  27087  lgsneg  27379  lgsdilem  27382  lgseisenlem1  27433  pntpbnd1  27644  pntibndlem2  27649  padicabvcxp  27690  ostth3  27696  axsegconlem9  28954  nvabs  30700  pjhthlem1  31419  xlt2addrd  32768  expgt0b  32822  ccfldextdgrr  33696  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  dya2ub  34251  sgnmul  34523  signsply0  34544  fdvneggt  34593  fdvnegge  34595  climlec3  35713  poimirlem29  37635  itg2gt0cn  37661  ibladdnc  37663  itgaddnclem2  37665  iblabsnclem  37669  itgmulc2nclem2  37673  itgmulc2nc  37674  ftc1anclem5  37683  dvasin  37690  areacirclem1  37694  areacirclem4  37697  areacirclem5  37698  areacirc  37699  posbezout  42081  bcle2d  42160  aks6d1c7lem1  42161  oexpreposd  42335  3cubeslem4  42676  pellexlem6  42821  pell1234qrdich  42848  acongeq  42971  sqrtcval  43630  radcnvrat  44309  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  infnsuprnmpt  45194  neglt  45234  fperiodmul  45254  supsubc  45302  ltmulneg  45341  rexabslelem  45367  supminfrnmpt  45394  leneg2d  45397  leneg3d  45406  supminfxr  45413  climliminflimsupd  45756  liminfreuzlem  45757  liminfltlem  45759  stoweidlem1  45956  stoweidlem7  45962  stoweidlem13  45968  stoweidlem23  45978  stoweidlem34  45989  stoweidlem42  45997  stoweidlem47  46002  stirlinglem6  46034  stirlinglem10  46038  fourierdlem24  46086  fourierdlem39  46101  fourierdlem40  46102  fourierdlem43  46105  fourierdlem44  46106  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem58  46119  fourierdlem62  46123  fourierdlem72  46133  fourierdlem78  46139  fourierdlem83  46144  fourierdlem85  46146  fourierdlem88  46149  fourierdlem92  46153  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem109  46170  fourierdlem111  46172  fourierdlem112  46173  sqwvfoura  46183  etransclem23  46212  etransclem46  46235  hoicvr  46503  hoicvrrex  46511  smfinflem  46772  smfliminflem  46785  finfdm  46801  smfinfdmmbllem  46803  sigaradd  46821  sqrtnegnre  47256  proththd  47538  requad01  47545  requad1  47546  requad2  47547  dignn0flhalflem1  48464  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  line2ylem  48600  itscnhlc0yqe  48608  itsclquadb  48625  itscnhlinecirc02p  48634  amgmwlem  49032