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

Theorem rpgt0d 12422
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 12389 . 2 (𝐴 ∈ ℝ+ → 0 < 𝐴)
31, 2syl 17 1 (𝜑 → 0 < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111   class class class wbr 5030  0cc0 10526   < clt 10664  +crp 12377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-rp 12378
This theorem is referenced by:  rpregt0d  12425  ltmulgt11d  12454  ltmulgt12d  12455  gt0divd  12456  ge0divd  12457  lediv12ad  12478  prodge0rd  12484  expgt0  13458  nnesq  13584  bccl2  13679  sqrlem7  14600  sqrtgt0d  14764  iseralt  15033  fsumlt  15147  geomulcvg  15224  eirrlem  15549  sqrt2irrlem  15593  prmind2  16019  4sqlem11  16281  4sqlem12  16282  ssblex  23035  nrginvrcn  23298  mulc1cncf  23510  nmoleub2lem2  23721  itg2mulclem  24350  itggt0  24447  dvgt0  24607  ftc1lem5  24643  aaliou3lem2  24939  abelthlem8  25034  tanord  25130  tanregt0  25131  logccv  25254  cxpcn3lem  25336  jensenlem2  25573  dmlogdmgm  25609  basellem1  25666  sgmnncl  25732  chpdifbndlem2  26138  pntibndlem1  26173  pntibnd  26177  pntlemc  26179  abvcxp  26199  ostth2lem1  26202  ostth2lem3  26219  ostth2  26221  xrge0iifhom  31290  omssubadd  31668  sgnmulrp2  31911  signsply0  31931  sinccvglem  33028  unblimceq0lem  33958  unbdqndv2lem2  33962  knoppndvlem14  33977  taupilem1  34735  poimirlem29  35086  heicant  35092  itggt0cn  35127  ftc1cnnc  35129  bfplem1  35260  rrncmslem  35270  irrapxlem4  39764  irrapxlem5  39765  imo72b2lem1  40872  dvdivbd  42563  ioodvbdlimc1lem2  42572  ioodvbdlimc2lem  42574  stoweidlem1  42641  stoweidlem7  42647  stoweidlem11  42651  stoweidlem25  42665  stoweidlem26  42666  stoweidlem34  42674  stoweidlem49  42689  stoweidlem52  42692  stoweidlem60  42700  wallispi  42710  stirlinglem6  42719  stirlinglem11  42724  fourierdlem30  42777  qndenserrnbl  42935  ovnsubaddlem1  43207  hoiqssbllem2  43260  pimrecltpos  43342  smfmullem1  43421  smfmullem2  43422  smfmullem3  43423
  Copyright terms: Public domain W3C validator