Description: Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | gt0srpr | |- ( 0R |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltsrpr | |- ( [ <. 1P , 1P >. ] ~R |
|
2 | df-0r | |- 0R = [ <. 1P , 1P >. ] ~R |
|
3 | 2 | breq1i | |- ( 0R |
4 | 1pr | |- 1P e. P. |
|
5 | ltapr | |- ( 1P e. P. -> ( B |
|
6 | 4 5 | ax-mp | |- ( B |
7 | 1 3 6 | 3bitr4i | |- ( 0R |