This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 )