Theorem elrege0 13595

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146   class class class wbr 5105  (class class class)co 7427  ℝcr 11209  0cc0 11210  +∞cpnf 11350   ≤ cle 11354  [,)cico 13488

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267  ax-1cn 11268  ax-addrcl 11271  ax-rnegex 11281  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-po 5562  df-so 5563  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-er 8728  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-ico 13492

This theorem is used by:  nn0rp0  13596  rge0ssre  13597  0e0icopnf  13599  ge0addcl  13601  ge0mulcl  13602  fsumge0  15974  fprodge0  16172  isabvd  21081  abvge0  21086  nmolb  25048  nmoge0  25052  nmoi  25059  icopnfcnv  25275  cphsqrtcl  25517  tcphcph  25570  cphsscph  25584  ovolfsf  25804  ovolmge0  25810  ovolunlem1a  25829  ovoliunlem1  25835  ovolicc2lem4  25853  ioombl1lem4  25894  uniioombllem2  25916  uniioombllem6  25921  0plef  26005  i1fpos  26039  mbfi1fseqlem1  26048  mbfi1fseqlem3  26050  mbfi1fseqlem4  26051  mbfi1fseqlem5  26052  mbfi1fseqlem6  26053  mbfi1flimlem  26055  itg2const  26073  itg2const2  26074  itg2mulclem  26079  itg2mulc  26080  itg2monolem1  26083  itg2mono  26086  itg2addlem  26091  itg2gt0  26093  itg2cnlem1  26094  itg2cnlem2  26095  itg2cn  26096  iblconst  26150  itgconst  26151  ibladdlem  26152  itgaddlem1  26155  iblabslem  26160  iblabs  26161  iblmulc2  26163  itgmulc2lem1  26164  bddmulibl  26171  bddiblnc  26174  itggt0  26176  itgcn  26177  dvge0  26338  dvle  26339  dvfsumrlim  26363  cxpcn3lem  27087  cxpcn3  27088  resqrtcn  27089  loglesqrt  27101  areaf  27301  areacl  27302  areage0  27303  rlimcnp3  27307  jensenlem2  27327  jensen  27328  amgmlem  27329  amgm  27330  dchrisumlem3  27830  dchrmusumlema  27832  dchrmusum2  27833  dchrvmasumlem2  27837  dchrvmasumiflem1  27840  dchrisum0lema  27853  dchrisum0lem1b  27854  dchrisum0lem1  27855  dchrisum0lem2  27857  axcontlem2  29555  axcontlem7  29560  axcontlem8  29561  axcontlem10  29563  rge0scvg  34634  esumpcvgval  34763  hasheuni  34770  esumcvg  34771  sibfof  35025  mbfposadd  38725  itg2addnclem2  38730  itg2addnclem3  38731  itg2addnc  38732  itg2gt0cn  38733  ibladdnclem  38734  itgaddnclem1  38736  iblabsnclem  38741  iblabsnc  38742  iblmulc2nc  38743  itgmulc2nclem1  38744  itggt0cn  38748  ftc1anclem3  38753  ftc1anclem4  38754  ftc1anclem5  38755  ftc1anclem6  38756  ftc1anclem7  38757  ftc1anclem8  38758  areacirclem2  38767  sge0iunmptlemfi  47562  digvalnn0  49850  nn0digval  49851  dignn0fr  49852  dig2nn1st  49856  digexp  49858  2sphere  50000  itsclc0  50022  itsclc0b  50023