Theorem fzomaxdif

Description: A bound on the separation of two points in a half-open range. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Assertion	fzomaxdif	⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	⊢ ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐴 ∈ ℤ )
2	1	zcnd	⊢ ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐴 ∈ ℂ )
3		elfzoelz	⊢ ( 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐵 ∈ ℤ )
4	3	zcnd	⊢ ( 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐵 ∈ ℂ )
5		abssub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
6	2 4 5	syl2an	⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
7	6	adantr	⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
8		fzomaxdiflem	⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )
9	7 8	eqeltrd	⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )
10		fzomaxdiflem	⊢ ( ( ( 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐵 ≤ 𝐴 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )
11	10	ancom1s	⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐵 ≤ 𝐴 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )
12	1	zred	⊢ ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐴 ∈ ℝ )
13	3	zred	⊢ ( 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐵 ∈ ℝ )
14		letric	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) )
15	12 13 14	syl2an	⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) )
16	9 11 15	mpjaodan	⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )