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

Theorem rpregt0d 11287
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 11281 . 2  |-  ( ph  ->  A  e.  RR )
31rpgt0d 11284 . 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 1819   class class class wbr 4456   RRcr 9508   0cc0 9509    < clt 9645   RR+crp 11245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-rp 11246
This theorem is referenced by:  reclt1d  11294  recgt1d  11295  ltrecd  11299  lerecd  11300  ltrec1d  11301  lerec2d  11302  lediv2ad  11303  ltdiv2d  11304  lediv2d  11305  ledivdivd  11306  divge0d  11317  ltmul1d  11318  ltmul2d  11319  lemul1d  11320  lemul2d  11321  ltdiv1d  11322  lediv1d  11323  ltmuldivd  11324  ltmuldiv2d  11325  lemuldivd  11326  lemuldiv2d  11327  ltdivmuld  11328  ltdivmul2d  11329  ledivmuld  11330  ledivmul2d  11331  ltdiv23d  11337  lediv23d  11338  lt2mul2divd  11339  mertenslem1  13705  isprm6  14262  nmoi  21361  icopnfhmeo  21569  nmoleub2lem3  21724  lmnn  21828  ovolscalem1  22050  aaliou2b  22863  birthdaylem3  23409  fsumharmonic  23467  bcmono  23678  chtppilim  23786  dchrisum0lem1a  23797  dchrvmasumiflem1  23812  dchrisum0lem1b  23826  dchrisum0lem1  23827  mulog2sumlem2  23846  selberg3lem1  23868  pntrsumo1  23876  pntibndlem1  23900  pntibndlem3  23903  pntlemr  23913  pntlemj  23914  ostth3  23949  minvecolem3  25919  lnconi  27079  stoweidlem14  31999  stoweidlem34  32019  stoweidlem42  32027  stoweidlem51  32036  stoweidlem59  32044  stirlinglem5  32063
  Copyright terms: Public domain W3C validator