Theorem elrege0 13480

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

Syntax hints:   ↔ wb 205   ∧ wa 394   ∈ wcel 2098   class class class wbr 5152  (class class class)co 7423  ℝcr 11153  0cc0 11154  +∞cpnf 11291   ≤ cle 11295  [,)cico 13375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-addrcl 11215  ax-rnegex 11225  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5579  df-po 5593  df-so 5594  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7426  df-oprab 7427  df-mpo 7428  df-er 8733  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-ico 13379

This theorem is referenced by:  nn0rp0  13481  rge0ssre  13482  0e0icopnf  13484  ge0addcl  13486  ge0mulcl  13487  fsumge0  15794  fprodge0  15990  isabvd  20740  abvge0  20745  nmolb  24717  nmoge0  24721  nmoi  24728  icopnfcnv  24950  cphsqrtcl  25195  tcphcph  25248  cphsscph  25262  ovolfsf  25483  ovolmge0  25489  ovolunlem1a  25508  ovoliunlem1  25514  ovolicc2lem4  25532  ioombl1lem4  25573  uniioombllem2  25595  uniioombllem6  25600  0plef  25684  i1fpos  25719  mbfi1fseqlem1  25728  mbfi1fseqlem3  25730  mbfi1fseqlem4  25731  mbfi1fseqlem5  25732  mbfi1fseqlem6  25733  mbfi1flimlem  25735  itg2const  25753  itg2const2  25754  itg2mulclem  25759  itg2mulc  25760  itg2monolem1  25763  itg2mono  25766  itg2addlem  25771  itg2gt0  25773  itg2cnlem1  25774  itg2cnlem2  25775  itg2cn  25776  iblconst  25830  itgconst  25831  ibladdlem  25832  itgaddlem1  25835  iblabslem  25840  iblabs  25841  iblmulc2  25843  itgmulc2lem1  25844  bddmulibl  25851  bddiblnc  25854  itggt0  25856  itgcn  25857  dvge0  26022  dvle  26023  dvfsumrlim  26049  cxpcn3lem  26767  cxpcn3  26768  resqrtcn  26769  loglesqrt  26781  areaf  26981  areacl  26982  areage0  26983  rlimcnp3  26987  jensenlem2  27008  jensen  27009  amgmlem  27010  amgm  27011  dchrisumlem3  27512  dchrmusumlema  27514  dchrmusum2  27515  dchrvmasumlem2  27519  dchrvmasumiflem1  27522  dchrisum0lema  27535  dchrisum0lem1b  27536  dchrisum0lem1  27537  dchrisum0lem2  27539  axcontlem2  28891  axcontlem7  28896  axcontlem8  28897  axcontlem10  28899  rge0scvg  33732  esumpcvgval  33879  hasheuni  33886  esumcvg  33887  sibfof  34142  mbfposadd  37328  itg2addnclem2  37333  itg2addnclem3  37334  itg2addnc  37335  itg2gt0cn  37336  ibladdnclem  37337  itgaddnclem1  37339  iblabsnclem  37344  iblabsnc  37345  iblmulc2nc  37346  itgmulc2nclem1  37347  itggt0cn  37351  ftc1anclem3  37356  ftc1anclem4  37357  ftc1anclem5  37358  ftc1anclem6  37359  ftc1anclem7  37360  ftc1anclem8  37361  areacirclem2  37370  sge0iunmptlemfi  45983  digvalnn0  47936  nn0digval  47937  dignn0fr  47938  dig2nn1st  47942  digexp  47944  2sphere  48086  itsclc0  48108  itsclc0b  48109