Theorem elrege0 13428

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 11213	. 2 ⊢ 0 ∈ ℝ
2		elicopnf 13419	. 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 5148  (class class class)co 7406  ℝcr 11106  0cc0 11107  +∞cpnf 11242   ≤ cle 11246  [,)cico 13323

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 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-addrcl 11168  ax-rnegex 11178  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182

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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-ico 13327

This theorem is referenced by:  nn0rp0  13429  rge0ssre  13430  0e0icopnf  13432  ge0addcl  13434  ge0mulcl  13435  fsumge0  15738  fprodge0  15934  isabvd  20421  abvge0  20426  nmolb  24226  nmoge0  24230  nmoi  24237  icopnfcnv  24450  cphsqrtcl  24693  tcphcph  24746  cphsscph  24760  ovolfsf  24980  ovolmge0  24986  ovolunlem1a  25005  ovoliunlem1  25011  ovolicc2lem4  25029  ioombl1lem4  25070  uniioombllem2  25092  uniioombllem6  25097  0plef  25181  i1fpos  25216  mbfi1fseqlem1  25225  mbfi1fseqlem3  25227  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  mbfi1flimlem  25232  itg2const  25250  itg2const2  25251  itg2mulclem  25256  itg2mulc  25257  itg2monolem1  25260  itg2mono  25263  itg2addlem  25268  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  itg2cn  25273  iblconst  25327  itgconst  25328  ibladdlem  25329  itgaddlem1  25332  iblabslem  25337  iblabs  25338  iblmulc2  25340  itgmulc2lem1  25341  bddmulibl  25348  bddiblnc  25351  itggt0  25353  itgcn  25354  dvge0  25515  dvle  25516  dvfsumrlim  25540  cxpcn3lem  26245  cxpcn3  26246  resqrtcn  26247  loglesqrt  26256  areaf  26456  areacl  26457  areage0  26458  rlimcnp3  26462  jensenlem2  26482  jensen  26483  amgmlem  26484  amgm  26485  dchrisumlem3  26984  dchrmusumlema  26986  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumiflem1  26994  dchrisum0lema  27007  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2  27011  axcontlem2  28213  axcontlem7  28218  axcontlem8  28219  axcontlem10  28221  rge0scvg  32918  esumpcvgval  33065  hasheuni  33072  esumcvg  33073  sibfof  33328  mbfposadd  36524  itg2addnclem2  36529  itg2addnclem3  36530  itg2addnc  36531  itg2gt0cn  36532  ibladdnclem  36533  itgaddnclem1  36535  iblabsnclem  36540  iblabsnc  36541  iblmulc2nc  36542  itgmulc2nclem1  36543  itggt0cn  36547  ftc1anclem3  36552  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  areacirclem2  36566  sge0iunmptlemfi  45116  digvalnn0  47239  nn0digval  47240  dignn0fr  47241  dig2nn1st  47245  digexp  47247  2sphere  47389  itsclc0  47411  itsclc0b  47412