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

Theorem rpgt0d 11307
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 11276 . 2  |-  ( A  e.  RR+  ->  0  < 
A )
31, 2syl 17 1  |-  ( ph  ->  0  <  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   class class class wbr 4395   0cc0 9522    < clt 9658   RR+crp 11265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396  df-rp 11266
This theorem is referenced by:  rpregt0d  11310  ltmulgt11d  11335  ltmulgt12d  11336  gt0divd  11337  ge0divd  11338  lediv12ad  11359  expgt0  12243  nnesq  12334  bccl2  12445  sqrlem7  13231  sqrtgt0d  13393  iseralt  13656  fsumlt  13765  geomulcvg  13837  eirrlem  14146  sqr2irrlem  14190  prmind2  14437  4sqlem11  14682  4sqlem12  14683  ssblex  21223  nrginvrcn  21492  mulc1cncf  21701  nmoleub2lem2  21891  itg2mulclem  22445  itggt0  22540  dvgt0  22697  ftc1lem5  22733  aaliou3lem2  23031  abelthlem8  23126  tanord  23217  tanregt0  23218  logccv  23338  cxpcn3lem  23417  jensenlem2  23643  dmlogdmgm  23679  basellem1  23735  sgmnncl  23802  chpdifbndlem2  24120  pntibndlem1  24155  pntibnd  24159  pntlemc  24161  abvcxp  24181  ostth2lem1  24184  ostth2lem3  24201  ostth2  24203  xrge0iifhom  28372  omssubadd  28748  sgnmulrp2  28988  signsply0  29014  sinccvglem  29890  taupilem1  31247  heicant  31421  itggt0cn  31460  ftc1cnnc  31462  bfplem1  31600  rrncmslem  31610  irrapxlem4  35122  irrapxlem5  35123  imo72b2lem1  35999  dvdivbd  37088  ioodvbdlimc1lem2  37097  ioodvbdlimc2lem  37099  stoweidlem1  37151  stoweidlem7  37157  stoweidlem11  37161  stoweidlem25  37175  stoweidlem26  37176  stoweidlem34  37184  stoweidlem49  37199  stoweidlem52  37202  stoweidlem60  37210  wallispi  37220  stirlinglem6  37229  stirlinglem11  37234  fourierdlem30  37287
  Copyright terms: Public domain W3C validator