Metamath Proof Explorer

Theorem fzocongeq

Description: Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion fzocongeq 
|- ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( D - C ) || ( A - B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 elfzoel2 
 |-  ( B e. ( C ..^ D ) -> D e. ZZ )
2 elfzoel1 
 |-  ( B e. ( C ..^ D ) -> C e. ZZ )
3 1 2 zsubcld 
 |-  ( B e. ( C ..^ D ) -> ( D - C ) e. ZZ )
4 elfzoelz 
 |-  ( A e. ( C ..^ D ) -> A e. ZZ )
5 elfzoelz 
 |-  ( B e. ( C ..^ D ) -> B e. ZZ )
6 zsubcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )
7 4 5 6 syl2an 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( A - B ) e. ZZ )
8 dvdsabsb 
 |-  ( ( ( D - C ) e. ZZ /\ ( A - B ) e. ZZ ) -> ( ( D - C ) || ( A - B ) <-> ( D - C ) || ( abs ` ( A - B ) ) ) )
9 3 7 8 syl2an2 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( D - C ) || ( A - B ) <-> ( D - C ) || ( abs ` ( A - B ) ) ) )
10 fzomaxdif 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( abs ` ( A - B ) ) e. ( 0 ..^ ( D - C ) ) )
11 fzo0dvdseq 
 |-  ( ( abs ` ( A - B ) ) e. ( 0 ..^ ( D - C ) ) -> ( ( D - C ) || ( abs ` ( A - B ) ) <-> ( abs ` ( A - B ) ) = 0 ) )
12 10 11 syl 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( D - C ) || ( abs ` ( A - B ) ) <-> ( abs ` ( A - B ) ) = 0 ) )
13 9 12 bitrd 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( D - C ) || ( A - B ) <-> ( abs ` ( A - B ) ) = 0 ) )
14 4 zcnd 
 |-  ( A e. ( C ..^ D ) -> A e. CC )
15 5 zcnd 
 |-  ( B e. ( C ..^ D ) -> B e. CC )
16 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
17 14 15 16 syl2an 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( A - B ) e. CC )
18 17 abs00ad 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( abs ` ( A - B ) ) = 0 <-> ( A - B ) = 0 ) )
19 subeq0 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) = 0 <-> A = B ) )
20 14 15 19 syl2an 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( A - B ) = 0 <-> A = B ) )
21 18 20 bitrd 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( abs ` ( A - B ) ) = 0 <-> A = B ) )
22 13 21 bitrd 
 |-  ( ( A e. ( C ..^ D ) /\ B e. ( C ..^ D ) ) -> ( ( D - C ) || ( A - B ) <-> A = B ) )