Theorem elrege0 13382

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 11146	. 2 ⊢ 0 ∈ ℝ
2		elicopnf 13373	. 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 5100  (class class class)co 7368  ℝcr 11037  0cc0 11038  +∞cpnf 11175   ≤ cle 11179  [,)cico 13275

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-ico 13279

This theorem is referenced by:  nn0rp0  13383  rge0ssre  13384  0e0icopnf  13386  ge0addcl  13388  ge0mulcl  13389  fsumge0  15730  fprodge0  15928  isabvd  20757  abvge0  20762  nmolb  24673  nmoge0  24677  nmoi  24684  icopnfcnv  24908  cphsqrtcl  25152  tcphcph  25205  cphsscph  25219  ovolfsf  25440  ovolmge0  25446  ovolunlem1a  25465  ovoliunlem1  25471  ovolicc2lem4  25489  ioombl1lem4  25530  uniioombllem2  25552  uniioombllem6  25557  0plef  25641  i1fpos  25675  mbfi1fseqlem1  25684  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  mbfi1flimlem  25691  itg2const  25709  itg2const2  25710  itg2mulclem  25715  itg2mulc  25716  itg2monolem1  25719  itg2mono  25722  itg2addlem  25727  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  itg2cn  25732  iblconst  25787  itgconst  25788  ibladdlem  25789  itgaddlem1  25792  iblabslem  25797  iblabs  25798  iblmulc2  25800  itgmulc2lem1  25801  bddmulibl  25808  bddiblnc  25811  itggt0  25813  itgcn  25814  dvge0  25979  dvle  25980  dvfsumrlim  26006  cxpcn3lem  26725  cxpcn3  26726  resqrtcn  26727  loglesqrt  26739  areaf  26939  areacl  26940  areage0  26941  rlimcnp3  26945  jensenlem2  26966  jensen  26967  amgmlem  26968  amgm  26969  dchrisumlem3  27470  dchrmusumlema  27472  dchrmusum2  27473  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2  27497  axcontlem2  29050  axcontlem7  29055  axcontlem8  29056  axcontlem10  29058  rge0scvg  34127  esumpcvgval  34256  hasheuni  34263  esumcvg  34264  sibfof  34518  mbfposadd  37918  itg2addnclem2  37923  itg2addnclem3  37924  itg2addnc  37925  itg2gt0cn  37926  ibladdnclem  37927  itgaddnclem1  37929  iblabsnclem  37934  iblabsnc  37935  iblmulc2nc  37936  itgmulc2nclem1  37937  itggt0cn  37941  ftc1anclem3  37946  ftc1anclem4  37947  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anclem7  37950  ftc1anclem8  37951  areacirclem2  37960  sge0iunmptlemfi  46771  digvalnn0  48959  nn0digval  48960  dignn0fr  48961  dig2nn1st  48965  digexp  48967  2sphere  49109  itsclc0  49131  itsclc0b  49132