Metamath Proof Explorer

Theorem icodiamlt

Description: Two elements in a half-open interval have separationstrictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Assertion icodiamlt 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) ) -> ( abs ` ( C - D ) ) < ( B - A ) )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( B e. RR -> B e. RR* )
2 elico2 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) )
3 elico2 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( D e. ( A [,) B ) <-> ( D e. RR /\ A <_ D /\ D < B ) ) )
4 2 3 anbi12d 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) <-> ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) )
5 4 biimpd 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) -> ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) )
6 1 5 sylan2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) -> ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) )
7 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> B e. RR )
8 7 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> B e. CC )
9 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> A e. RR )
10 9 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> A e. CC )
11 8 10 negsubdi2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> -u ( B - A ) = ( A - B ) )
12 9 7 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( A - B ) e. RR )
13 simprl1 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> C e. RR )
14 13 7 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( C - B ) e. RR )
15 simprr1 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> D e. RR )
16 13 15 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( C - D ) e. RR )
17 simprl2 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> A <_ C )
18 9 13 7 17 lesub1dd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( A - B ) <_ ( C - B ) )
19 simprr3 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> D < B )
20 15 7 13 19 ltsub2dd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( C - B ) < ( C - D ) )
21 12 14 16 18 20 lelttrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( A - B ) < ( C - D ) )
22 11 21 eqbrtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> -u ( B - A ) < ( C - D ) )
23 7 15 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( B - D ) e. RR )
24 7 9 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( B - A ) e. RR )
25 simprl3 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> C < B )
26 13 7 15 25 ltsub1dd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( C - D ) < ( B - D ) )
27 simprr2 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> A <_ D )
28 9 15 7 27 lesub2dd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( B - D ) <_ ( B - A ) )
29 16 23 24 26 28 ltletrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( C - D ) < ( B - A ) )
30 16 24 absltd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( ( abs ` ( C - D ) ) < ( B - A ) <-> ( -u ( B - A ) < ( C - D ) /\ ( C - D ) < ( B - A ) ) ) )
31 22 29 30 mpbir2and 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) ) -> ( abs ` ( C - D ) ) < ( B - A ) )
32 31 ex 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( C e. RR /\ A <_ C /\ C < B ) /\ ( D e. RR /\ A <_ D /\ D < B ) ) -> ( abs ` ( C - D ) ) < ( B - A ) ) )
33 6 32 syld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) -> ( abs ` ( C - D ) ) < ( B - A ) ) )
34 33 imp 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) ) -> ( abs ` ( C - D ) ) < ( B - A ) )