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

Theorem rpregt0 11023
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 11012 . 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 369    e. wcel 1756   class class class wbr 4311   RRcr 9300   0cc0 9301    < clt 9437   RR+crp 11010
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-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2743  df-v 2993  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903  df-br 4312  df-rp 11011
This theorem is referenced by:  rpne0  11025  modge0  11736  modlt  11737  modid  11751  expnlbnd  12013  o1fsum  13295  isprm6  13814  gexexlem  16353  lmnn  20793  aaliou2b  21826  harmonicbnd4  22423  logfaclbnd  22580  logfacrlim  22582  chto1ub  22744  vmadivsum  22750  dchrmusumlema  22761  dchrvmasumlem2  22766  dchrisum0lem2a  22785  dchrisum0lem2  22786  dchrisum0lem3  22787  mulogsumlem  22799  mulog2sumlem2  22803  selberg2lem  22818  selberg3lem1  22825  pntrmax  22832  pntrsumo1  22833  pntibndlem3  22860
  Copyright terms: Public domain W3C validator