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