This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( ( 𝐷 − 𝐶 ) ∥ ( 𝐴 − 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

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