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

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

Proof of Theorem rpregt0d
StepHypRef Expression
1 rpred.1 . . 3 (𝜑𝐴 ∈ ℝ+)
21rpred 12085 . 2 (𝜑𝐴 ∈ ℝ)
31rpgt0d 12088 . 2 (𝜑 → 0 < 𝐴)
42, 3jca 555 1 (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2139   class class class wbr 4804  cr 10147  0cc0 10148   < clt 10286  +crp 12045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-rp 12046
This theorem is referenced by:  reclt1d  12098  recgt1d  12099  ltrecd  12103  lerecd  12104  ltrec1d  12105  lerec2d  12106  lediv2ad  12107  ltdiv2d  12108  lediv2d  12109  ledivdivd  12110  divge0d  12125  ltmul1d  12126  ltmul2d  12127  lemul1d  12128  lemul2d  12129  ltdiv1d  12130  lediv1d  12131  ltmuldivd  12132  ltmuldiv2d  12133  lemuldivd  12134  lemuldiv2d  12135  ltdivmuld  12136  ltdivmul2d  12137  ledivmuld  12138  ledivmul2d  12139  ltdiv23d  12150  lediv23d  12151  lt2mul2divd  12152  mertenslem1  14835  isprm6  15648  nmoi  22753  icopnfhmeo  22963  nmoleub2lem3  23135  lmnn  23281  ovolscalem1  23501  aaliou2b  24315  birthdaylem3  24900  fsumharmonic  24958  bcmono  25222  chtppilim  25384  dchrisum0lem1a  25395  dchrvmasumiflem1  25410  dchrisum0lem1b  25424  dchrisum0lem1  25425  mulog2sumlem2  25444  selberg3lem1  25466  pntrsumo1  25474  pntibndlem1  25498  pntibndlem3  25501  pntlemr  25511  pntlemj  25512  ostth3  25547  minvecolem3  28062  lnconi  29222  poimirlem29  33769  poimirlem30  33770  poimirlem31  33771  poimirlem32  33772  stoweidlem14  40752  stoweidlem34  40772  stoweidlem42  40780  stoweidlem51  40789  stoweidlem59  40797  stirlinglem5  40816  elbigolo1  42879
  Copyright terms: Public domain W3C validator