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

Theorem rpgt0d 10607
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 10579 . 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 1721   class class class wbr 4172   0cc0 8946    < clt 9076   RR+crp 10568
This theorem is referenced by:  rpregt0d  10610  ltmulgt11d  10635  ltmulgt12d  10636  gt0divd  10637  ge0divd  10638  lediv12ad  10659  expgt0  11368  nnesq  11458  bccl2  11569  sqrlem7  12009  sqrgt0d  12170  iseralt  12433  fsumlt  12534  geomulcvg  12608  eirrlem  12758  sqr2irrlem  12802  prmind2  13045  4sqlem11  13278  4sqlem12  13279  ssblex  18411  nrginvrcn  18680  mulc1cncf  18888  nmoleub2lem2  19077  itg2mulclem  19591  itggt0  19686  dvgt0  19841  ftc1lem5  19877  aaliou3lem2  20213  abelthlem8  20308  tanord  20393  tanregt0  20394  logccv  20507  cxpcn3lem  20584  jensenlem2  20779  basellem1  20816  sgmnncl  20883  chpdifbndlem2  21201  pntibndlem1  21236  pntibnd  21240  pntlemc  21242  abvcxp  21262  ostth2lem1  21265  ostth2lem3  21282  ostth2  21284  xrge0iifhom  24276  dmlogdmgm  24761  sinccvglem  25062  itggt0cn  26176  ftc1cnnc  26178  bfplem1  26421  rrncmslem  26431  irrapxlem4  26778  irrapxlem5  26779  stoweidlem1  27617  stoweidlem7  27623  stoweidlem11  27627  stoweidlem25  27641  stoweidlem26  27642  stoweidlem34  27650  stoweidlem49  27665  stoweidlem52  27668  stoweidlem60  27676  wallispi  27686  stirlinglem6  27695  stirlinglem11  27700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-rp 10569
  Copyright terms: Public domain W3C validator