Theorem rpgt0 11230

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

Step	Hyp	Ref	Expression
1		elrp 11221	. 2 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
2	1	simprbi 464	1 |- ( A e. RR+ -> 0 < A )

Syntax hints:   -> wi 4   e. wcel 1767   class class class wbr 4447   RRcr 9490   0cc0 9491   < clt 9627   RR+crp 11219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-rp 11220

This theorem is referenced by:  rpge0  11231  rpgecl  11244  0nrp  11249  rpgt0d  11258  0mod  11994  sgnrrp  12886  sqrlem2  13039  sqrlem4  13041  sqrlem6  13043  resqrex  13046  rpsqrtcl  13060  climconst  13328  rlimconst  13329  divrcnv  13626  blcntrps  20666  blcntr  20667  stdbdmet  20770  stdbdmopn  20772  prdsxmslem2  20783  metustidOLD  20813  metustid  20814  nmoix  20987  metdseq0  21109  lebnumii  21217  itgulm  22553  pilem2  22597  tanregt0  22675  logdmnrp  22766  cxple2  22822  asinneg  22961  asin1  22969  reasinsin  22971  atanbndlem  23000  atanbnd  23001  atan1  23003  rlimcnp  23039  chtrpcl  23193  ppiltx  23195  bposlem8  23310  pntlem3  23538  padicabvcxp  23561  0cnop  26590  0cnfn  26591  xdivpnfrp  27313  pnfinf  27405  signsplypnf  28163  rprisefaccl  28738  itg2gt0cn  29663  areacirclem1  29700  areacirclem4  29703  prdstotbnd  29909  prdsbnd2  29910  irrapxlem3  30380  neglt  31060  constlimc  31182  ioodvbdlimc1lem1  31277  fourierdlem45  31468  fourierdlem103  31526  fourierdlem104  31527  taupilem1  36776