MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rge0ssre Structured version   Visualization version   GIF version

Theorem rge0ssre 12838
Description: Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
Assertion
Ref Expression
rge0ssre (0[,)+∞) ⊆ ℝ

Proof of Theorem rge0ssre
StepHypRef Expression
1 elrege0 12836 . . 3 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
21simplbi 501 . 2 (𝑥 ∈ (0[,)+∞) → 𝑥 ∈ ℝ)
32ssriv 3922 1 (0[,)+∞) ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  wss 3884   class class class wbr 5033  (class class class)co 7139  cr 10529  0cc0 10530  +∞cpnf 10665  cle 10669  [,)cico 12732
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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-addrcl 10591  ax-rnegex 10601  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605
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 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-so 5443  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-ico 12736
This theorem is referenced by:  fsumge0  15146  fprodge0  15343  abvf  19591  rege0subm  20151  rge0srg  20166  icopnfhmeo  23552  iccpnfcnv  23553  cphsqrtcl  23793  ovollb2lem  24096  ovollb2  24097  ovolunlem1a  24104  ovolunlem1  24105  ovoliunlem1  24110  ovolicc1  24124  ovolicc2lem4  24128  ovolre  24133  ioombl1lem2  24167  ioombl1lem4  24169  uniioombllem1  24189  uniioombllem2  24191  uniioombllem3  24193  uniioombllem6  24196  0plef  24280  mbfi1fseqlem3  24325  mbfi1fseqlem4  24326  mbfi1fseqlem5  24327  itg2mulclem  24354  itg2mulc  24355  itg2monolem1  24358  itg2mono  24361  itg2i1fseq  24363  itg2gt0  24368  itg2cnlem1  24369  itg2cnlem2  24370  cxpcn3  25341  rlimcnp  25555  efrlim  25559  jensenlem1  25576  jensenlem2  25577  jensen  25578  amgm  25580  axcontlem10  26771  ex-fpar  28251  xrge0adddir  30730  fsumrp0cl  30733  xrge0slmod  30972  xrge0iifcnv  31290  lmlimxrge0  31305  rge0scvg  31306  lmdvg  31310  esumfsupre  31444  esumpfinvallem  31447  esumpfinval  31448  esumpfinvalf  31449  esumpcvgval  31451  esumcvg  31459  sibfof  31712  sitgclg  31714  sitgaddlemb  31720  hgt750lemf  32038  hgt750leme  32043  tgoldbachgtde  32045  itg2addnclem2  35108  itg2addnclem3  35109  itg2gt0cn  35111  ftc1anclem3  35131  areacirclem2  35145  xralrple2  41983  ge0xrre  42165  fsumge0cl  42212  liminfresre  42418  fouriersw  42870  sge0rnre  43000  fge0iccre  43010  sge0sn  43015  sge0tsms  43016  sge0f1o  43018  sge0repnf  43022  sge0fsum  43023  sge0pr  43030  sge0ltfirp  43036  sge0resplit  43042  sge0le  43043  sge0split  43045  sge0iunmptlemre  43051  sge0isum  43063  sge0ad2en  43067  sge0isummpt2  43068  sge0xaddlem1  43069  sge0xaddlem2  43070  sge0gtfsumgt  43079  sge0uzfsumgt  43080  sge0seq  43082  sge0reuz  43083  sge0reuzb  43084  meassre  43113  meaiuninclem  43116  omessre  43146  omeiunltfirp  43155  carageniuncl  43159  hoidmvlelem1  43231  hoidmvlelem2  43232  hoidmvlelem3  43233  hoidmvlelem4  43234  hoidmvlelem5  43235  hspmbllem1  43262
  Copyright terms: Public domain W3C validator