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

Theorem rpgt0d 11136
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 11108 . 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 1758   class class class wbr 4395   0cc0 9388    < clt 9524   RR+crp 11097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-rab 2805  df-v 3074  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-sn 3981  df-pr 3983  df-op 3987  df-br 4396  df-rp 11098
This theorem is referenced by:  rpregt0d  11139  ltmulgt11d  11164  ltmulgt12d  11165  gt0divd  11166  ge0divd  11167  lediv12ad  11188  expgt0  12009  nnesq  12100  bccl2  12211  sqrlem7  12851  sqrgt0d  13012  iseralt  13275  fsumlt  13376  geomulcvg  13449  eirrlem  13599  sqr2irrlem  13643  prmind2  13887  4sqlem11  14129  4sqlem12  14130  ssblex  20130  nrginvrcn  20399  mulc1cncf  20608  nmoleub2lem2  20798  itg2mulclem  21352  itggt0  21447  dvgt0  21604  ftc1lem5  21640  aaliou3lem2  21937  abelthlem8  22032  tanord  22122  tanregt0  22123  logccv  22236  cxpcn3lem  22313  jensenlem2  22509  basellem1  22546  sgmnncl  22613  chpdifbndlem2  22931  pntibndlem1  22966  pntibnd  22970  pntlemc  22972  abvcxp  22992  ostth2lem1  22995  ostth2lem3  23012  ostth2  23014  xrge0iifhom  26507  sgnmulrp2  27065  signsply0  27091  dmlogdmgm  27149  sinccvglem  27456  heicant  28569  itggt0cn  28607  ftc1cnnc  28609  bfplem1  28864  rrncmslem  28874  irrapxlem4  29309  irrapxlem5  29310  stoweidlem1  29939  stoweidlem7  29945  stoweidlem11  29949  stoweidlem25  29963  stoweidlem26  29964  stoweidlem34  29972  stoweidlem49  29987  stoweidlem52  29990  stoweidlem60  29998  wallispi  30008  stirlinglem6  30017  stirlinglem11  30022  taupilem1  35934
  Copyright terms: Public domain W3C validator