MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrege0 Structured version   Visualization version   GIF version

Theorem elrege0 12463
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
StepHypRef Expression
1 0re 10224 . 2 0 ∈ ℝ
2 elicopnf 12454 . 2 (0 ∈ ℝ → (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)))
31, 2ax-mp 5 1 (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wcel 2131   class class class wbr 4796  (class class class)co 6805  cr 10119  0cc0 10120  +∞cpnf 10255  cle 10259  [,)cico 12362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-i2m1 10188  ax-1ne0 10189  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-po 5179  df-so 5180  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-er 7903  df-en 8114  df-dom 8115  df-sdom 8116  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-ico 12366
This theorem is referenced by:  nn0rp0  12464  rge0ssre  12465  0e0icopnf  12467  ge0addcl  12469  ge0mulcl  12470  fsumge0  14718  fprodge0  14915  isabvd  19014  abvge0  19019  nmolb  22714  nmoge0  22718  nmoi  22725  icopnfcnv  22934  cphsqrtcl  23176  tchcph  23228  ovolfsf  23432  ovolmge0  23437  ovolunlem1a  23456  ovoliunlem1  23462  ovolicc2lem4  23480  ioombl1lem4  23521  uniioombllem2  23543  uniioombllem6  23548  0plef  23630  i1fpos  23664  mbfi1fseqlem1  23673  mbfi1fseqlem3  23675  mbfi1fseqlem4  23676  mbfi1fseqlem5  23677  mbfi1fseqlem6  23678  mbfi1flimlem  23680  itg2const  23698  itg2const2  23699  itg2mulclem  23704  itg2mulc  23705  itg2monolem1  23708  itg2mono  23711  itg2addlem  23716  itg2gt0  23718  itg2cnlem1  23719  itg2cnlem2  23720  itg2cn  23721  iblconst  23775  itgconst  23776  ibladdlem  23777  itgaddlem1  23780  iblabslem  23785  iblabs  23786  iblmulc2  23788  itgmulc2lem1  23789  bddmulibl  23796  itggt0  23799  itgcn  23800  dvge0  23960  dvle  23961  dvfsumrlim  23985  cxpcn3lem  24679  cxpcn3  24680  resqrtcn  24681  loglesqrt  24690  areaf  24879  areacl  24880  areage0  24881  rlimcnp3  24885  jensenlem2  24905  jensen  24906  amgmlem  24907  amgm  24908  dchrisumlem3  25371  dchrmusumlema  25373  dchrmusum2  25374  dchrvmasumlem2  25378  dchrvmasumiflem1  25381  dchrisum0lema  25394  dchrisum0lem1b  25395  dchrisum0lem1  25396  dchrisum0lem2  25398  axcontlem2  26036  axcontlem7  26041  axcontlem8  26042  axcontlem10  26044  rge0scvg  30296  esumpcvgval  30441  hasheuni  30448  esumcvg  30449  sibfof  30703  mbfposadd  33762  itg2addnclem2  33767  itg2addnclem3  33768  itg2addnc  33769  itg2gt0cn  33770  ibladdnclem  33771  itgaddnclem1  33773  iblabsnclem  33778  iblabsnc  33779  iblmulc2nc  33780  itgmulc2nclem1  33781  bddiblnc  33785  itggt0cn  33787  ftc1anclem3  33792  ftc1anclem4  33793  ftc1anclem5  33794  ftc1anclem6  33795  ftc1anclem7  33796  ftc1anclem8  33797  areacirclem2  33806  sge0iunmptlemfi  41125  digvalnn0  42895  nn0digval  42896  dignn0fr  42897  dig2nn1st  42901  digexp  42903
  Copyright terms: Public domain W3C validator