Metamath Proof Explorer

Theorem hashfz

Description: Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014) (Proof shortened by Mario Carneiro, 15-Apr-2015)

Ref Expression
Assertion hashfz ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( 𝐴 ... 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 eluzel2 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐴 ∈ ℤ )
2 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℤ )
3 1z ⊢ 1 ∈ ℤ
4 zsubcl ⊢ ( ( 1 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 1 − 𝐴 ) ∈ ℤ )
5 3 1 4 sylancr ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 1 − 𝐴 ) ∈ ℤ )
6 fzen ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 1 − 𝐴 ) ∈ ℤ ) → ( 𝐴 ... 𝐵 ) ≈ ( ( 𝐴 + ( 1 − 𝐴 ) ) ... ( 𝐵 + ( 1 − 𝐴 ) ) ) )
7 1 2 5 6 syl3anc ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ... 𝐵 ) ≈ ( ( 𝐴 + ( 1 − 𝐴 ) ) ... ( 𝐵 + ( 1 − 𝐴 ) ) ) )
8 1 zcnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐴 ∈ ℂ )
9 ax-1cn ⊢ 1 ∈ ℂ
10 pncan3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 + ( 1 − 𝐴 ) ) = 1 )
11 8 9 10 sylancl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 + ( 1 − 𝐴 ) ) = 1 )
12 1cnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 1 ∈ ℂ )
13 2 zcnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℂ )
14 13 8 subcld ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
15 13 12 8 addsub12d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 + ( 1 − 𝐴 ) ) = ( 1 + ( 𝐵 − 𝐴 ) ) )
16 12 14 15 comraddd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 + ( 1 − 𝐴 ) ) = ( ( 𝐵 − 𝐴 ) + 1 ) )
17 11 16 oveq12d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 + ( 1 − 𝐴 ) ) ... ( 𝐵 + ( 1 − 𝐴 ) ) ) = ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) )
18 7 17 breqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ... 𝐵 ) ≈ ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) )
19 hasheni ⊢ ( ( 𝐴 ... 𝐵 ) ≈ ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) → ( ♯ ‘ ( 𝐴 ... 𝐵 ) ) = ( ♯ ‘ ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) ) )
20 18 19 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( 𝐴 ... 𝐵 ) ) = ( ♯ ‘ ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) ) )
21 uznn0sub ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 − 𝐴 ) ∈ ℕ0 )
22 peano2nn0 ⊢ ( ( 𝐵 − 𝐴 ) ∈ ℕ0 → ( ( 𝐵 − 𝐴 ) + 1 ) ∈ ℕ0 )
23 hashfz1 ⊢ ( ( ( 𝐵 − 𝐴 ) + 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) ) = ( ( 𝐵 − 𝐴 ) + 1 ) )
24 21 22 23 3syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) ) = ( ( 𝐵 − 𝐴 ) + 1 ) )
25 20 24 eqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( 𝐴 ... 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) + 1 ) )