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