Theorem elrege0 13469

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119  (class class class)co 7403  ℝcr 11126  0cc0 11127  +∞cpnf 11264   ≤ cle 11268  [,)cico 13362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-addrcl 11188  ax-rnegex 11198  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  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 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-ico 13366

This theorem is referenced by:  nn0rp0  13470  rge0ssre  13471  0e0icopnf  13473  ge0addcl  13475  ge0mulcl  13476  fsumge0  15809  fprodge0  16007  isabvd  20770  abvge0  20775  nmolb  24654  nmoge0  24658  nmoi  24665  icopnfcnv  24889  cphsqrtcl  25134  tcphcph  25187  cphsscph  25201  ovolfsf  25422  ovolmge0  25428  ovolunlem1a  25447  ovoliunlem1  25453  ovolicc2lem4  25471  ioombl1lem4  25512  uniioombllem2  25534  uniioombllem6  25539  0plef  25623  i1fpos  25657  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  mbfi1flimlem  25673  itg2const  25691  itg2const2  25692  itg2mulclem  25697  itg2mulc  25698  itg2monolem1  25701  itg2mono  25704  itg2addlem  25709  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  itg2cn  25714  iblconst  25769  itgconst  25770  ibladdlem  25771  itgaddlem1  25774  iblabslem  25779  iblabs  25780  iblmulc2  25782  itgmulc2lem1  25783  bddmulibl  25790  bddiblnc  25793  itggt0  25795  itgcn  25796  dvge0  25961  dvle  25962  dvfsumrlim  25988  cxpcn3lem  26707  cxpcn3  26708  resqrtcn  26709  loglesqrt  26721  areaf  26921  areacl  26922  areage0  26923  rlimcnp3  26927  jensenlem2  26948  jensen  26949  amgmlem  26950  amgm  26951  dchrisumlem3  27452  dchrmusumlema  27454  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2  27479  axcontlem2  28890  axcontlem7  28895  axcontlem8  28896  axcontlem10  28898  rge0scvg  33926  esumpcvgval  34055  hasheuni  34062  esumcvg  34063  sibfof  34318  mbfposadd  37637  itg2addnclem2  37642  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  ibladdnclem  37646  itgaddnclem1  37648  iblabsnclem  37653  iblabsnc  37654  iblmulc2nc  37655  itgmulc2nclem1  37656  itggt0cn  37660  ftc1anclem3  37665  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  areacirclem2  37679  sge0iunmptlemfi  46390  digvalnn0  48527  nn0digval  48528  dignn0fr  48529  dig2nn1st  48533  digexp  48535  2sphere  48677  itsclc0  48699  itsclc0b  48700