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

Theorem rpregt0d 10610
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 10604 . 2  |-  ( ph  ->  A  e.  RR )
31rpgt0d 10607 . 2  |-  ( ph  ->  0  <  A )
42, 3jca 519 1  |-  ( ph  ->  ( A  e.  RR  /\  0  <  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   class class class wbr 4172   RRcr 8945   0cc0 8946    < clt 9076   RR+crp 10568
This theorem is referenced by:  reclt1d  10617  recgt1d  10618  ltrecd  10622  lerecd  10623  ltrec1d  10624  lerec2d  10625  lediv2ad  10626  ltdiv2d  10627  lediv2d  10628  ledivdivd  10629  divge0d  10640  ltmul1d  10641  ltmul2d  10642  lemul1d  10643  lemul2d  10644  ltdiv1d  10645  lediv1d  10646  ltmuldivd  10647  ltmuldiv2d  10648  lemuldivd  10649  lemuldiv2d  10650  ltdivmuld  10651  ltdivmul2d  10652  ledivmuld  10653  ledivmul2d  10654  ltdiv23d  10660  lediv23d  10661  lt2mul2divd  10662  mertenslem1  12616  isprm6  13064  nmoi  18715  icopnfhmeo  18921  nmoleub2lem3  19076  lmnn  19169  ovolscalem1  19362  aaliou2b  20211  birthdaylem3  20745  fsumharmonic  20803  bcmono  21014  chtppilim  21122  dchrisum0lem1a  21133  dchrvmasumiflem1  21148  dchrisum0lem1b  21162  dchrisum0lem1  21163  mulog2sumlem2  21182  selberg3lem1  21204  pntrsumo1  21212  pntibndlem1  21236  pntibndlem3  21239  pntlemr  21249  pntlemj  21250  ostth3  21285  minvecolem3  22331  lnconi  23489  stoweidlem14  27630  stoweidlem34  27650  stoweidlem42  27658  stoweidlem51  27667  stoweidlem59  27675  stirlinglem5  27694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-rp 10569
  Copyright terms: Public domain W3C validator