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