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 ) )