Theorem elrege0 13354

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2111   class class class wbr 5089  (class class class)co 7346  ℝcr 11005  0cc0 11006  +∞cpnf 11143   ≤ cle 11147  [,)cico 13247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-addrcl 11067  ax-rnegex 11077  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-ico 13251

This theorem is referenced by:  nn0rp0  13355  rge0ssre  13356  0e0icopnf  13358  ge0addcl  13360  ge0mulcl  13361  fsumge0  15702  fprodge0  15900  isabvd  20727  abvge0  20732  nmolb  24632  nmoge0  24636  nmoi  24643  icopnfcnv  24867  cphsqrtcl  25111  tcphcph  25164  cphsscph  25178  ovolfsf  25399  ovolmge0  25405  ovolunlem1a  25424  ovoliunlem1  25430  ovolicc2lem4  25448  ioombl1lem4  25489  uniioombllem2  25511  uniioombllem6  25516  0plef  25600  i1fpos  25634  mbfi1fseqlem1  25643  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  mbfi1fseqlem6  25648  mbfi1flimlem  25650  itg2const  25668  itg2const2  25669  itg2mulclem  25674  itg2mulc  25675  itg2monolem1  25678  itg2mono  25681  itg2addlem  25686  itg2gt0  25688  itg2cnlem1  25689  itg2cnlem2  25690  itg2cn  25691  iblconst  25746  itgconst  25747  ibladdlem  25748  itgaddlem1  25751  iblabslem  25756  iblabs  25757  iblmulc2  25759  itgmulc2lem1  25760  bddmulibl  25767  bddiblnc  25770  itggt0  25772  itgcn  25773  dvge0  25938  dvle  25939  dvfsumrlim  25965  cxpcn3lem  26684  cxpcn3  26685  resqrtcn  26686  loglesqrt  26698  areaf  26898  areacl  26899  areage0  26900  rlimcnp3  26904  jensenlem2  26925  jensen  26926  amgmlem  26927  amgm  26928  dchrisumlem3  27429  dchrmusumlema  27431  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumiflem1  27439  dchrisum0lema  27452  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2  27456  axcontlem2  28943  axcontlem7  28948  axcontlem8  28949  axcontlem10  28951  rge0scvg  33962  esumpcvgval  34091  hasheuni  34098  esumcvg  34099  sibfof  34353  mbfposadd  37717  itg2addnclem2  37722  itg2addnclem3  37723  itg2addnc  37724  itg2gt0cn  37725  ibladdnclem  37726  itgaddnclem1  37728  iblabsnclem  37733  iblabsnc  37734  iblmulc2nc  37735  itgmulc2nclem1  37736  itggt0cn  37740  ftc1anclem3  37745  ftc1anclem4  37746  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  areacirclem2  37759  sge0iunmptlemfi  46521  digvalnn0  48710  nn0digval  48711  dignn0fr  48712  dig2nn1st  48716  digexp  48718  2sphere  48860  itsclc0  48882  itsclc0b  48883