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	$$⊢0_{𝑹}{<}_{𝑹}\left[⟨A,B⟩\right]{~}_{𝑹}\leftrightarrow B{<}_{𝑷}A$$

Proof

Step	Hyp	Ref	Expression
1		ltsrpr	$$⊢\left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}{<}_{𝑹}\left[⟨A,B⟩\right]{~}_{𝑹}\leftrightarrow \left(1_{𝑷}{+}_{𝑷}B\right){<}_{𝑷}\left(1_{𝑷}{+}_{𝑷}A\right)$$
2		df-0r	$$⊢0_{𝑹}=\left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}$$
3	2	breq1i	$$⊢0_{𝑹}{<}_{𝑹}\left[⟨A,B⟩\right]{~}_{𝑹}\leftrightarrow \left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}{<}_{𝑹}\left[⟨A,B⟩\right]{~}_{𝑹}$$
4		1pr	$$⊢1_{𝑷}\in 𝑷$$
5		ltapr	$$⊢1_{𝑷}\in 𝑷\to \left(B{<}_{𝑷}A\leftrightarrow \left(1_{𝑷}{+}_{𝑷}B\right){<}_{𝑷}\left(1_{𝑷}{+}_{𝑷}A\right)\right)$$
6	4 5	ax-mp	$$⊢B{<}_{𝑷}A\leftrightarrow \left(1_{𝑷}{+}_{𝑷}B\right){<}_{𝑷}\left(1_{𝑷}{+}_{𝑷}A\right)$$
7	1 3 6	3bitr4i	$$⊢0_{𝑹}{<}_{𝑹}\left[⟨A,B⟩\right]{~}_{𝑹}\leftrightarrow B{<}_{𝑷}A$$