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

Theorem rpregt0d 12423
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 12417 . 2 (𝜑𝐴 ∈ ℝ)
31rpgt0d 12420 . 2 (𝜑 → 0 < 𝐴)
42, 3jca 515 1 (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115   class class class wbr 5047  cr 10521  0cc0 10522   < clt 10660  +crp 12375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-br 5048  df-rp 12376
This theorem is referenced by:  reclt1d  12430  recgt1d  12431  ltrecd  12435  lerecd  12436  ltrec1d  12437  lerec2d  12438  lediv2ad  12439  ltdiv2d  12440  lediv2d  12441  ledivdivd  12442  divge0d  12457  ltmul1d  12458  ltmul2d  12459  lemul1d  12460  lemul2d  12461  ltdiv1d  12462  lediv1d  12463  ltmuldivd  12464  ltmuldiv2d  12465  lemuldivd  12466  lemuldiv2d  12467  ltdivmuld  12468  ltdivmul2d  12469  ledivmuld  12470  ledivmul2d  12471  ltdiv23d  12484  lediv23d  12485  lt2mul2divd  12486  mertenslem1  15229  isprm6  16045  nmoi  23323  icopnfhmeo  23537  nmoleub2lem3  23709  lmnn  23856  ovolscalem1  24106  aaliou2b  24926  birthdaylem3  25528  fsumharmonic  25586  bcmono  25850  chtppilim  26048  dchrisum0lem1a  26059  dchrvmasumiflem1  26074  dchrisum0lem1b  26088  dchrisum0lem1  26089  mulog2sumlem2  26108  selberg3lem1  26130  pntrsumo1  26138  pntibndlem1  26162  pntibndlem3  26165  pntlemr  26175  pntlemj  26176  ostth3  26211  minvecolem3  28648  lnconi  29805  poimirlem29  34986  poimirlem30  34987  poimirlem31  34988  poimirlem32  34989  stoweidlem14  42498  stoweidlem34  42518  stoweidlem42  42526  stoweidlem51  42535  stoweidlem59  42543  stirlinglem5  42562  elbigolo1  44812
  Copyright terms: Public domain W3C validator