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	|- C e. R.
Assertion	ltpsrpr	|- ( ( C +R [ <. A , 1P >. ] ~R ) . ] ~R ) <-> A

Proof

Step	Hyp	Ref	Expression
1		ltpsrpr.3	|- C e. R.
2		ltasr	|- ( C e. R. -> ( [ <. A , 1P >. ] ~R . ] ~R <-> ( C +R [ <. A , 1P >. ] ~R ) . ] ~R ) ) )
3	1 2	ax-mp	|- ( [ <. A , 1P >. ] ~R . ] ~R <-> ( C +R [ <. A , 1P >. ] ~R ) . ] ~R ) )
4		addcompr	|- ( A +P. 1P ) = ( 1P +P. A )
5	4	breq1i	|- ( ( A +P. 1P ) ( 1P +P. A )
6		ltsrpr	|- ( [ <. A , 1P >. ] ~R . ] ~R <-> ( A +P. 1P )
7		1pr	|- 1P e. P.
8		ltapr	|- ( 1P e. P. -> ( A ( 1P +P. A )
9	7 8	ax-mp	|- ( A ( 1P +P. A )
10	5 6 9	3bitr4i	|- ( [ <. A , 1P >. ] ~R . ] ~R <-> A
11	3 10	bitr3i	|- ( ( C +R [ <. A , 1P >. ] ~R ) . ] ~R ) <-> A