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

Theorem rpgt0d 11707
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 11676 . 2 (𝐴 ∈ ℝ+ → 0 < 𝐴)
31, 2syl 17 1 (𝜑 → 0 < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976   class class class wbr 4577  0cc0 9792   < clt 9930  +crp 11664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-rp 11665
This theorem is referenced by:  rpregt0d  11710  ltmulgt11d  11739  ltmulgt12d  11740  gt0divd  11741  ge0divd  11742  lediv12ad  11763  expgt0  12710  nnesq  12805  bccl2  12927  sqrlem7  13783  sqrtgt0d  13945  iseralt  14209  fsumlt  14319  geomulcvg  14392  eirrlem  14717  sqr2irrlem  14762  prmind2  15182  4sqlem11  15443  4sqlem12  15444  ssblex  21984  nrginvrcn  22239  mulc1cncf  22447  nmoleub2lem2  22655  itg2mulclem  23236  itggt0  23331  dvgt0  23488  ftc1lem5  23524  aaliou3lem2  23819  abelthlem8  23914  tanord  24005  tanregt0  24006  logccv  24126  cxpcn3lem  24205  jensenlem2  24431  dmlogdmgm  24467  basellem1  24524  sgmnncl  24590  chpdifbndlem2  24960  pntibndlem1  24995  pntibnd  24999  pntlemc  25001  abvcxp  25021  ostth2lem1  25024  ostth2lem3  25041  ostth2  25043  xrge0iifhom  29117  omssubadd  29495  sgnmulrp2  29738  signsply0  29760  sinccvglem  30626  unblimceq0lem  31473  unbdqndv2lem2  31477  knoppndvlem14  31492  taupilem1  32140  poimirlem29  32404  heicant  32410  itggt0cn  32448  ftc1cnnc  32450  bfplem1  32587  rrncmslem  32597  irrapxlem4  36203  irrapxlem5  36204  imo72b2lem1  37289  dvdivbd  38610  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  stoweidlem1  38691  stoweidlem7  38697  stoweidlem11  38701  stoweidlem25  38715  stoweidlem26  38716  stoweidlem34  38724  stoweidlem49  38739  stoweidlem52  38742  stoweidlem60  38750  wallispi  38760  stirlinglem6  38769  stirlinglem11  38774  fourierdlem30  38827  qndenserrnbl  38988  ovnsubaddlem1  39257  hoiqssbllem2  39310  pimrecltpos  39393  smfmullem1  39473  smfmullem2  39474  smfmullem3  39475
  Copyright terms: Public domain W3C validator