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

Theorem rpgt0d 10393
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 10365 . 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 1684   class class class wbr 4023   0cc0 8737    < clt 8867   RR+crp 10354
This theorem is referenced by:  rpregt0d  10396  ltmulgt11d  10421  ltmulgt12d  10422  gt0divd  10423  ge0divd  10424  lediv12ad  10445  expgt0  11135  nnesq  11225  bccl2  11335  sqrlem7  11734  sqrgt0d  11895  iseralt  12157  fsumlt  12258  geomulcvg  12332  eirrlem  12482  sqr2irrlem  12526  prmind2  12769  4sqlem11  13002  4sqlem12  13003  ssblex  17974  nrginvrcn  18202  mulc1cncf  18409  nmoleub2lem2  18597  itg2mulclem  19101  itggt0  19196  dvgt0  19351  ftc1lem5  19387  aaliou3lem2  19723  abelthlem8  19815  tanord  19900  tanregt0  19901  logccv  20010  cxpcn3lem  20087  jensenlem2  20282  basellem1  20318  sgmnncl  20385  chpdifbndlem2  20703  pntibndlem1  20738  pntibnd  20742  pntlemc  20744  abvcxp  20764  ostth2lem1  20767  ostth2lem3  20784  ostth2  20786  xrge0iifhom  23319  esumcst  23436  sinccvglem  24005  bfplem1  26546  rrncmslem  26556  irrapxlem4  26910  irrapxlem5  26911  wallispi  27819  stirlinglem1  27823  stirlinglem4  27826  stirlinglem6  27828  stirlinglem8  27830  stirlinglem11  27833
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-rp 10355
  Copyright terms: Public domain W3C validator