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

Theorem rpgt0d 10485
Description: A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpgt0d  |-  ( ph  ->  0  <  A )

Proof of Theorem rpgt0d
StepHypRef Expression
1 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
2 rpgt0 10457 . 2  |-  ( A  e.  RR+  ->  0  < 
A )
31, 2syl 15 1  |-  ( ph  ->  0  <  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   class class class wbr 4104   0cc0 8827    < clt 8957   RR+crp 10446
This theorem is referenced by:  rpregt0d  10488  ltmulgt11d  10513  ltmulgt12d  10514  gt0divd  10515  ge0divd  10516  lediv12ad  10537  expgt0  11228  nnesq  11318  bccl2  11428  sqrlem7  11830  sqrgt0d  11991  iseralt  12254  fsumlt  12355  geomulcvg  12429  eirrlem  12579  sqr2irrlem  12623  prmind2  12866  4sqlem11  13099  4sqlem12  13100  ssblex  18076  nrginvrcn  18304  mulc1cncf  18512  nmoleub2lem2  18701  itg2mulclem  19205  itggt0  19300  dvgt0  19455  ftc1lem5  19491  aaliou3lem2  19827  abelthlem8  19922  tanord  20007  tanregt0  20008  logccv  20121  cxpcn3lem  20198  jensenlem2  20393  basellem1  20430  sgmnncl  20497  chpdifbndlem2  20815  pntibndlem1  20850  pntibnd  20854  pntlemc  20856  abvcxp  20876  ostth2lem1  20879  ostth2lem3  20896  ostth2  20898  xrge0iifhom  23479  esumcst  23721  dmlogdmgm  24057  sinccvglem  24409  itggt0cn  25512  ftc1cnnc  25514  bfplem1  25869  rrncmslem  25879  irrapxlem4  26233  irrapxlem5  26234  wallispi  27142  stirlinglem1  27146  stirlinglem4  27149  stirlinglem6  27151  stirlinglem8  27153  stirlinglem11  27156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105  df-rp 10447
  Copyright terms: Public domain W3C validator