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

Theorem rpregt0 11278
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 11267 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
21biimpi 194 1  |-  ( A  e.  RR+  ->  ( A  e.  RR  /\  0  <  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1842   class class class wbr 4395   RRcr 9521   0cc0 9522    < clt 9658   RR+crp 11265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396  df-rp 11266
This theorem is referenced by:  rpne0  11280  modge0  12044  modlt  12045  modid  12059  expnlbnd  12340  o1fsum  13778  isprm6  14459  gexexlem  17182  lmnn  21994  aaliou2b  23029  harmonicbnd4  23666  logfaclbnd  23878  logfacrlim  23880  chto1ub  24042  vmadivsum  24048  dchrmusumlema  24059  dchrvmasumlem2  24064  dchrisum0lem2a  24083  dchrisum0lem2  24084  dchrisum0lem3  24085  mulogsumlem  24097  mulog2sumlem2  24101  selberg2lem  24116  selberg3lem1  24123  pntrmax  24130  pntrsumo1  24131  pntibndlem3  24158  divge1b  38627  divgt1b  38628  divlt1lt  38629
  Copyright terms: Public domain W3C validator