Theorem elrege0 13431

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∈ wcel 2107   class class class wbr 5149  (class class class)co 7409  ℝcr 11109  0cc0 11110  +∞cpnf 11245   ≤ cle 11249  [,)cico 13326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-addrcl 11171  ax-rnegex 11181  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-ico 13330

This theorem is referenced by:  nn0rp0  13432  rge0ssre  13433  0e0icopnf  13435  ge0addcl  13437  ge0mulcl  13438  fsumge0  15741  fprodge0  15937  isabvd  20428  abvge0  20433  nmolb  24234  nmoge0  24238  nmoi  24245  icopnfcnv  24458  cphsqrtcl  24701  tcphcph  24754  cphsscph  24768  ovolfsf  24988  ovolmge0  24994  ovolunlem1a  25013  ovoliunlem1  25019  ovolicc2lem4  25037  ioombl1lem4  25078  uniioombllem2  25100  uniioombllem6  25105  0plef  25189  i1fpos  25224  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  mbfi1flimlem  25240  itg2const  25258  itg2const2  25259  itg2mulclem  25264  itg2mulc  25265  itg2monolem1  25268  itg2mono  25271  itg2addlem  25276  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  itg2cn  25281  iblconst  25335  itgconst  25336  ibladdlem  25337  itgaddlem1  25340  iblabslem  25345  iblabs  25346  iblmulc2  25348  itgmulc2lem1  25349  bddmulibl  25356  bddiblnc  25359  itggt0  25361  itgcn  25362  dvge0  25523  dvle  25524  dvfsumrlim  25548  cxpcn3lem  26255  cxpcn3  26256  resqrtcn  26257  loglesqrt  26266  areaf  26466  areacl  26467  areage0  26468  rlimcnp3  26472  jensenlem2  26492  jensen  26493  amgmlem  26494  amgm  26495  dchrisumlem3  26994  dchrmusumlema  26996  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  dchrisum0lema  27017  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2  27021  axcontlem2  28223  axcontlem7  28228  axcontlem8  28229  axcontlem10  28231  rge0scvg  32929  esumpcvgval  33076  hasheuni  33083  esumcvg  33084  sibfof  33339  mbfposadd  36535  itg2addnclem2  36540  itg2addnclem3  36541  itg2addnc  36542  itg2gt0cn  36543  ibladdnclem  36544  itgaddnclem1  36546  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  itgmulc2nclem1  36554  itggt0cn  36558  ftc1anclem3  36563  ftc1anclem4  36564  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  areacirclem2  36577  sge0iunmptlemfi  45129  digvalnn0  47285  nn0digval  47286  dignn0fr  47287  dig2nn1st  47291  digexp  47293  2sphere  47435  itsclc0  47457  itsclc0b  47458