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

Theorem rpgt0d 11288
Description: A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1
Assertion
Ref Expression
rpgt0d

Proof of Theorem rpgt0d
StepHypRef Expression
1 rpred.1 . 2
2 rpgt0 11260 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   class class class wbr 4452  0cc0 9513   clt 9649   crp 11249
This theorem is referenced by:  rpregt0d  11291  ltmulgt11d  11316  ltmulgt12d  11317  gt0divd  11318  ge0divd  11319  lediv12ad  11340  expgt0  12199  nnesq  12290  bccl2  12401  sqrlem7  13082  sqrtgt0d  13244  iseralt  13507  fsumlt  13614  geomulcvg  13685  eirrlem  13937  sqr2irrlem  13981  prmind2  14228  4sqlem11  14473  4sqlem12  14474  ssblex  20931  nrginvrcn  21200  mulc1cncf  21409  nmoleub2lem2  21599  itg2mulclem  22153  itggt0  22248  dvgt0  22405  ftc1lem5  22441  aaliou3lem2  22739  abelthlem8  22834  tanord  22925  tanregt0  22926  logccv  23044  cxpcn3lem  23121  jensenlem2  23317  basellem1  23354  sgmnncl  23421  chpdifbndlem2  23739  pntibndlem1  23774  pntibnd  23778  pntlemc  23780  abvcxp  23800  ostth2lem1  23803  ostth2lem3  23820  ostth2  23822  xrge0iifhom  27919  sgnmulrp2  28482  signsply0  28508  dmlogdmgm  28566  sinccvglem  29038  heicant  30049  itggt0cn  30087  ftc1cnnc  30089  bfplem1  30318  rrncmslem  30328  irrapxlem4  30761  irrapxlem5  30762  dvdivbd  31720  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem1  31783  stoweidlem7  31789  stoweidlem11  31793  stoweidlem25  31807  stoweidlem26  31808  stoweidlem34  31816  stoweidlem49  31831  stoweidlem52  31834  stoweidlem60  31842  wallispi  31852  stirlinglem6  31861  stirlinglem11  31866  fourierdlem30  31919  taupilem1  37696  imo72b2lem1  37988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-rp 11250
  Copyright terms: Public domain W3C validator