Metamath Proof Explorer


Theorem gt0srpr

Description: Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996) (New usage is discouraged.)

Ref Expression
Assertion gt0srpr
|- ( 0R . ] ~R <-> B 


Proof

Step Hyp Ref Expression
1 ltsrpr
 |-  ( [ <. 1P , 1P >. ] ~R . ] ~R <-> ( 1P +P. B ) 

2 df-0r
 |-  0R = [ <. 1P , 1P >. ] ~R
3 2 breq1i
 |-  ( 0R . ] ~R <-> [ <. 1P , 1P >. ] ~R . ] ~R )
4 1pr
 |-  1P e. P.
5 ltapr
 |-  ( 1P e. P. -> ( B 

( 1P +P. B )

6 4 5 ax-mp
 |-  ( B 

( 1P +P. B )

7 1 3 6 3bitr4i
 |-  ( 0R . ] ~R <-> B