Theorem ltpsrpr

Description: Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ltpsrpr.3	⊢ 𝐶 ∈ R
Assertion	ltpsrpr	⊢ ( ( 𝐶 +R [ ⟨ 𝐴 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝐵 , 1P ⟩ ] ~R ) ↔ 𝐴 <P 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ltpsrpr.3	⊢ 𝐶 ∈ R
2		ltasr	⊢ ( 𝐶 ∈ R → ( [ ⟨ 𝐴 , 1P ⟩ ] ~R <R [ ⟨ 𝐵 , 1P ⟩ ] ~R ↔ ( 𝐶 +R [ ⟨ 𝐴 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝐵 , 1P ⟩ ] ~R ) ) )
3	1 2	ax-mp	⊢ ( [ ⟨ 𝐴 , 1P ⟩ ] ~R <R [ ⟨ 𝐵 , 1P ⟩ ] ~R ↔ ( 𝐶 +R [ ⟨ 𝐴 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝐵 , 1P ⟩ ] ~R ) )
4		addcompr	⊢ ( 𝐴 +P 1P ) = ( 1P +P 𝐴 )
5	4	breq1i	⊢ ( ( 𝐴 +P 1P ) <P ( 1P +P 𝐵 ) ↔ ( 1P +P 𝐴 ) <P ( 1P +P 𝐵 ) )
6		ltsrpr	⊢ ( [ ⟨ 𝐴 , 1P ⟩ ] ~R <R [ ⟨ 𝐵 , 1P ⟩ ] ~R ↔ ( 𝐴 +P 1P ) <P ( 1P +P 𝐵 ) )
7		1pr	⊢ 1P ∈ P
8		ltapr	⊢ ( 1P ∈ P → ( 𝐴 <P 𝐵 ↔ ( 1P +P 𝐴 ) <P ( 1P +P 𝐵 ) ) )
9	7 8	ax-mp	⊢ ( 𝐴 <P 𝐵 ↔ ( 1P +P 𝐴 ) <P ( 1P +P 𝐵 ) )
10	5 6 9	3bitr4i	⊢ ( [ ⟨ 𝐴 , 1P ⟩ ] ~R <R [ ⟨ 𝐵 , 1P ⟩ ] ~R ↔ 𝐴 <P 𝐵 )
11	3 10	bitr3i	⊢ ( ( 𝐶 +R [ ⟨ 𝐴 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝐵 , 1P ⟩ ] ~R ) ↔ 𝐴 <P 𝐵 )