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	⊢ ( 𝐵 ∈ ( ℤ_≥ ‘ 𝐴 ) → ( 𝐵 − 𝐴 ) ∈ ℕ₀ )
22		peano2nn0	⊢ ( ( 𝐵 − 𝐴 ) ∈ ℕ₀ → ( ( 𝐵 − 𝐴 ) + 1 ) ∈ ℕ₀ )
23		hashfz1	⊢ ( ( ( 𝐵 − 𝐴 ) + 1 ) ∈ ℕ₀ → ( ♯ ‘ ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) ) = ( ( 𝐵 − 𝐴 ) + 1 ) )
24	21 22 23	3syl	⊢ ( 𝐵 ∈ ( ℤ_≥ ‘ 𝐴 ) → ( ♯ ‘ ( 1 ... ( ( 𝐵 − 𝐴 ) + 1 ) ) ) = ( ( 𝐵 − 𝐴 ) + 1 ) )
25	20 24	eqtrd	⊢ ( 𝐵 ∈ ( ℤ_≥ ‘ 𝐴 ) → ( ♯ ‘ ( 𝐴 ... 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) + 1 ) )

Metamath Proof Explorer

Theorem hashfz

Proof