Theorem elrege0 13357

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  (class class class)co 7349  ℝcr 11008  0cc0 11009  +∞cpnf 11146   ≤ cle 11150  [,)cico 13250

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-addrcl 11070  ax-rnegex 11080  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-ico 13254

This theorem is referenced by:  nn0rp0  13358  rge0ssre  13359  0e0icopnf  13361  ge0addcl  13363  ge0mulcl  13364  fsumge0  15702  fprodge0  15900  isabvd  20697  abvge0  20702  nmolb  24603  nmoge0  24607  nmoi  24614  icopnfcnv  24838  cphsqrtcl  25082  tcphcph  25135  cphsscph  25149  ovolfsf  25370  ovolmge0  25376  ovolunlem1a  25395  ovoliunlem1  25401  ovolicc2lem4  25419  ioombl1lem4  25460  uniioombllem2  25482  uniioombllem6  25487  0plef  25571  i1fpos  25605  mbfi1fseqlem1  25614  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  mbfi1fseqlem6  25619  mbfi1flimlem  25621  itg2const  25639  itg2const2  25640  itg2mulclem  25645  itg2mulc  25646  itg2monolem1  25649  itg2mono  25652  itg2addlem  25657  itg2gt0  25659  itg2cnlem1  25660  itg2cnlem2  25661  itg2cn  25662  iblconst  25717  itgconst  25718  ibladdlem  25719  itgaddlem1  25722  iblabslem  25727  iblabs  25728  iblmulc2  25730  itgmulc2lem1  25731  bddmulibl  25738  bddiblnc  25741  itggt0  25743  itgcn  25744  dvge0  25909  dvle  25910  dvfsumrlim  25936  cxpcn3lem  26655  cxpcn3  26656  resqrtcn  26657  loglesqrt  26669  areaf  26869  areacl  26870  areage0  26871  rlimcnp3  26875  jensenlem2  26896  jensen  26897  amgmlem  26898  amgm  26899  dchrisumlem3  27400  dchrmusumlema  27402  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumiflem1  27410  dchrisum0lema  27423  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2  27427  axcontlem2  28910  axcontlem7  28915  axcontlem8  28916  axcontlem10  28918  rge0scvg  33916  esumpcvgval  34045  hasheuni  34052  esumcvg  34053  sibfof  34308  mbfposadd  37651  itg2addnclem2  37656  itg2addnclem3  37657  itg2addnc  37658  itg2gt0cn  37659  ibladdnclem  37660  itgaddnclem1  37662  iblabsnclem  37667  iblabsnc  37668  iblmulc2nc  37669  itgmulc2nclem1  37670  itggt0cn  37674  ftc1anclem3  37679  ftc1anclem4  37680  ftc1anclem5  37681  ftc1anclem6  37682  ftc1anclem7  37683  ftc1anclem8  37684  areacirclem2  37693  sge0iunmptlemfi  46398  digvalnn0  48588  nn0digval  48589  dignn0fr  48590  dig2nn1st  48594  digexp  48596  2sphere  48738  itsclc0  48760  itsclc0b  48761