Theorem elrege0 13458

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	⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))

Proof of Theorem elrege0

Step	Hyp	Ref	Expression
1		0re 11183	. 2 ⊢ 0 ∈ ℝ
2		elicopnf 13449	. 2 ⊢ (0 ∈ ℝ → (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2142   class class class wbr 5100  (class class class)co 7396  ℝcr 11072  0cc0 11073  +∞cpnf 11213   ≤ cle 11217  [,)cico 13351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-addrcl 11134  ax-rnegex 11144  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-ico 13355

This theorem is referenced by:  nn0rp0  13459  rge0ssre  13460  0e0icopnf  13462  ge0addcl  13464  ge0mulcl  13465  fsumge0  15823  fprodge0  16023  isabvd  20861  abvge0  20866  nmolb  24777  nmoge0  24781  nmoi  24788  icopnfcnv  25004  cphsqrtcl  25246  tcphcph  25299  cphsscph  25313  ovolfsf  25533  ovolmge0  25539  ovolunlem1a  25558  ovoliunlem1  25564  ovolicc2lem4  25582  ioombl1lem4  25623  uniioombllem2  25645  uniioombllem6  25650  0plef  25734  i1fpos  25768  mbfi1fseqlem1  25777  mbfi1fseqlem3  25779  mbfi1fseqlem4  25780  mbfi1fseqlem5  25781  mbfi1fseqlem6  25782  mbfi1flimlem  25784  itg2const  25802  itg2const2  25803  itg2mulclem  25808  itg2mulc  25809  itg2monolem1  25812  itg2mono  25815  itg2addlem  25820  itg2gt0  25822  itg2cnlem1  25823  itg2cnlem2  25824  itg2cn  25825  iblconst  25880  itgconst  25881  ibladdlem  25882  itgaddlem1  25885  iblabslem  25890  iblabs  25891  iblmulc2  25893  itgmulc2lem1  25894  bddmulibl  25901  bddiblnc  25904  itggt0  25906  itgcn  25907  dvge0  26068  dvle  26069  dvfsumrlim  26093  cxpcn3lem  26812  cxpcn3  26813  resqrtcn  26814  loglesqrt  26826  areaf  27026  areacl  27027  areage0  27028  rlimcnp3  27032  jensenlem2  27052  jensen  27053  amgmlem  27054  amgm  27055  dchrisumlem3  27555  dchrmusumlema  27557  dchrmusum2  27558  dchrvmasumlem2  27562  dchrvmasumiflem1  27565  dchrisum0lema  27578  dchrisum0lem1b  27579  dchrisum0lem1  27580  dchrisum0lem2  27582  axcontlem2  29166  axcontlem7  29171  axcontlem8  29172  axcontlem10  29174  rge0scvg  34246  esumpcvgval  34375  hasheuni  34382  esumcvg  34383  sibfof  34637  mbfposadd  38166  itg2addnclem2  38171  itg2addnclem3  38172  itg2addnc  38173  itg2gt0cn  38174  ibladdnclem  38175  itgaddnclem1  38177  iblabsnclem  38182  iblabsnc  38183  iblmulc2nc  38184  itgmulc2nclem1  38185  itggt0cn  38189  ftc1anclem3  38194  ftc1anclem4  38195  ftc1anclem5  38196  ftc1anclem6  38197  ftc1anclem7  38198  ftc1anclem8  38199  areacirclem2  38208  sge0iunmptlemfi  46987  digvalnn0  49221  nn0digval  49222  dignn0fr  49223  dig2nn1st  49227  digexp  49229  2sphere  49371  itsclc0  49393  itsclc0b  49394