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

Theorem rpregt0d 11054
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 11048 . 2  |-  ( ph  ->  A  e.  RR )
31rpgt0d 11051 . 2  |-  ( ph  ->  0  <  A )
42, 3jca 532 1  |-  ( ph  ->  ( A  e.  RR  /\  0  <  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   class class class wbr 4313   RRcr 9302   0cc0 9303    < clt 9439   RR+crp 11012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-rp 11013
This theorem is referenced by:  reclt1d  11061  recgt1d  11062  ltrecd  11066  lerecd  11067  ltrec1d  11068  lerec2d  11069  lediv2ad  11070  ltdiv2d  11071  lediv2d  11072  ledivdivd  11073  divge0d  11084  ltmul1d  11085  ltmul2d  11086  lemul1d  11087  lemul2d  11088  ltdiv1d  11089  lediv1d  11090  ltmuldivd  11091  ltmuldiv2d  11092  lemuldivd  11093  lemuldiv2d  11094  ltdivmuld  11095  ltdivmul2d  11096  ledivmuld  11097  ledivmul2d  11098  ltdiv23d  11104  lediv23d  11105  lt2mul2divd  11106  mertenslem1  13365  isprm6  13816  nmoi  20329  icopnfhmeo  20537  nmoleub2lem3  20692  lmnn  20796  ovolscalem1  21018  aaliou2b  21829  birthdaylem3  22369  fsumharmonic  22427  bcmono  22638  chtppilim  22746  dchrisum0lem1a  22757  dchrvmasumiflem1  22772  dchrisum0lem1b  22786  dchrisum0lem1  22787  mulog2sumlem2  22806  selberg3lem1  22828  pntrsumo1  22836  pntibndlem1  22860  pntibndlem3  22863  pntlemr  22873  pntlemj  22874  ostth3  22909  ttgcontlem1  23153  minvecolem3  24299  lnconi  25459  stoweidlem14  29835  stoweidlem34  29855  stoweidlem42  29863  stoweidlem51  29872  stoweidlem59  29880  stirlinglem5  29899
  Copyright terms: Public domain W3C validator