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

Theorem rpgt0d 10640
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 10612 . 2  |-  ( A  e.  RR+  ->  0  < 
A )
31, 2syl 16 1  |-  ( ph  ->  0  <  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   class class class wbr 4204   0cc0 8979    < clt 9109   RR+crp 10601
This theorem is referenced by:  rpregt0d  10643  ltmulgt11d  10668  ltmulgt12d  10669  gt0divd  10670  ge0divd  10671  lediv12ad  10692  expgt0  11401  nnesq  11491  bccl2  11602  sqrlem7  12042  sqrgt0d  12203  iseralt  12466  fsumlt  12567  geomulcvg  12641  eirrlem  12791  sqr2irrlem  12835  prmind2  13078  4sqlem11  13311  4sqlem12  13312  ssblex  18446  nrginvrcn  18715  mulc1cncf  18923  nmoleub2lem2  19112  itg2mulclem  19626  itggt0  19721  dvgt0  19876  ftc1lem5  19912  aaliou3lem2  20248  abelthlem8  20343  tanord  20428  tanregt0  20429  logccv  20542  cxpcn3lem  20619  jensenlem2  20814  basellem1  20851  sgmnncl  20918  chpdifbndlem2  21236  pntibndlem1  21271  pntibnd  21275  pntlemc  21277  abvcxp  21297  ostth2lem1  21300  ostth2lem3  21317  ostth2  21319  xrge0iifhom  24311  dmlogdmgm  24796  sinccvglem  25097  itggt0cn  26223  ftc1cnnc  26225  bfplem1  26468  rrncmslem  26478  irrapxlem4  26825  irrapxlem5  26826  stoweidlem1  27664  stoweidlem7  27670  stoweidlem11  27674  stoweidlem25  27688  stoweidlem26  27689  stoweidlem34  27697  stoweidlem49  27712  stoweidlem52  27715  stoweidlem60  27723  wallispi  27733  stirlinglem6  27742  stirlinglem11  27747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-rp 10602
  Copyright terms: Public domain W3C validator