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

Theorem elrege0 11384
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  |-  ( A  e.  ( 0 [,) +oo )  <->  ( A  e.  RR  /\  0  <_  A ) )

Proof of Theorem elrege0
StepHypRef Expression
1 0re 9378 . 2  |-  0  e.  RR
2 elicopnf 11377 . 2  |-  ( 0  e.  RR  ->  ( A  e.  ( 0 [,) +oo )  <->  ( A  e.  RR  /\  0  <_  A ) ) )
31, 2ax-mp 5 1  |-  ( A  e.  ( 0 [,) +oo )  <->  ( A  e.  RR  /\  0  <_  A ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1756   class class class wbr 4287  (class class class)co 6086   RRcr 9273   0cc0 9274   +oocpnf 9407    <_ cle 9411   [,)cico 11294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-ico 11298
This theorem is referenced by:  rge0ssre  11385  0e0icopnf  11387  ge0addcl  11389  ge0mulcl  11390  fsumge0  13250  isabvd  16883  abvge0  16888  nmolb  20271  nmoge0  20275  nmoi  20282  icopnfcnv  20489  icopnfhmeo  20490  cphsqrcl  20678  tchcph  20727  ovolfsf  20930  ovolmge0  20935  ovolunlem1a  20954  ovoliunlem1  20960  ovolicc2lem4  20978  ioombl1lem4  21017  uniioombllem2  21038  uniioombllem6  21043  0plef  21125  i1fpos  21159  mbfi1fseqlem1  21168  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1fseqlem6  21173  mbfi1flimlem  21175  itg2const  21193  itg2const2  21194  itg2mulclem  21199  itg2mulc  21200  itg2monolem1  21203  itg2monolem2  21204  itg2monolem3  21205  itg2mono  21206  itg2i1fseqle  21207  itg2i1fseq3  21210  itg2addlem  21211  itg2gt0  21213  itg2cnlem1  21214  itg2cnlem2  21215  itg2cn  21216  iblconst  21270  itgconst  21271  ibladdlem  21272  itgaddlem1  21275  iblabslem  21280  iblabs  21281  iblmulc2  21283  itgmulc2lem1  21284  bddmulibl  21291  itggt0  21294  itgcn  21295  dvge0  21453  dvle  21454  dvfsumrlim  21478  cxpcn3lem  22160  cxpcn3  22161  resqrcn  22162  loglesqr  22171  areaf  22330  areacl  22331  areage0  22332  rlimcnp3  22336  jensenlem2  22356  jensen  22357  amgmlem  22358  amgm  22359  dchrisumlem3  22715  dchrmusumlema  22717  dchrmusum2  22718  dchrvmasumlem2  22722  dchrvmasumiflem1  22725  dchrisum0lema  22738  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2  22742  axcontlem2  23162  axcontlem7  23167  axcontlem8  23168  axcontlem10  23170  rge0scvg  26331  esumpcvgval  26479  hasheuni  26486  esumcvg  26487  sibfof  26678  mbfposadd  28392  itg2addnclem2  28397  itg2addnclem3  28398  itg2addnc  28399  itg2gt0cn  28400  ibladdnclem  28401  itgaddnclem1  28403  iblabsnclem  28408  iblabsnc  28409  iblmulc2nc  28410  itgmulc2nclem1  28411  bddiblnc  28415  itggt0cn  28417  ftc1anclem3  28422  ftc1anclem4  28423  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  areacirclem2  28438
  Copyright terms: Public domain W3C validator