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

Theorem rpregt0 10383
Description: A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
Assertion
Ref Expression
rpregt0  |-  ( A  e.  RR+  ->  ( A  e.  RR  /\  0  <  A ) )

Proof of Theorem rpregt0
StepHypRef Expression
1 elrp 10372 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
21biimpi 186 1  |-  ( A  e.  RR+  ->  ( A  e.  RR  /\  0  <  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   class class class wbr 4039   RRcr 8752   0cc0 8753    < clt 8883   RR+crp 10370
This theorem is referenced by:  rpne0  10385  modge0  10996  modlt  10997  modid  11009  expnlbnd  11247  o1fsum  12287  isprm6  12804  gexexlem  15160  lmnn  18705  aaliou2b  19737  harmonicbnd4  20320  logfaclbnd  20477  logfacrlim  20479  chto1ub  20641  vmadivsum  20647  dchrmusumlema  20658  dchrvmasumlem2  20663  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0lem3  20684  mulogsumlem  20696  mulog2sumlem2  20700  selberg2lem  20715  selberg3lem1  20722  pntrmax  20729  pntrsumo1  20730  pntibndlem3  20757  equivbnd  26617
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-rp 10371
  Copyright terms: Public domain W3C validator