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 2105   class class class wbr 5057  0cc0 10525   < clt 10663  +crp 12377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-rp 12378
This theorem is referenced by:  rpregt0d  12425  ltmulgt11d  12454  ltmulgt12d  12455  gt0divd  12456  ge0divd  12457  lediv12ad  12478  prodge0rd  12484  expgt0  13450  nnesq  13576  bccl2  13671  sqrlem7  14596  sqrtgt0d  14760  iseralt  15029  fsumlt  15143  geomulcvg  15220  eirrlem  15545  sqrt2irrlem  15589  prmind2  16017  4sqlem11  16279  4sqlem12  16280  ssblex  22965  nrginvrcn  23228  mulc1cncf  23440  nmoleub2lem2  23647  itg2mulclem  24274  itggt0  24369  dvgt0  24528  ftc1lem5  24564  aaliou3lem2  24859  abelthlem8  24954  tanord  25049  tanregt0  25050  logccv  25173  cxpcn3lem  25255  jensenlem2  25492  dmlogdmgm  25528  basellem1  25585  sgmnncl  25651  chpdifbndlem2  26057  pntibndlem1  26092  pntibnd  26096  pntlemc  26098  abvcxp  26118  ostth2lem1  26121  ostth2lem3  26138  ostth2  26140  xrge0iifhom  31079  omssubadd  31457  sgnmulrp2  31700  signsply0  31720  sinccvglem  32812  unblimceq0lem  33742  unbdqndv2lem2  33746  knoppndvlem14  33761  taupilem1  34484  poimirlem29  34802  heicant  34808  itggt0cn  34845  ftc1cnnc  34847  bfplem1  34981  rrncmslem  34991  irrapxlem4  39300  irrapxlem5  39301  imo72b2lem1  40399  dvdivbd  42084  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  stoweidlem1  42163  stoweidlem7  42169  stoweidlem11  42173  stoweidlem25  42187  stoweidlem26  42188  stoweidlem34  42196  stoweidlem49  42211  stoweidlem52  42214  stoweidlem60  42222  wallispi  42232  stirlinglem6  42241  stirlinglem11  42246  fourierdlem30  42299  qndenserrnbl  42457  ovnsubaddlem1  42729  hoiqssbllem2  42782  pimrecltpos  42864  smfmullem1  42943  smfmullem2  42944  smfmullem3  42945
  Copyright terms: Public domain W3C validator