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

Theorem rpregt0 11262
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

Proof of Theorem rpregt0
StepHypRef Expression
1 elrp 11251 . 2
21biimpi 194 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818   class class class wbr 4452   cr 9512  0cc0 9513   clt 9649   crp 11249
This theorem is referenced by:  rpne0  11264  modge0  12005  modlt  12006  modid  12020  expnlbnd  12296  o1fsum  13627  isprm6  14250  gexexlem  16858  lmnn  21702  aaliou2b  22737  harmonicbnd4  23340  logfaclbnd  23497  logfacrlim  23499  chto1ub  23661  vmadivsum  23667  dchrmusumlema  23678  dchrvmasumlem2  23683  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0lem3  23704  mulogsumlem  23716  mulog2sumlem2  23720  selberg2lem  23735  selberg3lem1  23742  pntrmax  23749  pntrsumo1  23750  pntibndlem3  23777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-rp 11250
  Copyright terms: Public domain W3C validator