This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi 
 |-  ( ( ( ( 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 )