MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrege0 Unicode version

Theorem elrege0 10996
Description: The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
Assertion
Ref Expression
elrege0  |-  ( A  e.  ( 0 [,) 
+oo )  <->  ( A  e.  RR  /\  0  <_  A ) )

Proof of Theorem elrege0
StepHypRef Expression
1 0re 9080 . 2  |-  0  e.  RR
2 elicopnf 10989 . 2  |-  ( 0  e.  RR  ->  ( A  e.  ( 0 [,)  +oo )  <->  ( A  e.  RR  /\  0  <_  A ) ) )
31, 2ax-mp 8 1  |-  ( A  e.  ( 0 [,) 
+oo )  <->  ( A  e.  RR  /\  0  <_  A ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    e. wcel 1725   class class class wbr 4204  (class class class)co 6072   RRcr 8978   0cc0 8979    +oocpnf 9106    <_ cle 9110   [,)cico 10907
This theorem is referenced by:  ge0addcl  10998  ge0mulcl  10999  fsumge0  12562  isabvd  15896  abvge0  15901  rege0subm  16743  nmolb  18739  nmoge0  18743  nmoi  18750  icopnfcnv  18955  icopnfhmeo  18956  cphsqrcl  19135  tchcph  19182  ovolfsf  19356  ovolmge0  19361  ovolunlem1a  19380  ovoliunlem1  19386  ovolicc2lem4  19404  ioombl1lem4  19443  uniioombllem2  19463  uniioombllem6  19468  0plef  19552  i1fpos  19586  mbfi1fseqlem1  19595  mbfi1fseqlem3  19597  mbfi1fseqlem4  19598  mbfi1fseqlem5  19599  mbfi1fseqlem6  19600  mbfi1flimlem  19602  itg2const  19620  itg2const2  19621  itg2mulclem  19626  itg2mulc  19627  itg2monolem1  19630  itg2monolem2  19631  itg2monolem3  19632  itg2mono  19633  itg2i1fseqle  19634  itg2i1fseq3  19637  itg2addlem  19638  itg2gt0  19640  itg2cnlem1  19641  itg2cnlem2  19642  itg2cn  19643  iblconst  19697  itgconst  19698  ibladdlem  19699  itgaddlem1  19702  iblabslem  19707  iblabs  19708  iblmulc2  19710  itgmulc2lem1  19711  bddmulibl  19718  itggt0  19721  itgcn  19722  dvge0  19878  dvle  19879  dvfsumrlim  19903  cxpcn3lem  20619  cxpcn3  20620  resqrcn  20621  loglesqr  20630  areaf  20788  areacl  20789  areage0  20790  rlimcnp3  20794  efrlim  20796  jensenlem2  20814  jensen  20815  amgmlem  20816  amgm  20817  dchrisumlem3  21173  dchrmusumlema  21175  dchrmusum2  21176  dchrvmasumlem2  21180  dchrvmasumiflem1  21183  dchrisum0lema  21196  dchrisum0lem1b  21197  dchrisum0lem1  21198  dchrisum0lem2  21200  rge0scvg  24323  esumpcvgval  24456  hasheuni  24463  esumcvg  24464  sibfof  24642  axcontlem2  25852  axcontlem7  25857  axcontlem8  25858  axcontlem10  25860  mbfposadd  26200  itg2addnclem2  26203  itg2addnclem3  26204  itg2addnc  26205  itg2gt0cn  26206  ibladdnclem  26207  itgaddnclem1  26209  iblabsnclem  26214  iblabsnc  26215  iblmulc2nc  26216  itgmulc2nclem1  26217  bddiblnc  26221  itggt0cn  26223  areacirclem4  26230
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-cnex 9035  ax-resscn 9036  ax-1cn 9037  ax-icn 9038  ax-addcl 9039  ax-addrcl 9040  ax-mulcl 9041  ax-mulrcl 9042  ax-i2m1 9047  ax-1ne0 9048  ax-rnegex 9050  ax-rrecex 9051  ax-cnre 9052  ax-pre-lttri 9053  ax-pre-lttrn 9054
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-po 4495  df-so 4496  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-er 6896  df-en 7101  df-dom 7102  df-sdom 7103  df-pnf 9111  df-mnf 9112  df-xr 9113  df-ltxr 9114  df-le 9115  df-ico 10911
  Copyright terms: Public domain W3C validator