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

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 ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ℤ ) ∧ 𝐵 < 𝐶 ) → ( 𝐴 ... 𝐵 ) ≺ ( 𝐴 ... 𝐶 ) )

Proof

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