Theorem elrege0 12834

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2108   class class class wbr 5057  (class class class)co 7148  ℝcr 10528  0cc0 10529  +∞cpnf 10664   ≤ cle 10668  [,)cico 12732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-addrcl 10590  ax-rnegex 10600  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-ico 12736

This theorem is referenced by:  nn0rp0  12835  rge0ssre  12836  0e0icopnf  12838  ge0addcl  12840  ge0mulcl  12841  fsumge0  15142  fprodge0  15339  isabvd  19583  abvge0  19588  nmolb  23318  nmoge0  23322  nmoi  23329  icopnfcnv  23538  cphsqrtcl  23780  tcphcph  23832  cphsscph  23846  ovolfsf  24064  ovolmge0  24070  ovolunlem1a  24089  ovoliunlem1  24095  ovolicc2lem4  24113  ioombl1lem4  24154  uniioombllem2  24176  uniioombllem6  24181  0plef  24265  i1fpos  24299  mbfi1fseqlem1  24308  mbfi1fseqlem3  24310  mbfi1fseqlem4  24311  mbfi1fseqlem5  24312  mbfi1fseqlem6  24313  mbfi1flimlem  24315  itg2const  24333  itg2const2  24334  itg2mulclem  24339  itg2mulc  24340  itg2monolem1  24343  itg2mono  24346  itg2addlem  24351  itg2gt0  24353  itg2cnlem1  24354  itg2cnlem2  24355  itg2cn  24356  iblconst  24410  itgconst  24411  ibladdlem  24412  itgaddlem1  24415  iblabslem  24420  iblabs  24421  iblmulc2  24423  itgmulc2lem1  24424  bddmulibl  24431  itggt0  24434  itgcn  24435  dvge0  24595  dvle  24596  dvfsumrlim  24620  cxpcn3lem  25320  cxpcn3  25321  resqrtcn  25322  loglesqrt  25331  areaf  25531  areacl  25532  areage0  25533  rlimcnp3  25537  jensenlem2  25557  jensen  25558  amgmlem  25559  amgm  25560  dchrisumlem3  26059  dchrmusumlema  26061  dchrmusum2  26062  dchrvmasumlem2  26066  dchrvmasumiflem1  26069  dchrisum0lema  26082  dchrisum0lem1b  26083  dchrisum0lem1  26084  dchrisum0lem2  26086  axcontlem2  26743  axcontlem7  26748  axcontlem8  26749  axcontlem10  26751  rge0scvg  31185  esumpcvgval  31330  hasheuni  31337  esumcvg  31338  sibfof  31591  mbfposadd  34931  itg2addnclem2  34936  itg2addnclem3  34937  itg2addnc  34938  itg2gt0cn  34939  ibladdnclem  34940  itgaddnclem1  34942  iblabsnclem  34947  iblabsnc  34948  iblmulc2nc  34949  itgmulc2nclem1  34950  bddiblnc  34954  itggt0cn  34956  ftc1anclem3  34961  ftc1anclem4  34962  ftc1anclem5  34963  ftc1anclem6  34964  ftc1anclem7  34965  ftc1anclem8  34966  areacirclem2  34975  sge0iunmptlemfi  42686  digvalnn0  44650  nn0digval  44651  dignn0fr  44652  dig2nn1st  44656  digexp  44658  2sphere  44727  itsclc0  44749  itsclc0b  44750