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

Theorem rpgt0d 11255
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 11227 . 2  |-  ( A  e.  RR+  ->  0  < 
A )
31, 2syl 16 1  |-  ( ph  ->  0  <  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   class class class wbr 4447   0cc0 9488    < clt 9624   RR+crp 11216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-rp 11217
This theorem is referenced by:  rpregt0d  11258  ltmulgt11d  11283  ltmulgt12d  11284  gt0divd  11285  ge0divd  11286  lediv12ad  11307  expgt0  12163  nnesq  12254  bccl2  12365  sqrlem7  13041  sqrtgt0d  13203  iseralt  13466  fsumlt  13573  geomulcvg  13644  eirrlem  13794  sqr2irrlem  13838  prmind2  14083  4sqlem11  14328  4sqlem12  14329  ssblex  20666  nrginvrcn  20935  mulc1cncf  21144  nmoleub2lem2  21334  itg2mulclem  21888  itggt0  21983  dvgt0  22140  ftc1lem5  22176  aaliou3lem2  22473  abelthlem8  22568  tanord  22658  tanregt0  22659  logccv  22772  cxpcn3lem  22849  jensenlem2  23045  basellem1  23082  sgmnncl  23149  chpdifbndlem2  23467  pntibndlem1  23502  pntibnd  23506  pntlemc  23508  abvcxp  23528  ostth2lem1  23531  ostth2lem3  23548  ostth2  23550  xrge0iifhom  27555  sgnmulrp2  28122  signsply0  28148  dmlogdmgm  28206  sinccvglem  28513  heicant  29626  itggt0cn  29664  ftc1cnnc  29666  bfplem1  29921  rrncmslem  29931  irrapxlem4  30365  irrapxlem5  30366  dvdivbd  31253  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem1  31301  stoweidlem7  31307  stoweidlem11  31311  stoweidlem25  31325  stoweidlem26  31326  stoweidlem34  31334  stoweidlem49  31349  stoweidlem52  31352  stoweidlem60  31360  wallispi  31370  stirlinglem6  31379  stirlinglem11  31384  fourierdlem30  31437  fourierdlem39  31446  taupilem1  36767
  Copyright terms: Public domain W3C validator