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

Theorem elrege0 13372
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 11158 . 2 0 ∈ ℝ
2 elicopnf 13363 . 2 (0 ∈ ℝ → (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)))
31, 2ax-mp 5 1 (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wcel 2107   class class class wbr 5106  (class class class)co 7358  cr 11051  0cc0 11052  +∞cpnf 11187  cle 11191  [,)cico 13267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-addrcl 11113  ax-rnegex 11123  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-ico 13271
This theorem is referenced by:  nn0rp0  13373  rge0ssre  13374  0e0icopnf  13376  ge0addcl  13378  ge0mulcl  13379  fsumge0  15681  fprodge0  15877  isabvd  20282  abvge0  20287  nmolb  24084  nmoge0  24088  nmoi  24095  icopnfcnv  24308  cphsqrtcl  24551  tcphcph  24604  cphsscph  24618  ovolfsf  24838  ovolmge0  24844  ovolunlem1a  24863  ovoliunlem1  24869  ovolicc2lem4  24887  ioombl1lem4  24928  uniioombllem2  24950  uniioombllem6  24955  0plef  25039  i1fpos  25074  mbfi1fseqlem1  25083  mbfi1fseqlem3  25085  mbfi1fseqlem4  25086  mbfi1fseqlem5  25087  mbfi1fseqlem6  25088  mbfi1flimlem  25090  itg2const  25108  itg2const2  25109  itg2mulclem  25114  itg2mulc  25115  itg2monolem1  25118  itg2mono  25121  itg2addlem  25126  itg2gt0  25128  itg2cnlem1  25129  itg2cnlem2  25130  itg2cn  25131  iblconst  25185  itgconst  25186  ibladdlem  25187  itgaddlem1  25190  iblabslem  25195  iblabs  25196  iblmulc2  25198  itgmulc2lem1  25199  bddmulibl  25206  bddiblnc  25209  itggt0  25211  itgcn  25212  dvge0  25373  dvle  25374  dvfsumrlim  25398  cxpcn3lem  26103  cxpcn3  26104  resqrtcn  26105  loglesqrt  26114  areaf  26314  areacl  26315  areage0  26316  rlimcnp3  26320  jensenlem2  26340  jensen  26341  amgmlem  26342  amgm  26343  dchrisumlem3  26842  dchrmusumlema  26844  dchrmusum2  26845  dchrvmasumlem2  26849  dchrvmasumiflem1  26852  dchrisum0lema  26865  dchrisum0lem1b  26866  dchrisum0lem1  26867  dchrisum0lem2  26869  axcontlem2  27917  axcontlem7  27922  axcontlem8  27923  axcontlem10  27925  rge0scvg  32533  esumpcvgval  32680  hasheuni  32687  esumcvg  32688  sibfof  32943  mbfposadd  36128  itg2addnclem2  36133  itg2addnclem3  36134  itg2addnc  36135  itg2gt0cn  36136  ibladdnclem  36137  itgaddnclem1  36139  iblabsnclem  36144  iblabsnc  36145  iblmulc2nc  36146  itgmulc2nclem1  36147  itggt0cn  36151  ftc1anclem3  36156  ftc1anclem4  36157  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  areacirclem2  36170  sge0iunmptlemfi  44661  digvalnn0  46692  nn0digval  46693  dignn0fr  46694  dig2nn1st  46698  digexp  46700  2sphere  46842  itsclc0  46864  itsclc0b  46865
  Copyright terms: Public domain W3C validator