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

Theorem rpgt0d 11913
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 11882 . 2 (𝐴 ∈ ℝ+ → 0 < 𝐴)
31, 2syl 17 1 (𝜑 → 0 < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030   class class class wbr 4685  0cc0 9974   < clt 10112  +crp 11870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-rp 11871
This theorem is referenced by:  rpregt0d  11916  ltmulgt11d  11945  ltmulgt12d  11946  gt0divd  11947  ge0divd  11948  lediv12ad  11969  expgt0  12933  nnesq  13028  bccl2  13150  sqrlem7  14033  sqrtgt0d  14195  iseralt  14459  fsumlt  14576  geomulcvg  14651  eirrlem  14976  sqrt2irrlem  15021  sqrt2irrlemOLD  15022  prmind2  15445  4sqlem11  15706  4sqlem12  15707  ssblex  22280  nrginvrcn  22543  mulc1cncf  22755  nmoleub2lem2  22962  itg2mulclem  23558  itggt0  23653  dvgt0  23812  ftc1lem5  23848  aaliou3lem2  24143  abelthlem8  24238  tanord  24329  tanregt0  24330  logccv  24454  cxpcn3lem  24533  jensenlem2  24759  dmlogdmgm  24795  basellem1  24852  sgmnncl  24918  chpdifbndlem2  25288  pntibndlem1  25323  pntibnd  25327  pntlemc  25329  abvcxp  25349  ostth2lem1  25352  ostth2lem3  25369  ostth2  25371  xrge0iifhom  30111  omssubadd  30490  sgnmulrp2  30733  signsply0  30756  sinccvglem  31692  unblimceq0lem  32622  unbdqndv2lem2  32626  knoppndvlem14  32641  taupilem1  33297  poimirlem29  33568  heicant  33574  itggt0cn  33612  ftc1cnnc  33614  bfplem1  33751  rrncmslem  33761  irrapxlem4  37706  irrapxlem5  37707  imo72b2lem1  38788  dvdivbd  40456  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem1  40536  stoweidlem7  40542  stoweidlem11  40546  stoweidlem25  40560  stoweidlem26  40561  stoweidlem34  40569  stoweidlem49  40584  stoweidlem52  40587  stoweidlem60  40595  wallispi  40605  stirlinglem6  40614  stirlinglem11  40619  fourierdlem30  40672  qndenserrnbl  40833  ovnsubaddlem1  41105  hoiqssbllem2  41158  pimrecltpos  41240  smfmullem1  41319  smfmullem2  41320  smfmullem3  41321
  Copyright terms: Public domain W3C validator