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 AC..^DBC..^DDCABA=B

Proof

Step Hyp Ref Expression
1 elfzoel2 BC..^DD
2 elfzoel1 BC..^DC
3 1 2 zsubcld BC..^DDC
4 elfzoelz AC..^DA
5 elfzoelz BC..^DB
6 zsubcl ABAB
7 4 5 6 syl2an AC..^DBC..^DAB
8 dvdsabsb DCABDCABDCAB
9 3 7 8 syl2an2 AC..^DBC..^DDCABDCAB
10 fzomaxdif AC..^DBC..^DAB0..^DC
11 fzo0dvdseq AB0..^DCDCABAB=0
12 10 11 syl AC..^DBC..^DDCABAB=0
13 9 12 bitrd AC..^DBC..^DDCABAB=0
14 4 zcnd AC..^DA
15 5 zcnd BC..^DB
16 subcl ABAB
17 14 15 16 syl2an AC..^DBC..^DAB
18 17 abs00ad AC..^DBC..^DAB=0AB=0
19 subeq0 ABAB=0A=B
20 14 15 19 syl2an AC..^DBC..^DAB=0A=B
21 18 20 bitrd AC..^DBC..^DAB=0A=B
22 13 21 bitrd AC..^DBC..^DDCABA=B