Theorem elrege0 13374

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5099  (class class class)co 7360  ℝcr 11029  0cc0 11030  +∞cpnf 11167   ≤ cle 11171  [,)cico 13267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087  ax-1cn 11088  ax-addrcl 11091  ax-rnegex 11101  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-ico 13271

This theorem is referenced by:  nn0rp0  13375  rge0ssre  13376  0e0icopnf  13378  ge0addcl  13380  ge0mulcl  13381  fsumge0  15722  fprodge0  15920  isabvd  20749  abvge0  20754  nmolb  24665  nmoge0  24669  nmoi  24676  icopnfcnv  24900  cphsqrtcl  25144  tcphcph  25197  cphsscph  25211  ovolfsf  25432  ovolmge0  25438  ovolunlem1a  25457  ovoliunlem1  25463  ovolicc2lem4  25481  ioombl1lem4  25522  uniioombllem2  25544  uniioombllem6  25549  0plef  25633  i1fpos  25667  mbfi1fseqlem1  25676  mbfi1fseqlem3  25678  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  mbfi1fseqlem6  25681  mbfi1flimlem  25683  itg2const  25701  itg2const2  25702  itg2mulclem  25707  itg2mulc  25708  itg2monolem1  25711  itg2mono  25714  itg2addlem  25719  itg2gt0  25721  itg2cnlem1  25722  itg2cnlem2  25723  itg2cn  25724  iblconst  25779  itgconst  25780  ibladdlem  25781  itgaddlem1  25784  iblabslem  25789  iblabs  25790  iblmulc2  25792  itgmulc2lem1  25793  bddmulibl  25800  bddiblnc  25803  itggt0  25805  itgcn  25806  dvge0  25971  dvle  25972  dvfsumrlim  25998  cxpcn3lem  26717  cxpcn3  26718  resqrtcn  26719  loglesqrt  26731  areaf  26931  areacl  26932  areage0  26933  rlimcnp3  26937  jensenlem2  26958  jensen  26959  amgmlem  26960  amgm  26961  dchrisumlem3  27462  dchrmusumlema  27464  dchrmusum2  27465  dchrvmasumlem2  27469  dchrvmasumiflem1  27472  dchrisum0lema  27485  dchrisum0lem1b  27486  dchrisum0lem1  27487  dchrisum0lem2  27489  axcontlem2  29021  axcontlem7  29026  axcontlem8  29027  axcontlem10  29029  rge0scvg  34087  esumpcvgval  34216  hasheuni  34223  esumcvg  34224  sibfof  34478  mbfposadd  37839  itg2addnclem2  37844  itg2addnclem3  37845  itg2addnc  37846  itg2gt0cn  37847  ibladdnclem  37848  itgaddnclem1  37850  iblabsnclem  37855  iblabsnc  37856  iblmulc2nc  37857  itgmulc2nclem1  37858  itggt0cn  37862  ftc1anclem3  37867  ftc1anclem4  37868  ftc1anclem5  37869  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anclem8  37872  areacirclem2  37881  sge0iunmptlemfi  46693  digvalnn0  48881  nn0digval  48882  dignn0fr  48883  dig2nn1st  48887  digexp  48889  2sphere  49031  itsclc0  49053  itsclc0b  49054