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

Metamath Proof Explorer

Theorem mappsrpr

Description: Mapping 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 mappsrpr.2 ⊢ 𝐶 ∈ R
Assertion mappsrpr ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝐴 , 1P ⟩ ] ~R ) ↔ 𝐴 ∈ P )

Proof

Step Hyp Ref Expression
1 mappsrpr.2 ⊢ 𝐶 ∈ R
2 df-m1r ⊢ -1R = [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R
3 2 breq1i ⊢ ( -1R <R [ ⟨ 𝐴 , 1P ⟩ ] ~R ↔ [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R <R [ ⟨ 𝐴 , 1P ⟩ ] ~R )
4 ltsrpr ⊢ ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R <R [ ⟨ 𝐴 , 1P ⟩ ] ~R ↔ ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 𝐴 ) )
5 3 4 bitri ⊢ ( -1R <R [ ⟨ 𝐴 , 1P ⟩ ] ~R ↔ ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 𝐴 ) )
6 ltasr ⊢ ( 𝐶 ∈ R → ( -1R <R [ ⟨ 𝐴 , 1P ⟩ ] ~R ↔ ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝐴 , 1P ⟩ ] ~R ) ) )
7 1 6 ax-mp ⊢ ( -1R <R [ ⟨ 𝐴 , 1P ⟩ ] ~R ↔ ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝐴 , 1P ⟩ ] ~R ) )
8 ltrelpr ⊢ <P ⊆ ( P × P )
9 8 brel ⊢ ( ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 𝐴 ) → ( ( 1P +P 1P ) ∈ P ∧ ( ( 1P +P 1P ) +P 𝐴 ) ∈ P ) )
10 dmplp ⊢ dom +P = ( P × P )
11 0npr ⊢ ¬ ∅ ∈ P
12 10 11 ndmovrcl ⊢ ( ( ( 1P +P 1P ) +P 𝐴 ) ∈ P → ( ( 1P +P 1P ) ∈ P ∧ 𝐴 ∈ P ) )
13 12 simprd ⊢ ( ( ( 1P +P 1P ) +P 𝐴 ) ∈ P → 𝐴 ∈ P )
14 9 13 simpl2im ⊢ ( ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 𝐴 ) → 𝐴 ∈ P )
15 1pr ⊢ 1P ∈ P
16 addclpr ⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) ∈ P )
17 15 15 16 mp2an ⊢ ( 1P +P 1P ) ∈ P
18 ltaddpr ⊢ ( ( ( 1P +P 1P ) ∈ P ∧ 𝐴 ∈ P ) → ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 𝐴 ) )
19 17 18 mpan ⊢ ( 𝐴 ∈ P → ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 𝐴 ) )
20 14 19 impbii ⊢ ( ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 𝐴 ) ↔ 𝐴 ∈ P )
21 5 7 20 3bitr3i ⊢ ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝐴 , 1P ⟩ ] ~R ) ↔ 𝐴 ∈ P )