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