Metamath Proof Explorer

Theorem fzomaxdif

Description: A bound on the separation of two points in a half-open range. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion fzomaxdif 
|- ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( abs ` ( A - B ) ) e. ( 0 ..^ ( D - C ) ) )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( A e. ( C ..^ D ) -> A e. ZZ )
2 1 zcnd 
 |-  ( A e. ( C ..^ D ) -> A e. CC )
3 elfzoelz 
 |-  ( B e. ( C ..^ D ) -> B e. ZZ )
4 3 zcnd 
 |-  ( B e. ( C ..^ D ) -> B e. CC )
5 abssub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
6 2 4 5 syl2an 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
7 6 adantr 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
8 fzomaxdiflem 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( abs ` ( B - A ) ) e. ( 0 ..^ ( D - C ) ) )
9 7 8 eqeltrd 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ A <_ B ) -> ( abs ` ( A - B ) ) e. ( 0 ..^ ( D - C ) ) )
10 fzomaxdiflem 
 |-  ( ( ( B e. ( C ..^ D ) /\ A e. ( C ..^ D ) ) /\ B <_ A ) -> ( abs ` ( A - B ) ) e. ( 0 ..^ ( D - C ) ) )
11 10 ancom1s 
 |-  ( ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) /\ B <_ A ) -> ( abs ` ( A - B ) ) e. ( 0 ..^ ( D - C ) ) )
12 1 zred 
 |-  ( A e. ( C ..^ D ) -> A e. RR )
13 3 zred 
 |-  ( B e. ( C ..^ D ) -> B e. RR )
14 letric 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B <_ A ) )
15 12 13 14 syl2an 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( A <_ B \/ B <_ A ) )
16 9 11 15 mpjaodan 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( abs ` ( A - B ) ) e. ( 0 ..^ ( D - C ) ) )