Theorem elrege0 13401

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  (class class class)co 7361  ℝcr 11031  0cc0 11032  +∞cpnf 11170   ≤ cle 11174  [,)cico 13294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-addrcl 11093  ax-rnegex 11103  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-ico 13298

This theorem is referenced by:  nn0rp0  13402  rge0ssre  13403  0e0icopnf  13405  ge0addcl  13407  ge0mulcl  13408  fsumge0  15752  fprodge0  15952  isabvd  20783  abvge0  20788  nmolb  24695  nmoge0  24699  nmoi  24706  icopnfcnv  24922  cphsqrtcl  25164  tcphcph  25217  cphsscph  25231  ovolfsf  25451  ovolmge0  25457  ovolunlem1a  25476  ovoliunlem1  25482  ovolicc2lem4  25500  ioombl1lem4  25541  uniioombllem2  25563  uniioombllem6  25568  0plef  25652  i1fpos  25686  mbfi1fseqlem1  25695  mbfi1fseqlem3  25697  mbfi1fseqlem4  25698  mbfi1fseqlem5  25699  mbfi1fseqlem6  25700  mbfi1flimlem  25702  itg2const  25720  itg2const2  25721  itg2mulclem  25726  itg2mulc  25727  itg2monolem1  25730  itg2mono  25733  itg2addlem  25738  itg2gt0  25740  itg2cnlem1  25741  itg2cnlem2  25742  itg2cn  25743  iblconst  25798  itgconst  25799  ibladdlem  25800  itgaddlem1  25803  iblabslem  25808  iblabs  25809  iblmulc2  25811  itgmulc2lem1  25812  bddmulibl  25819  bddiblnc  25822  itggt0  25824  itgcn  25825  dvge0  25986  dvle  25987  dvfsumrlim  26011  cxpcn3lem  26727  cxpcn3  26728  resqrtcn  26729  loglesqrt  26741  areaf  26941  areacl  26942  areage0  26943  rlimcnp3  26947  jensenlem2  26968  jensen  26969  amgmlem  26970  amgm  26971  dchrisumlem3  27471  dchrmusumlema  27473  dchrmusum2  27474  dchrvmasumlem2  27478  dchrvmasumiflem1  27481  dchrisum0lema  27494  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2  27498  axcontlem2  29051  axcontlem7  29056  axcontlem8  29057  axcontlem10  29059  rge0scvg  34112  esumpcvgval  34241  hasheuni  34248  esumcvg  34249  sibfof  34503  mbfposadd  38005  itg2addnclem2  38010  itg2addnclem3  38011  itg2addnc  38012  itg2gt0cn  38013  ibladdnclem  38014  itgaddnclem1  38016  iblabsnclem  38021  iblabsnc  38022  iblmulc2nc  38023  itgmulc2nclem1  38024  itggt0cn  38028  ftc1anclem3  38033  ftc1anclem4  38034  ftc1anclem5  38035  ftc1anclem6  38036  ftc1anclem7  38037  ftc1anclem8  38038  areacirclem2  38047  sge0iunmptlemfi  46862  digvalnn0  49090  nn0digval  49091  dignn0fr  49092  dig2nn1st  49096  digexp  49098  2sphere  49240  itsclc0  49262  itsclc0b  49263