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

Proof

Step Hyp Ref Expression
1 mappsrpr.2 
 |-  C e. R.
2 df-m1r 
 |-  -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
3 2 breq1i 
 |-  ( -1R . ] ~R <-> [ <. 1P , ( 1P +P. 1P ) >. ] ~R . ] ~R )
4 ltsrpr 
 |-  ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R . ] ~R <-> ( 1P +P. 1P )
5 3 4 bitri 
 |-  ( -1R . ] ~R <-> ( 1P +P. 1P )
6 ltasr 
 |-  ( C e. R. -> ( -1R . ] ~R <-> ( C +R -1R ) . ] ~R ) ) )
7 1 6 ax-mp 
 |-  ( -1R . ] ~R <-> ( C +R -1R ) . ] ~R ) )
8 ltrelpr 
 |-
9 8 brel 
 |-  ( ( 1P +P. 1P ) 
 ( ( 1P +P. 1P ) e. P. /\ ( ( 1P +P. 1P ) +P. A ) e. P. ) )
10 dmplp 
 |-  dom +P. = ( P. X. P. )
11 0npr 
 |-  -. (/) e. P.
12 10 11 ndmovrcl 
 |-  ( ( ( 1P +P. 1P ) +P. A ) e. P. -> ( ( 1P +P. 1P ) e. P. /\ A e. P. ) )
13 12 simprd 
 |-  ( ( ( 1P +P. 1P ) +P. A ) e. P. -> A e. P. )
14 9 13 simpl2im 
 |-  ( ( 1P +P. 1P ) 
 A e. P. )
15 1pr 
 |-  1P e. P.
16 addclpr 
 |-  ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
17 15 15 16 mp2an 
 |-  ( 1P +P. 1P ) e. P.
18 ltaddpr 
 |-  ( ( ( 1P +P. 1P ) e. P. /\ A e. P. ) -> ( 1P +P. 1P )
19 17 18 mpan 
 |-  ( A e. P. -> ( 1P +P. 1P )
20 14 19 impbii 
 |-  ( ( 1P +P. 1P ) 
 A e. P. )
21 5 7 20 3bitr3i 
 |-  ( ( C +R -1R ) . ] ~R ) <-> A e. P. )