Theorem rpgt0 11256

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 11247	. 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 1819   class class class wbr 4456   RRcr 9508   0cc0 9509   < clt 9645   RR+crp 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  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 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-rp 11246

This theorem is referenced by:  rpge0  11257  rpgecl  11270  0nrp  11275  rpgt0d  11284  0mod  12029  sgnrrp  12935  sqrlem2  13088  sqrlem4  13090  sqrlem6  13092  resqrex  13095  rpsqrtcl  13109  climconst  13377  rlimconst  13378  divrcnv  13675  blcntrps  21040  blcntr  21041  stdbdmet  21144  stdbdmopn  21146  prdsxmslem2  21157  metustidOLD  21187  metustid  21188  nmoix  21361  metdseq0  21483  lebnumii  21591  itgulm  22928  pilem2  22972  tanregt0  23051  logdmnrp  23147  cxple2  23203  asinneg  23342  asin1  23350  reasinsin  23352  atanbndlem  23381  atanbnd  23382  atan1  23384  rlimcnp  23420  chtrpcl  23574  ppiltx  23576  bposlem8  23691  pntlem3  23919  padicabvcxp  23942  0cnop  27024  0cnfn  27025  xdivpnfrp  27781  pnfinf  27879  rprisefaccl  29320  itg2gt0cn  30232  areacirclem1  30269  areacirclem4  30272  prdstotbnd  30452  prdsbnd2  30453  irrapxlem3  30922  neglt  31628  constlimc  31791  ioodvbdlimc1lem1  31889  fourierdlem103  32153  fourierdlem104  32154  etransclem18  32196  etransclem46  32224  taupilem1  37797