Theorem rpgt0 9807

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 9797	. 2 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
2	1	simprbi 275	1 |- ( A e. RR+ -> 0 < A )

Syntax hints:   -> wi 4   e. wcel 2177   class class class wbr 4051   RRcr 7944   0cc0 7945   < clt 8127   RR+crp 9795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052  df-rp 9796

This theorem is referenced by:  rpge0  9808  rpap0  9812  rpgecl  9824  0nrp  9831  rpgt0d  9841  addlelt  9910  rpsqrtcl  11427  rpmaxcl  11609  rpmincl  11624  xrminrpcl  11660  climconst  11676  sinltxirr  12147  blcntrps  14962  blcntr  14963  bdmet  15049  bdmopn  15051  reeff1o  15320  coseq00topi  15382  coseq0negpitopi  15383