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

Metamath Proof Explorer

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 ..^ ( 𝐷 − 𝐶 ) ) )