Theorem rpgt0 11014

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 11005	. 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 1756   class class class wbr 4304   RRcr 9293   0cc0 9294   < clt 9430   RR+crp 11003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-rp 11004

This theorem is referenced by:  rpge0  11015  rpgecl  11028  0nrp  11033  rpgt0d  11042  0mod  11751  sgnrrp  12592  sqrlem2  12745  sqrlem4  12747  sqrlem6  12749  resqrex  12752  rpsqrcl  12766  climconst  13033  rlimconst  13034  divrcnv  13327  blcntrps  19999  blcntr  20000  stdbdmet  20103  stdbdmopn  20105  prdsxmslem2  20116  metustidOLD  20146  metustid  20147  nmoix  20320  metdseq0  20442  lebnumii  20550  itgulm  21885  pilem2  21929  tanregt0  22007  logdmnrp  22098  cxple2  22154  asinneg  22293  asin1  22301  reasinsin  22303  atanbndlem  22332  atanbnd  22333  atan1  22335  rlimcnp  22371  chtrpcl  22525  ppiltx  22527  bposlem8  22642  pntlem3  22870  padicabvcxp  22893  0cnop  25395  0cnfn  25396  xdivpnfrp  26120  pnfinf  26212  signsplypnf  26963  rprisefaccl  27538  itg2gt0cn  28459  areacirclem1  28496  areacirclem4  28499  prdstotbnd  28705  prdsbnd2  28706  irrapxlem3  29177  taupilem1  35627