Theorem rpgt0 11260

Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)

Assertion

Ref	Expression
rpgt0

Proof of Theorem rpgt0

Step	Hyp	Ref	Expression
1		elrp 11251	. 2
2	1	simprbi 464	1

Syntax hints:  ->wi 4  e.wcel 1818   class class class wbr 4452  cr 9512  0cc0 9513  clt 9649  crp 11249

This theorem is referenced by:  rpge0  11261  rpgecl  11274  0nrp  11279  rpgt0d  11288  0mod  12027  sgnrrp  12924  sqrlem2  13077  sqrlem4  13079  sqrlem6  13081  resqrex  13084  rpsqrtcl  13098  climconst  13366  rlimconst  13367  divrcnv  13664  blcntrps  20915  blcntr  20916  stdbdmet  21019  stdbdmopn  21021  prdsxmslem2  21032  metustidOLD  21062  metustid  21063  nmoix  21236  metdseq0  21358  lebnumii  21466  itgulm  22803  pilem2  22847  tanregt0  22926  logdmnrp  23022  cxple2  23078  asinneg  23217  asin1  23225  reasinsin  23227  atanbndlem  23256  atanbnd  23257  atan1  23259  rlimcnp  23295  chtrpcl  23449  ppiltx  23451  bposlem8  23566  pntlem3  23794  padicabvcxp  23817  0cnop  26898  0cnfn  26899  xdivpnfrp  27629  pnfinf  27727  rprisefaccl  29145  itg2gt0cn  30070  areacirclem1  30107  areacirclem4  30110  prdstotbnd  30290  prdsbnd2  30291  irrapxlem3  30760  neglt  31467  constlimc  31630  ioodvbdlimc1lem1  31728  fourierdlem103  31992  fourierdlem104  31993  etransclem18  32035  etransclem46  32063  taupilem1  37696

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