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

Theorem rpregt0d 11291
Description: A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1
Assertion
Ref Expression
rpregt0d

Proof of Theorem rpregt0d
StepHypRef Expression
1 rpred.1 . . 3
21rpred 11285 . 2
31rpgt0d 11288 . 2
42, 3jca 532 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818   class class class wbr 4452   cr 9512  0cc0 9513   clt 9649   crp 11249
This theorem is referenced by:  reclt1d  11298  recgt1d  11299  ltrecd  11303  lerecd  11304  ltrec1d  11305  lerec2d  11306  lediv2ad  11307  ltdiv2d  11308  lediv2d  11309  ledivdivd  11310  divge0d  11321  ltmul1d  11322  ltmul2d  11323  lemul1d  11324  lemul2d  11325  ltdiv1d  11326  lediv1d  11327  ltmuldivd  11328  ltmuldiv2d  11329  lemuldivd  11330  lemuldiv2d  11331  ltdivmuld  11332  ltdivmul2d  11333  ledivmuld  11334  ledivmul2d  11335  ltdiv23d  11341  lediv23d  11342  lt2mul2divd  11343  mertenslem1  13693  isprm6  14250  nmoi  21235  icopnfhmeo  21443  nmoleub2lem3  21598  lmnn  21702  ovolscalem1  21924  aaliou2b  22737  birthdaylem3  23283  fsumharmonic  23341  bcmono  23552  chtppilim  23660  dchrisum0lem1a  23671  dchrvmasumiflem1  23686  dchrisum0lem1b  23700  dchrisum0lem1  23701  mulog2sumlem2  23720  selberg3lem1  23742  pntrsumo1  23750  pntibndlem1  23774  pntibndlem3  23777  pntlemr  23787  pntlemj  23788  ostth3  23823  minvecolem3  25792  lnconi  26952  stoweidlem14  31796  stoweidlem34  31816  stoweidlem42  31824  stoweidlem51  31833  stoweidlem59  31841  stirlinglem5  31860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  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 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-rp 11250
  Copyright terms: Public domain W3C validator