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 ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B ∈ 0 ..^ D − C

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ A ∈ C ..^ D → A ∈ ℤ
2 1 zcnd ⊢ A ∈ C ..^ D → A ∈ ℂ
3 elfzoelz ⊢ B ∈ C ..^ D → B ∈ ℤ
4 3 zcnd ⊢ B ∈ C ..^ D → B ∈ ℂ
5 abssub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B = B − A
6 2 4 5 syl2an ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B = B − A
7 6 adantr ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D ∧ A ≤ B → A − B = B − A
8 fzomaxdiflem ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D ∧ A ≤ B → B − A ∈ 0 ..^ D − C
9 7 8 eqeltrd ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D ∧ A ≤ B → A − B ∈ 0 ..^ D − C
10 fzomaxdiflem ⊢ B ∈ C ..^ D ∧ A ∈ C ..^ D ∧ B ≤ A → A − B ∈ 0 ..^ D − C
11 10 ancom1s ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D ∧ B ≤ A → A − B ∈ 0 ..^ D − C
12 1 zred ⊢ A ∈ C ..^ D → A ∈ ℝ
13 3 zred ⊢ B ∈ C ..^ D → B ∈ ℝ
14 letric ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∨ B ≤ A
15 12 13 14 syl2an ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A ≤ B ∨ B ≤ A
16 9 11 15 mpjaodan ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D → A − B ∈ 0 ..^ D − C