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