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

Theorem rpregt0d 11172
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 11166 . 2
31rpgt0d 11169 . 2
42, 3jca 532 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1758   class class class wbr 4409   cr 9418  0cc0 9419   clt 9555   crp 11130
This theorem is referenced by:  reclt1d  11179  recgt1d  11180  ltrecd  11184  lerecd  11185  ltrec1d  11186  lerec2d  11187  lediv2ad  11188  ltdiv2d  11189  lediv2d  11190  ledivdivd  11191  divge0d  11202  ltmul1d  11203  ltmul2d  11204  lemul1d  11205  lemul2d  11206  ltdiv1d  11207  lediv1d  11208  ltmuldivd  11209  ltmuldiv2d  11210  lemuldivd  11211  lemuldiv2d  11212  ltdivmuld  11213  ltdivmul2d  11214  ledivmuld  11215  ledivmul2d  11216  ltdiv23d  11222  lediv23d  11223  lt2mul2divd  11224  mertenslem1  13502  isprm6  13953  nmoi  20706  icopnfhmeo  20914  nmoleub2lem3  21069  lmnn  21173  ovolscalem1  21395  aaliou2b  22207  birthdaylem3  22747  fsumharmonic  22805  bcmono  23016  chtppilim  23124  dchrisum0lem1a  23135  dchrvmasumiflem1  23150  dchrisum0lem1b  23164  dchrisum0lem1  23165  mulog2sumlem2  23184  selberg3lem1  23206  pntrsumo1  23214  pntibndlem1  23238  pntibndlem3  23241  pntlemr  23251  pntlemj  23252  ostth3  23287  ttgcontlem1  23600  minvecolem3  24746  lnconi  25906  stoweidlem14  30543  stoweidlem34  30563  stoweidlem42  30571  stoweidlem51  30580  stoweidlem59  30588  stirlinglem5  30607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-br 4410  df-rp 11131
  Copyright terms: Public domain W3C validator