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

Theorem rpregt0d 10978
Description: A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1
Assertion
Ref Expression
rpregt0d

Proof of Theorem rpregt0d
StepHypRef Expression
1 rpred.1 . . 3
21rpred 10972 . 2
31rpgt0d 10975 . 2
42, 3jca 522 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  e.wcel 1749   class class class wbr 4267   cr 9227  0cc0 9228   clt 9364   crp 10936
This theorem is referenced by:  reclt1d  10985  recgt1d  10986  ltrecd  10990  lerecd  10991  ltrec1d  10992  lerec2d  10993  lediv2ad  10994  ltdiv2d  10995  lediv2d  10996  ledivdivd  10997  divge0d  11008  ltmul1d  11009  ltmul2d  11010  lemul1d  11011  lemul2d  11012  ltdiv1d  11013  lediv1d  11014  ltmuldivd  11015  ltmuldiv2d  11016  lemuldivd  11017  lemuldiv2d  11018  ltdivmuld  11019  ltdivmul2d  11020  ledivmuld  11021  ledivmul2d  11022  ltdiv23d  11028  lediv23d  11029  lt2mul2divd  11030  mertenslem1  13284  isprm6  13735  nmoi  20007  icopnfhmeo  20215  nmoleub2lem3  20370  lmnn  20474  ovolscalem1  20696  aaliou2b  21548  birthdaylem3  22088  fsumharmonic  22146  bcmono  22357  chtppilim  22465  dchrisum0lem1a  22476  dchrvmasumiflem1  22491  dchrisum0lem1b  22505  dchrisum0lem1  22506  mulog2sumlem2  22525  selberg3lem1  22547  pntrsumo1  22555  pntibndlem1  22579  pntibndlem3  22582  pntlemr  22592  pntlemj  22593  ostth3  22628  ttgcontlem1  22810  minvecolem3  23956  lnconi  25116  stoweidlem14  29483  stoweidlem34  29503  stoweidlem42  29511  stoweidlem51  29520  stoweidlem59  29528  stirlinglem5  29547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-br 4268  df-rp 10937
  Copyright terms: Public domain W3C validator