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

Theorem elrege0 11566
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 9525 . 2  |-  0  e.  RR
2 elicopnf 11559 . 2  |-  ( 0  e.  RR  ->  ( A  e.  ( 0 [,) +oo )  <->  ( A  e.  RR  /\  0  <_  A ) ) )
31, 2ax-mp 5 1  |-  ( A  e.  ( 0 [,) +oo )  <->  ( A  e.  RR  /\  0  <_  A ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    e. wcel 1836   class class class wbr 4380  (class class class)co 6214   RRcr 9420   0cc0 9421   +oocpnf 9554    <_ cle 9558   [,)cico 11470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-i2m1 9489  ax-1ne0 9490  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-po 4727  df-so 4728  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-ico 11474
This theorem is referenced by:  rge0ssre  11567  0e0icopnf  11569  ge0addcl  11571  ge0mulcl  11572  fsumge0  13630  isabvd  17601  abvge0  17606  nmolb  21328  nmoge0  21332  nmoi  21339  icopnfcnv  21546  cphsqrtcl  21735  tchcph  21784  ovolfsf  21987  ovolmge0  21992  ovolunlem1a  22011  ovoliunlem1  22017  ovolicc2lem4  22035  ioombl1lem4  22075  uniioombllem2  22096  uniioombllem6  22101  0plef  22183  i1fpos  22217  mbfi1fseqlem1  22226  mbfi1fseqlem3  22228  mbfi1fseqlem4  22229  mbfi1fseqlem5  22230  mbfi1fseqlem6  22231  mbfi1flimlem  22233  itg2const  22251  itg2const2  22252  itg2mulclem  22257  itg2mulc  22258  itg2monolem1  22261  itg2mono  22264  itg2addlem  22269  itg2gt0  22271  itg2cnlem1  22272  itg2cnlem2  22273  itg2cn  22274  iblconst  22328  itgconst  22329  ibladdlem  22330  itgaddlem1  22333  iblabslem  22338  iblabs  22339  iblmulc2  22341  itgmulc2lem1  22342  bddmulibl  22349  itggt0  22352  itgcn  22353  dvge0  22511  dvle  22512  dvfsumrlim  22536  cxpcn3lem  23227  cxpcn3  23228  resqrtcn  23229  loglesqrt  23238  areaf  23427  areacl  23428  areage0  23429  rlimcnp3  23433  jensenlem2  23453  jensen  23454  amgmlem  23455  amgm  23456  dchrisumlem3  23812  dchrmusumlema  23814  dchrmusum2  23815  dchrvmasumlem2  23819  dchrvmasumiflem1  23822  dchrisum0lema  23835  dchrisum0lem1b  23836  dchrisum0lem1  23837  dchrisum0lem2  23839  axcontlem2  24410  axcontlem7  24415  axcontlem8  24416  axcontlem10  24418  rge0scvg  28116  esumpcvgval  28257  hasheuni  28264  esumcvg  28265  sibfof  28501  mbfposadd  30263  itg2addnclem2  30269  itg2addnclem3  30270  itg2addnc  30271  itg2gt0cn  30272  ibladdnclem  30273  itgaddnclem1  30275  iblabsnclem  30280  iblabsnc  30281  iblmulc2nc  30282  itgmulc2nclem1  30283  bddiblnc  30287  itggt0cn  30289  ftc1anclem3  30294  ftc1anclem4  30295  ftc1anclem5  30296  ftc1anclem6  30297  ftc1anclem7  30298  ftc1anclem8  30299  areacirclem2  30310  fprodge0  31798  nn0rp0  33359  digvalnn0  33455  nn0digval  33456  dignn0fr  33457  dig2nn1st  33461  digexp  33463
  Copyright terms: Public domain W3C validator