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

Theorem rpgt0d 11026
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 10998 . 2  |-  ( A  e.  RR+  ->  0  < 
A )
31, 2syl 16 1  |-  ( ph  ->  0  <  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   class class class wbr 4289   0cc0 9278    < clt 9414   RR+crp 10987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-rp 10988
This theorem is referenced by:  rpregt0d  11029  ltmulgt11d  11054  ltmulgt12d  11055  gt0divd  11056  ge0divd  11057  lediv12ad  11078  expgt0  11893  nnesq  11984  bccl2  12095  sqrlem7  12734  sqrgt0d  12895  iseralt  13158  fsumlt  13259  geomulcvg  13332  eirrlem  13482  sqr2irrlem  13526  prmind2  13770  4sqlem11  14012  4sqlem12  14013  ssblex  19962  nrginvrcn  20231  mulc1cncf  20440  nmoleub2lem2  20630  itg2mulclem  21183  itggt0  21278  dvgt0  21435  ftc1lem5  21471  aaliou3lem2  21768  abelthlem8  21863  tanord  21953  tanregt0  21954  logccv  22067  cxpcn3lem  22144  jensenlem2  22340  basellem1  22377  sgmnncl  22444  chpdifbndlem2  22762  pntibndlem1  22797  pntibnd  22801  pntlemc  22803  abvcxp  22823  ostth2lem1  22826  ostth2lem3  22843  ostth2  22845  xrge0iifhom  26303  sgnmulrp2  26856  signsply0  26882  dmlogdmgm  26940  sinccvglem  27246  heicant  28351  itggt0cn  28389  ftc1cnnc  28391  bfplem1  28646  rrncmslem  28656  irrapxlem4  29091  irrapxlem5  29092  stoweidlem1  29721  stoweidlem7  29727  stoweidlem11  29731  stoweidlem25  29745  stoweidlem26  29746  stoweidlem34  29754  stoweidlem49  29769  stoweidlem52  29772  stoweidlem60  29780  wallispi  29790  stirlinglem6  29799  stirlinglem11  29804  taupilem1  35337
  Copyright terms: Public domain W3C validator