Metamath Proof Explorer

Theorem ltasr

Description: Ordering property of addition. (Contributed by NM, 10-May-1996) (New usage is discouraged.)

Ref Expression
Assertion ltasr 
|- ( C e. R. -> ( A  ( C +R A )

Proof

Step Hyp Ref Expression
1 dmaddsr 
 |-  dom +R = ( R. X. R. )
2 ltrelsr 
 |-
3 0nsr 
 |-  -. (/) e. R.
4 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
5 oveq1 
 |-  ( [ <. v , u >. ] ~R = C -> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) = ( C +R [ <. x , y >. ] ~R ) )
6 oveq1 
 |-  ( [ <. v , u >. ] ~R = C -> ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) = ( C +R [ <. z , w >. ] ~R ) )
7 5 6 breq12d 
 |-  ( [ <. v , u >. ] ~R = C -> ( ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) . ] ~R +R [ <. z , w >. ] ~R ) <-> ( C +R [ <. x , y >. ] ~R ) . ] ~R ) ) )
8 7 bibi2d 
 |-  ( [ <. v , u >. ] ~R = C -> ( ( [ <. x , y >. ] ~R . ] ~R <-> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) . ] ~R +R [ <. z , w >. ] ~R ) ) <-> ( [ <. x , y >. ] ~R . ] ~R <-> ( C +R [ <. x , y >. ] ~R ) . ] ~R ) ) ) )
9 breq1 
 |-  ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R . ] ~R <-> A . ] ~R ) )
10 oveq2 
 |-  ( [ <. x , y >. ] ~R = A -> ( C +R [ <. x , y >. ] ~R ) = ( C +R A ) )
11 10 breq1d 
 |-  ( [ <. x , y >. ] ~R = A -> ( ( C +R [ <. x , y >. ] ~R ) . ] ~R ) <-> ( C +R A ) . ] ~R ) ) )
12 9 11 bibi12d 
 |-  ( [ <. x , y >. ] ~R = A -> ( ( [ <. x , y >. ] ~R . ] ~R <-> ( C +R [ <. x , y >. ] ~R ) . ] ~R ) ) <-> ( A . ] ~R <-> ( C +R A ) . ] ~R ) ) ) )
13 breq2 
 |-  ( [ <. z , w >. ] ~R = B -> ( A . ] ~R <-> A
14 oveq2 
 |-  ( [ <. z , w >. ] ~R = B -> ( C +R [ <. z , w >. ] ~R ) = ( C +R B ) )
15 14 breq2d 
 |-  ( [ <. z , w >. ] ~R = B -> ( ( C +R A ) . ] ~R ) <-> ( C +R A )
16 13 15 bibi12d 
 |-  ( [ <. z , w >. ] ~R = B -> ( ( A . ] ~R <-> ( C +R A ) . ] ~R ) ) <-> ( A  ( C +R A )
17 addclpr 
 |-  ( ( v e. P. /\ u e. P. ) -> ( v +P. u ) e. P. )
18 17 3ad2ant1 
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( v +P. u ) e. P. )
19 ltapr 
 |-  ( ( v +P. u ) e. P. -> ( ( x +P. w ) 
 ( ( v +P. u ) +P. ( x +P. w ) )
20 ltsrpr 
 |-  ( [ <. x , y >. ] ~R . ] ~R <-> ( x +P. w )
21 ltsrpr 
 |-  ( [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R . ] ~R <-> ( ( v +P. x ) +P. ( u +P. w ) )
22 vex 
 |-  v e. _V
23 vex 
 |-  x e. _V
24 vex 
 |-  u e. _V
25 addcompr 
 |-  ( y +P. z ) = ( z +P. y )
26 addasspr 
 |-  ( ( y +P. z ) +P. f ) = ( y +P. ( z +P. f ) )
27 vex 
 |-  w e. _V
28 22 23 24 25 26 27 caov4 
 |-  ( ( v +P. x ) +P. ( u +P. w ) ) = ( ( v +P. u ) +P. ( x +P. w ) )
29 addcompr 
 |-  ( ( u +P. y ) +P. ( v +P. z ) ) = ( ( v +P. z ) +P. ( u +P. y ) )
30 vex 
 |-  z e. _V
31 addcompr 
 |-  ( x +P. w ) = ( w +P. x )
32 addasspr 
 |-  ( ( x +P. w ) +P. f ) = ( x +P. ( w +P. f ) )
33 vex 
 |-  y e. _V
34 22 30 24 31 32 33 caov42 
 |-  ( ( v +P. z ) +P. ( u +P. y ) ) = ( ( v +P. u ) +P. ( y +P. z ) )
35 29 34 eqtri 
 |-  ( ( u +P. y ) +P. ( v +P. z ) ) = ( ( v +P. u ) +P. ( y +P. z ) )
36 28 35 breq12i 
 |-  ( ( ( v +P. x ) +P. ( u +P. w ) ) 
 ( ( v +P. u ) +P. ( x +P. w ) )
37 21 36 bitri 
 |-  ( [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R . ] ~R <-> ( ( v +P. u ) +P. ( x +P. w ) )
38 19 20 37 3bitr4g 
 |-  ( ( v +P. u ) e. P. -> ( [ <. x , y >. ] ~R . ] ~R <-> [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R . ] ~R ) )
39 18 38 syl 
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R . ] ~R <-> [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R . ] ~R ) )
40 addsrpr 
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) ) -> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) = [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R )
41 40 3adant3 
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) = [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R )
42 addsrpr 
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) = [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R )
43 42 3adant2 
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) = [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R )
44 41 43 breq12d 
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) . ] ~R +R [ <. z , w >. ] ~R ) <-> [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R . ] ~R ) )
45 39 44 bitr4d 
 |-  ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R . ] ~R <-> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) . ] ~R +R [ <. z , w >. ] ~R ) ) )
46 4 8 12 16 45 3ecoptocl 
 |-  ( ( C e. R. /\ A e. R. /\ B e. R. ) -> ( A  ( C +R A )
47 46 3coml 
 |-  ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( A  ( C +R A )
48 1 2 3 47 ndmovord 
 |-  ( C e. R. -> ( A  ( C +R A )