Theorem renegcld 11637

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 11105  -cneg 11441

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442  df-neg 11443

This theorem is referenced by:  ltord2  11739  leord2  11740  eqord2  11741  possumd  11835  recgt0  12056  riotaneg  12189  negiso  12190  nn0negleid  12520  difgtsumgt  12521  nnnegz  12557  prodge0rd  13077  modsub12d  13889  monoord2  13995  discr1  14198  discr  14199  recj  15067  reneg  15068  imcj  15075  imneg  15076  abslt  15257  absle  15258  o1lo1  15477  o1lo12  15478  icco1  15480  rlimrege0  15519  lo1sub  15571  iseraltlem2  15625  infcvgaux1i  15799  absefib  16137  efieq1re  16138  moddvds  16204  bitscmp  16375  bitsinv1lem  16378  mulgnegnn  18958  cnsubrg  20997  xrhmeo  24453  pjthlem1  24945  ivth2  24963  ovolshft  25019  shftmbl  25046  volsup2  25113  volivth  25115  mbfmulc2lem  25155  mbfposr  25160  mbfposb  25161  ismbf3d  25162  mbfmulc2  25171  mbfinf  25173  mbfi1fseqlem4  25227  mbfi1fseqlem5  25228  mbfi1fseqlem6  25229  mbfi1flimlem  25231  itg2monolem1  25259  iblposlem  25300  iblre  25302  itgreval  25305  itgneg  25312  i1fibl  25316  itgitg1  25317  itgle  25318  ibladd  25329  itgaddlem2  25332  iblabslem  25336  itgmulc2lem2  25341  itgmulc2  25342  bddiblnc  25350  dvferm2lem  25494  dvferm2  25495  rolle  25498  dvivth  25518  lhop2  25523  dvfsumge  25530  dvfsumlem2  25535  dvfsum2  25542  coseq0negpitopi  26004  tanabsge  26007  tanord  26038  tanregt0  26039  abslogimle  26073  logcj  26105  argimgt0  26111  logdiv2  26116  logcnlem3  26143  logccv  26162  abscxpbnd  26250  logreclem  26256  asinlem3a  26364  asinneg  26380  atanlogsublem  26409  atantan  26417  atans2  26425  birthdaylem3  26447  cxplim  26465  amgmlem  26483  emcllem7  26495  zetacvg  26508  eldmgm  26515  lgamgulmlem2  26523  lgsneg  26813  lgsdilem  26816  lgseisenlem1  26867  pntpbnd1  27078  pntibndlem2  27083  padicabvcxp  27124  ostth3  27130  axsegconlem9  28172  nvabs  29912  pjhthlem1  30631  xlt2addrd  31958  ccfldextdgrr  32734  xrge0iifcnv  32901  xrge0iifiso  32903  xrge0iifhom  32905  dya2ub  33257  sgnmul  33529  signsply0  33550  fdvneggt  33600  fdvnegge  33602  climlec3  34691  gg-dvfsumlem2  35171  poimirlem29  36505  itg2gt0cn  36531  ibladdnc  36533  itgaddnclem2  36535  iblabsnclem  36539  itgmulc2nclem2  36543  itgmulc2nc  36544  ftc1anclem5  36553  dvasin  36560  areacirclem1  36564  areacirclem4  36567  areacirclem5  36568  areacirc  36569  oexpreposd  41207  3cubeslem4  41412  pellexlem6  41557  pell1234qrdich  41584  acongeq  41707  sqrtcval  42377  radcnvrat  43058  binomcxplemdvbinom  43097  binomcxplemnotnn0  43100  infnsuprnmpt  43940  neglt  43980  fperiodmul  44000  supsubc  44049  ltmulneg  44088  rexabslelem  44114  supminfrnmpt  44141  leneg2d  44144  leneg3d  44153  supminfxr  44160  climliminflimsupd  44503  liminfreuzlem  44504  liminfltlem  44506  stoweidlem1  44703  stoweidlem7  44709  stoweidlem13  44715  stoweidlem23  44725  stoweidlem34  44736  stoweidlem42  44744  stoweidlem47  44749  stirlinglem6  44781  stirlinglem10  44785  fourierdlem24  44833  fourierdlem39  44848  fourierdlem40  44849  fourierdlem43  44852  fourierdlem44  44853  fourierdlem46  44854  fourierdlem48  44856  fourierdlem49  44857  fourierdlem58  44866  fourierdlem62  44870  fourierdlem72  44880  fourierdlem78  44886  fourierdlem83  44891  fourierdlem85  44893  fourierdlem88  44896  fourierdlem92  44900  fourierdlem97  44905  fourierdlem103  44911  fourierdlem104  44912  fourierdlem109  44917  fourierdlem111  44919  fourierdlem112  44920  sqwvfoura  44930  etransclem23  44959  etransclem46  44982  hoicvr  45250  hoicvrrex  45258  smfinflem  45519  smfliminflem  45532  finfdm  45548  smfinfdmmbllem  45550  sigaradd  45568  sqrtnegnre  46001  proththd  46268  requad01  46275  requad1  46276  requad2  46277  dignn0flhalflem1  47254  eenglngeehlnmlem1  47376  eenglngeehlnmlem2  47377  line2ylem  47390  itscnhlc0yqe  47398  itsclquadb  47415  itscnhlinecirc02p  47424  amgmwlem  47802