Theorem renegcld 11056

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 10525  -cneg 10860

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-sub 10861  df-neg 10862

This theorem is referenced by:  ltord2  11158  leord2  11159  eqord2  11160  possumd  11254  recgt0  11475  riotaneg  11607  negiso  11608  nn0negleid  11937  difgtsumgt  11938  nnnegz  11972  prodge0rd  12484  modsub12d  13291  monoord2  13397  discr1  13596  discr  13597  recj  14475  reneg  14476  imcj  14483  imneg  14484  abslt  14666  absle  14667  o1lo1  14886  o1lo12  14887  icco1  14889  rlimrege0  14928  lo1sub  14979  iseraltlem2  15031  infcvgaux1i  15204  absefib  15543  efieq1re  15544  moddvds  15610  bitscmp  15777  bitsinv1lem  15780  mulgnegnn  18230  cnsubrg  20151  xrhmeo  23551  pjthlem1  24041  ivth2  24059  ovolshft  24115  shftmbl  24142  volsup2  24209  volivth  24211  mbfmulc2lem  24251  mbfposr  24256  mbfposb  24257  ismbf3d  24258  mbfmulc2  24267  mbfinf  24269  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  mbfi1fseqlem6  24324  mbfi1flimlem  24326  itg2monolem1  24354  iblposlem  24395  iblre  24397  itgreval  24400  itgneg  24407  i1fibl  24411  itgitg1  24412  itgle  24413  ibladd  24424  itgaddlem2  24427  iblabslem  24431  itgmulc2lem2  24436  itgmulc2  24437  bddiblnc  24445  dvferm2lem  24589  dvferm2  24590  rolle  24593  dvivth  24613  lhop2  24618  dvfsumge  24625  dvfsumlem2  24630  dvfsum2  24637  coseq0negpitopi  25096  tanabsge  25099  tanord  25130  tanregt0  25131  abslogimle  25165  logcj  25197  argimgt0  25203  logdiv2  25208  logcnlem3  25235  logccv  25254  abscxpbnd  25342  logreclem  25348  asinlem3a  25456  asinneg  25472  atanlogsublem  25501  atantan  25509  atans2  25517  birthdaylem3  25539  cxplim  25557  amgmlem  25575  emcllem7  25587  zetacvg  25600  eldmgm  25607  lgamgulmlem2  25615  lgsneg  25905  lgsdilem  25908  lgseisenlem1  25959  pntpbnd1  26170  pntibndlem2  26175  padicabvcxp  26216  ostth3  26222  axsegconlem9  26719  nvabs  28455  pjhthlem1  29174  xlt2addrd  30508  ccfldextdgrr  31145  xrge0iifcnv  31286  xrge0iifiso  31288  xrge0iifhom  31290  dya2ub  31638  sgnmul  31910  signsply0  31931  fdvneggt  31981  fdvnegge  31983  climlec3  33078  poimirlem29  35086  itg2gt0cn  35112  ibladdnc  35114  itgaddnclem2  35116  iblabsnclem  35120  itgmulc2nclem2  35124  itgmulc2nc  35125  ftc1anclem5  35134  dvasin  35141  areacirclem1  35145  areacirclem4  35148  areacirclem5  35149  areacirc  35150  oexpreposd  39487  3cubeslem4  39630  pellexlem6  39775  pell1234qrdich  39802  acongeq  39924  sqrtcval  40341  radcnvrat  41018  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  infnsuprnmpt  41888  neglt  41915  fperiodmul  41936  supsubc  41985  ltmulneg  42028  rexabslelem  42055  supminfrnmpt  42082  leneg2d  42086  leneg3d  42096  supminfxr  42103  climliminflimsupd  42443  liminfreuzlem  42444  liminfltlem  42446  stoweidlem1  42643  stoweidlem7  42649  stoweidlem13  42655  stoweidlem23  42665  stoweidlem34  42676  stoweidlem42  42684  stoweidlem47  42689  stirlinglem6  42721  stirlinglem10  42725  fourierdlem24  42773  fourierdlem39  42788  fourierdlem40  42789  fourierdlem43  42792  fourierdlem44  42793  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem58  42806  fourierdlem62  42810  fourierdlem72  42820  fourierdlem78  42826  fourierdlem83  42831  fourierdlem85  42833  fourierdlem88  42836  fourierdlem92  42840  fourierdlem97  42845  fourierdlem103  42851  fourierdlem104  42852  fourierdlem109  42857  fourierdlem111  42859  fourierdlem112  42860  sqwvfoura  42870  etransclem23  42899  etransclem46  42922  hoicvr  43187  hoicvrrex  43195  smfinflem  43448  smfliminflem  43461  sigaradd  43480  sqrtnegnre  43864  proththd  44132  requad01  44139  requad1  44140  requad2  44141  dignn0flhalflem1  45029  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  line2ylem  45165  itscnhlc0yqe  45173  itsclquadb  45190  itscnhlinecirc02p  45199  amgmwlem  45330