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 )