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

Theorem rpregt0d 11829
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 11823 . 2 (𝜑𝐴 ∈ ℝ)
31rpgt0d 11826 . 2 (𝜑 → 0 < 𝐴)
42, 3jca 554 1 (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987   class class class wbr 4618  cr 9886  0cc0 9887   < clt 10025  +crp 11783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619  df-rp 11784
This theorem is referenced by:  reclt1d  11836  recgt1d  11837  ltrecd  11841  lerecd  11842  ltrec1d  11843  lerec2d  11844  lediv2ad  11845  ltdiv2d  11846  lediv2d  11847  ledivdivd  11848  divge0d  11863  ltmul1d  11864  ltmul2d  11865  lemul1d  11866  lemul2d  11867  ltdiv1d  11868  lediv1d  11869  ltmuldivd  11870  ltmuldiv2d  11871  lemuldivd  11872  lemuldiv2d  11873  ltdivmuld  11874  ltdivmul2d  11875  ledivmuld  11876  ledivmul2d  11877  ltdiv23d  11888  lediv23d  11889  lt2mul2divd  11890  mertenslem1  14548  isprm6  15357  nmoi  22451  icopnfhmeo  22661  nmoleub2lem3  22834  lmnn  22980  ovolscalem1  23200  aaliou2b  24013  birthdaylem3  24593  fsumharmonic  24651  bcmono  24915  chtppilim  25077  dchrisum0lem1a  25088  dchrvmasumiflem1  25103  dchrisum0lem1b  25117  dchrisum0lem1  25118  mulog2sumlem2  25137  selberg3lem1  25159  pntrsumo1  25167  pntibndlem1  25191  pntibndlem3  25194  pntlemr  25204  pntlemj  25205  ostth3  25240  minvecolem3  27599  lnconi  28759  poimirlem29  33097  poimirlem30  33098  poimirlem31  33099  poimirlem32  33100  stoweidlem14  39559  stoweidlem34  39579  stoweidlem42  39587  stoweidlem51  39596  stoweidlem59  39604  stirlinglem5  39623  elbigolo1  41664
  Copyright terms: Public domain W3C validator