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 ∈ C ..^ D ∧ B ∈ C ..^ D → D − C ∥ A − B ↔ A = B

Proof

Step Hyp Ref Expression
1 elfzoel2 ⊢ B ∈ C ..^ D → D ∈ ℤ
2 elfzoel1 ⊢ B ∈ C ..^ D → C ∈ ℤ
3 1 2 zsubcld ⊢ B ∈ C ..^ D → D − C ∈ ℤ
4 elfzoelz ⊢ A ∈ C ..^ D → A ∈ ℤ
5 elfzoelz ⊢ B ∈ C ..^ D → B ∈ ℤ
6 zsubcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A − B ∈ ℤ
7 4 5 6 syl2an ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B ∈ ℤ
8 dvdsabsb ⊢ D − C ∈ ℤ ∧ A − B ∈ ℤ → D − C ∥ A − B ↔ D − C ∥ A − B
9 3 7 8 syl2an2 ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → D − C ∥ A − B ↔ D − C ∥ A − B
10 fzomaxdif ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B ∈ 0 ..^ D − C
11 fzo0dvdseq ⊢ A − B ∈ 0 ..^ D − C → D − C ∥ A − B ↔ A − B = 0
12 10 11 syl ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → D − C ∥ A − B ↔ A − B = 0
13 9 12 bitrd ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → D − C ∥ A − B ↔ A − B = 0
14 4 zcnd ⊢ A ∈ C ..^ D → A ∈ ℂ
15 5 zcnd ⊢ B ∈ C ..^ D → B ∈ ℂ
16 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
17 14 15 16 syl2an ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B ∈ ℂ
18 17 abs00ad ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B = 0 ↔ A − B = 0
19 subeq0 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B = 0 ↔ A = B
20 14 15 19 syl2an ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B = 0 ↔ A = B
21 18 20 bitrd ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B = 0 ↔ A = B
22 13 21 bitrd ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → D − C ∥ A − B ↔ A = B