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 [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ↔ 𝐵 <P 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ltsrpr	⊢ ( [ ⟨ 1P , 1P ⟩ ] ~R <R [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ↔ ( 1P +P 𝐵 ) <P ( 1P +P 𝐴 ) )
2		df-0r	⊢ 0R = [ ⟨ 1P , 1P ⟩ ] ~R
3	2	breq1i	⊢ ( 0R <R [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ↔ [ ⟨ 1P , 1P ⟩ ] ~R <R [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R )
4		1pr	⊢ 1P ∈ P
5		ltapr	⊢ ( 1P ∈ P → ( 𝐵 <P 𝐴 ↔ ( 1P +P 𝐵 ) <P ( 1P +P 𝐴 ) ) )
6	4 5	ax-mp	⊢ ( 𝐵 <P 𝐴 ↔ ( 1P +P 𝐵 ) <P ( 1P +P 𝐴 ) )
7	1 3 6	3bitr4i	⊢ ( 0R <R [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ↔ 𝐵 <P 𝐴 )