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

Theorem rpregt0d 10396
Description: A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpregt0d  |-  ( ph  ->  ( A  e.  RR  /\  0  <  A ) )

Proof of Theorem rpregt0d
StepHypRef Expression
1 rpred.1 . . 3  |-  ( ph  ->  A  e.  RR+ )
21rpred 10390 . 2  |-  ( ph  ->  A  e.  RR )
31rpgt0d 10393 . 2  |-  ( ph  ->  0  <  A )
42, 3jca 518 1  |-  ( ph  ->  ( A  e.  RR  /\  0  <  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   class class class wbr 4023   RRcr 8736   0cc0 8737    < clt 8867   RR+crp 10354
This theorem is referenced by:  reclt1d  10403  recgt1d  10404  ltrecd  10408  lerecd  10409  ltrec1d  10410  lerec2d  10411  lediv2ad  10412  ltdiv2d  10413  lediv2d  10414  ledivdivd  10415  divge0d  10426  ltmul1d  10427  ltmul2d  10428  lemul1d  10429  lemul2d  10430  ltdiv1d  10431  lediv1d  10432  ltmuldivd  10433  ltmuldiv2d  10434  lemuldivd  10435  lemuldiv2d  10436  ltdivmuld  10437  ltdivmul2d  10438  ledivmuld  10439  ledivmul2d  10440  ltdiv23d  10446  lediv23d  10447  lt2mul2divd  10448  mertenslem1  12340  isprm6  12788  nmoi  18237  icopnfhmeo  18441  nmoleub2lem3  18596  lmnn  18689  ovolscalem1  18872  aaliou2b  19721  birthdaylem3  20248  fsumharmonic  20305  bcmono  20516  chtppilim  20624  dchrisum0lem1a  20635  dchrvmasumiflem1  20650  dchrisum0lem1b  20664  dchrisum0lem1  20665  mulog2sumlem2  20684  selberg3lem1  20706  pntrsumo1  20714  pntibndlem1  20738  pntibndlem3  20741  pntlemr  20751  pntlemj  20752  ostth3  20787  minvecolem3  21455  lnconi  22613  stirlinglem5  27827  stirlinglem6  27828
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-rp 10355
  Copyright terms: Public domain W3C validator