Metamath Proof Explorer

Theorem fzsdom2

Description: Condition for finite ranges to have a strict dominance relation. (Contributed by Stefan O'Rear, 12-Sep-2014) (Revised by Mario Carneiro, 15-Apr-2015)

Ref Expression
Assertion fzsdom2 ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → A … B ≺ A … C

Proof

Step Hyp Ref Expression
1 eluzelz ⊢ B ∈ ℤ ≥ A → B ∈ ℤ
2 1 ad2antrr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → B ∈ ℤ
3 2 zred ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → B ∈ ℝ
4 eluzel2 ⊢ B ∈ ℤ ≥ A → A ∈ ℤ
5 4 ad2antrr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → A ∈ ℤ
6 5 zred ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → A ∈ ℝ
7 3 6 resubcld ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → B − A ∈ ℝ
8 simplr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → C ∈ ℤ
9 8 zred ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → C ∈ ℝ
10 9 6 resubcld ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → C − A ∈ ℝ
11 1red ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → 1 ∈ ℝ
12 simpr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → B < C
13 3 9 6 12 ltsub1dd ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → B − A < C − A
14 7 10 11 13 ltadd1dd ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → B - A + 1 < C - A + 1
15 hashfz ⊢ B ∈ ℤ ≥ A → A … B = B - A + 1
16 15 ad2antrr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → A … B = B - A + 1
17 3 9 12 ltled ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → B ≤ C
18 eluz2 ⊢ C ∈ ℤ ≥ B ↔ B ∈ ℤ ∧ C ∈ ℤ ∧ B ≤ C
19 2 8 17 18 syl3anbrc ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → C ∈ ℤ ≥ B
20 simpll ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → B ∈ ℤ ≥ A
21 uztrn ⊢ C ∈ ℤ ≥ B ∧ B ∈ ℤ ≥ A → C ∈ ℤ ≥ A
22 19 20 21 syl2anc ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → C ∈ ℤ ≥ A
23 hashfz ⊢ C ∈ ℤ ≥ A → A … C = C - A + 1
24 22 23 syl ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → A … C = C - A + 1
25 14 16 24 3brtr4d ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → A … B < A … C
26 fzfi ⊢ A … B ∈ Fin
27 fzfi ⊢ A … C ∈ Fin
28 hashsdom ⊢ A … B ∈ Fin ∧ A … C ∈ Fin → A … B < A … C ↔ A … B ≺ A … C
29 26 27 28 mp2an ⊢ A … B < A … C ↔ A … B ≺ A … C
30 25 29 sylib ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℤ ∧ B < C → A … B ≺ A … C