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

Theorem rpgt0 10381
Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
Assertion
Ref Expression
rpgt0  |-  ( A  e.  RR+  ->  0  < 
A )

Proof of Theorem rpgt0
StepHypRef Expression
1 elrp 10372 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
21simprbi 450 1  |-  ( A  e.  RR+  ->  0  < 
A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   class class class wbr 4039   RRcr 8752   0cc0 8753    < clt 8883   RR+crp 10370
This theorem is referenced by:  rpge0  10382  rpgecl  10395  0nrp  10400  rpgt0d  10409  0mod  11011  sqrlem2  11745  sqrlem4  11747  sqrlem6  11749  resqrex  11752  rpsqrcl  11766  climconst  12033  rlimconst  12034  divrcnv  12327  blcntr  17980  stdbdmet  18078  stdbdmopn  18080  prdsxmslem2  18091  nmoix  18254  metdseq0  18374  lebnumii  18480  itgulm  19800  pilem2  19844  tanregt0  19917  logdmnrp  20004  cxple2  20060  asinneg  20198  asin1  20206  reasinsin  20208  atanbndlem  20237  atanbnd  20238  atan1  20240  rlimcnp  20276  chtrpcl  20429  ppiltx  20431  bposlem8  20546  pntlem3  20774  padicabvcxp  20797  0cnop  22575  0cnfn  22576  xdivpnfrp  23133  itg2addnclem  25003  itg2gt0cn  25006  areacirclem2  25028  areacirclem5  25032  prdstotbnd  26621  prdsbnd2  26622  irrapxlem3  27012  stoweidlem1  27853  stoweidlem3  27855  stoweidlem7  27859  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem18  27870  stoweidlem25  27877  stoweidlem26  27878  stoweidlem34  27886  stoweidlem42  27894  stoweidlem49  27901  stoweidlem51  27903  stoweidlem52  27904  stoweidlem59  27911  stoweidlem60  27912  sgnrrp  28502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-rp 10371
  Copyright terms: Public domain W3C validator