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

Theorem rpgt0d 12077
Description: A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1 (𝜑𝐴 ∈ ℝ+)
Assertion
Ref Expression
rpgt0d (𝜑 → 0 < 𝐴)

Proof of Theorem rpgt0d
StepHypRef Expression
1 rpred.1 . 2 (𝜑𝐴 ∈ ℝ+)
2 rpgt0 12046 . 2 (𝐴 ∈ ℝ+ → 0 < 𝐴)
31, 2syl 17 1 (𝜑 → 0 < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2144   class class class wbr 4784  0cc0 10137   < clt 10275  +crp 12034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785  df-rp 12035
This theorem is referenced by:  rpregt0d  12080  ltmulgt11d  12109  ltmulgt12d  12110  gt0divd  12111  ge0divd  12112  lediv12ad  12133  prodge0rd  12139  expgt0  13099  nnesq  13194  bccl2  13313  sqrlem7  14196  sqrtgt0d  14358  iseralt  14622  fsumlt  14738  geomulcvg  14813  eirrlem  15137  sqrt2irrlem  15182  sqrt2irrlemOLD  15183  prmind2  15604  4sqlem11  15865  4sqlem12  15866  ssblex  22452  nrginvrcn  22715  mulc1cncf  22927  nmoleub2lem2  23134  itg2mulclem  23732  itggt0  23827  dvgt0  23986  ftc1lem5  24022  aaliou3lem2  24317  abelthlem8  24412  tanord  24504  tanregt0  24505  logccv  24629  cxpcn3lem  24708  jensenlem2  24934  dmlogdmgm  24970  basellem1  25027  sgmnncl  25093  chpdifbndlem2  25463  pntibndlem1  25498  pntibnd  25502  pntlemc  25504  abvcxp  25524  ostth2lem1  25527  ostth2lem3  25544  ostth2  25546  xrge0iifhom  30317  omssubadd  30696  sgnmulrp2  30939  signsply0  30962  sinccvglem  31898  unblimceq0lem  32828  unbdqndv2lem2  32832  knoppndvlem14  32847  taupilem1  33497  poimirlem29  33764  heicant  33770  itggt0cn  33807  ftc1cnnc  33809  bfplem1  33946  rrncmslem  33956  irrapxlem4  37908  irrapxlem5  37909  imo72b2lem1  38990  dvdivbd  40650  ioodvbdlimc1lem2  40659  ioodvbdlimc2lem  40661  stoweidlem1  40729  stoweidlem7  40735  stoweidlem11  40739  stoweidlem25  40753  stoweidlem26  40754  stoweidlem34  40762  stoweidlem49  40777  stoweidlem52  40780  stoweidlem60  40788  wallispi  40798  stirlinglem6  40807  stirlinglem11  40812  fourierdlem30  40865  qndenserrnbl  41026  ovnsubaddlem1  41298  hoiqssbllem2  41351  pimrecltpos  41433  smfmullem1  41512  smfmullem2  41513  smfmullem3  41514
  Copyright terms: Public domain W3C validator