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

Theorem rpregt0d 11262
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 11256 . 2  |-  ( ph  ->  A  e.  RR )
31rpgt0d 11259 . 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 1767   class class class wbr 4447   RRcr 9491   0cc0 9492    < clt 9628   RR+crp 11220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-rp 11221
This theorem is referenced by:  reclt1d  11269  recgt1d  11270  ltrecd  11274  lerecd  11275  ltrec1d  11276  lerec2d  11277  lediv2ad  11278  ltdiv2d  11279  lediv2d  11280  ledivdivd  11281  divge0d  11292  ltmul1d  11293  ltmul2d  11294  lemul1d  11295  lemul2d  11296  ltdiv1d  11297  lediv1d  11298  ltmuldivd  11299  ltmuldiv2d  11300  lemuldivd  11301  lemuldiv2d  11302  ltdivmuld  11303  ltdivmul2d  11304  ledivmuld  11305  ledivmul2d  11306  ltdiv23d  11312  lediv23d  11313  lt2mul2divd  11314  mertenslem1  13656  isprm6  14109  nmoi  20998  icopnfhmeo  21206  nmoleub2lem3  21361  lmnn  21465  ovolscalem1  21687  aaliou2b  22499  birthdaylem3  23039  fsumharmonic  23097  bcmono  23308  chtppilim  23416  dchrisum0lem1a  23427  dchrvmasumiflem1  23442  dchrisum0lem1b  23456  dchrisum0lem1  23457  mulog2sumlem2  23476  selberg3lem1  23498  pntrsumo1  23506  pntibndlem1  23530  pntibndlem3  23533  pntlemr  23543  pntlemj  23544  ostth3  23579  ttgcontlem1  23892  minvecolem3  25496  lnconi  26656  stoweidlem14  31342  stoweidlem34  31362  stoweidlem42  31370  stoweidlem51  31379  stoweidlem59  31387  stirlinglem5  31406
  Copyright terms: Public domain W3C validator