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