Theorem elrege0 13115

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 10908	. 2 ⊢ 0 ∈ ℝ
2		elicopnf 13106	. 2 ⊢ (0 ∈ ℝ → (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  (class class class)co 7255  ℝcr 10801  0cc0 10802  +∞cpnf 10937   ≤ cle 10941  [,)cico 13010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-ico 13014

This theorem is referenced by:  nn0rp0  13116  rge0ssre  13117  0e0icopnf  13119  ge0addcl  13121  ge0mulcl  13122  fsumge0  15435  fprodge0  15631  isabvd  19995  abvge0  20000  nmolb  23787  nmoge0  23791  nmoi  23798  icopnfcnv  24011  cphsqrtcl  24253  tcphcph  24306  cphsscph  24320  ovolfsf  24540  ovolmge0  24546  ovolunlem1a  24565  ovoliunlem1  24571  ovolicc2lem4  24589  ioombl1lem4  24630  uniioombllem2  24652  uniioombllem6  24657  0plef  24741  i1fpos  24776  mbfi1fseqlem1  24785  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  mbfi1flimlem  24792  itg2const  24810  itg2const2  24811  itg2mulclem  24816  itg2mulc  24817  itg2monolem1  24820  itg2mono  24823  itg2addlem  24828  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  itg2cn  24833  iblconst  24887  itgconst  24888  ibladdlem  24889  itgaddlem1  24892  iblabslem  24897  iblabs  24898  iblmulc2  24900  itgmulc2lem1  24901  bddmulibl  24908  bddiblnc  24911  itggt0  24913  itgcn  24914  dvge0  25075  dvle  25076  dvfsumrlim  25100  cxpcn3lem  25805  cxpcn3  25806  resqrtcn  25807  loglesqrt  25816  areaf  26016  areacl  26017  areage0  26018  rlimcnp3  26022  jensenlem2  26042  jensen  26043  amgmlem  26044  amgm  26045  dchrisumlem3  26544  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2  26571  axcontlem2  27236  axcontlem7  27241  axcontlem8  27242  axcontlem10  27244  rge0scvg  31801  esumpcvgval  31946  hasheuni  31953  esumcvg  31954  sibfof  32207  mbfposadd  35751  itg2addnclem2  35756  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ibladdnclem  35760  itgaddnclem1  35762  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  itgmulc2nclem1  35770  itggt0cn  35774  ftc1anclem3  35779  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  areacirclem2  35793  sge0iunmptlemfi  43841  digvalnn0  45833  nn0digval  45834  dignn0fr  45835  dig2nn1st  45839  digexp  45841  2sphere  45983  itsclc0  46005  itsclc0b  46006