Theorem elrege0 12278

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

Step	Hyp	Ref	Expression
1		0re 10040	. 2 |- 0 e. RR
2		elicopnf 12269	. 2 |- ( 0 e. RR -> ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) ) )
3	1, 2	ax-mp 5	1 |- ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )

Syntax hints:   <-> wb 196   /\ wa 384   e. wcel 1990   class class class wbr 4653  (class class class)co 6650   RRcr 9935   0cc0 9936   +oocpnf 10071   <_ cle 10075   [,)cico 12177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-ico 12181

This theorem is referenced by:  nn0rp0  12279  rge0ssre  12280  0e0icopnf  12282  ge0addcl  12284  ge0mulcl  12285  fsumge0  14527  fprodge0  14724  isabvd  18820  abvge0  18825  nmolb  22521  nmoge0  22525  nmoi  22532  icopnfcnv  22741  cphsqrtcl  22984  tchcph  23036  ovolfsf  23240  ovolmge0  23245  ovolunlem1a  23264  ovoliunlem1  23270  ovolicc2lem4  23288  ioombl1lem4  23329  uniioombllem2  23351  uniioombllem6  23356  0plef  23439  i1fpos  23473  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  mbfi1flimlem  23489  itg2const  23507  itg2const2  23508  itg2mulclem  23513  itg2mulc  23514  itg2monolem1  23517  itg2mono  23520  itg2addlem  23525  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  itg2cn  23530  iblconst  23584  itgconst  23585  ibladdlem  23586  itgaddlem1  23589  iblabslem  23594  iblabs  23595  iblmulc2  23597  itgmulc2lem1  23598  bddmulibl  23605  itggt0  23608  itgcn  23609  dvge0  23769  dvle  23770  dvfsumrlim  23794  cxpcn3lem  24488  cxpcn3  24489  resqrtcn  24490  loglesqrt  24499  areaf  24688  areacl  24689  areage0  24690  rlimcnp3  24694  jensenlem2  24714  jensen  24715  amgmlem  24716  amgm  24717  dchrisumlem3  25180  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2  25207  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  axcontlem10  25853  rge0scvg  29995  esumpcvgval  30140  hasheuni  30147  esumcvg  30148  sibfof  30402  mbfposadd  33457  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem1  33468  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nclem1  33476  bddiblnc  33480  itggt0cn  33482  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  areacirclem2  33501  sge0iunmptlemfi  40630  digvalnn0  42393  nn0digval  42394  dignn0fr  42395  dig2nn1st  42399  digexp  42401