Metamath Proof Explorer


Theorem ltsrpr

Description: Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996) (Revised by Mario Carneiro, 12-Aug-2015) (New usage is discouraged.)

Ref Expression
Assertion ltsrpr
|- ( [ <. A , B >. ] ~R . ] ~R <-> ( A +P. D ) 


Proof

Step Hyp Ref Expression
1 enrer
 |-  ~R Er ( P. X. P. )
2 erdm
 |-  ( ~R Er ( P. X. P. ) -> dom ~R = ( P. X. P. ) )
3 1 2 ax-mp
 |-  dom ~R = ( P. X. P. )
4 df-nr
 |-  R. = ( ( P. X. P. ) /. ~R )
5 ltrelsr
 |-  
6 ltrelpr
 |-  

7 0npr
 |-  -. (/) e. P.
8 dmplp
 |-  dom +P. = ( P. X. P. )
9 enrex
 |-  ~R e. _V
10 df-ltr
 |-  . | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) 

11 addclpr
 |-  ( ( w e. P. /\ v e. P. ) -> ( w +P. v ) e. P. )
12 11 ad2ant2lr
 |-  ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( w +P. v ) e. P. )
13 addclpr
 |-  ( ( B e. P. /\ C e. P. ) -> ( B +P. C ) e. P. )
14 13 ad2ant2lr
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( B +P. C ) e. P. )
15 12 14 anim12ci
 |-  ( ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) /\ ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) )
16 15 an4s
 |-  ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) )
17 enreceq
 |-  ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) -> ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R <-> ( z +P. B ) = ( w +P. A ) ) )
18 enreceq
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. v , u >. ] ~R = [ <. C , D >. ] ~R <-> ( v +P. D ) = ( u +P. C ) ) )
19 eqcom
 |-  ( ( v +P. D ) = ( u +P. C ) <-> ( u +P. C ) = ( v +P. D ) )
20 18 19 bitrdi
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. v , u >. ] ~R = [ <. C , D >. ] ~R <-> ( u +P. C ) = ( v +P. D ) ) )
21 17 20 bi2anan9
 |-  ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) <-> ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) ) )
22 oveq12
 |-  ( ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) -> ( ( z +P. B ) +P. ( u +P. C ) ) = ( ( w +P. A ) +P. ( v +P. D ) ) )
23 addcompr
 |-  ( u +P. B ) = ( B +P. u )
24 23 oveq1i
 |-  ( ( u +P. B ) +P. C ) = ( ( B +P. u ) +P. C )
25 addasspr
 |-  ( ( u +P. B ) +P. C ) = ( u +P. ( B +P. C ) )
26 addasspr
 |-  ( ( B +P. u ) +P. C ) = ( B +P. ( u +P. C ) )
27 24 25 26 3eqtr3i
 |-  ( u +P. ( B +P. C ) ) = ( B +P. ( u +P. C ) )
28 27 oveq2i
 |-  ( z +P. ( u +P. ( B +P. C ) ) ) = ( z +P. ( B +P. ( u +P. C ) ) )
29 addasspr
 |-  ( ( z +P. u ) +P. ( B +P. C ) ) = ( z +P. ( u +P. ( B +P. C ) ) )
30 addasspr
 |-  ( ( z +P. B ) +P. ( u +P. C ) ) = ( z +P. ( B +P. ( u +P. C ) ) )
31 28 29 30 3eqtr4i
 |-  ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( z +P. B ) +P. ( u +P. C ) )
32 addcompr
 |-  ( v +P. A ) = ( A +P. v )
33 32 oveq1i
 |-  ( ( v +P. A ) +P. D ) = ( ( A +P. v ) +P. D )
34 addasspr
 |-  ( ( v +P. A ) +P. D ) = ( v +P. ( A +P. D ) )
35 addasspr
 |-  ( ( A +P. v ) +P. D ) = ( A +P. ( v +P. D ) )
36 33 34 35 3eqtr3i
 |-  ( v +P. ( A +P. D ) ) = ( A +P. ( v +P. D ) )
37 36 oveq2i
 |-  ( w +P. ( v +P. ( A +P. D ) ) ) = ( w +P. ( A +P. ( v +P. D ) ) )
38 addasspr
 |-  ( ( w +P. v ) +P. ( A +P. D ) ) = ( w +P. ( v +P. ( A +P. D ) ) )
39 addasspr
 |-  ( ( w +P. A ) +P. ( v +P. D ) ) = ( w +P. ( A +P. ( v +P. D ) ) )
40 37 38 39 3eqtr4i
 |-  ( ( w +P. v ) +P. ( A +P. D ) ) = ( ( w +P. A ) +P. ( v +P. D ) )
41 22 31 40 3eqtr4g
 |-  ( ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) -> ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) )
42 21 41 syl6bi
 |-  ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) -> ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) ) )
43 ovex
 |-  ( z +P. u ) e. _V
44 ovex
 |-  ( B +P. C ) e. _V
45 ltapr
 |-  ( f e. P. -> ( x 

( f +P. x )

46 ovex
 |-  ( w +P. v ) e. _V
47 addcompr
 |-  ( x +P. y ) = ( y +P. x )
48 ovex
 |-  ( A +P. D ) e. _V
49 43 44 45 46 47 48 caovord3
 |-  ( ( ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) /\ ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) ) -> ( ( z +P. u ) 

( A +P. D )

50 16 42 49 syl6an
 |-  ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) -> ( ( z +P. u ) 

( A +P. D )

51 9 1 4 10 50 brecop
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R . ] ~R <-> ( A +P. D ) 

52 3 4 5 6 7 8 51 brecop2
 |-  ( [ <. A , B >. ] ~R . ] ~R <-> ( A +P. D )