Theorem hashfzo0

Description: Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015)

	Ref	Expression
Assertion	hashfzo0	⊢ ( 𝐵 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝐵 ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		hashfzo	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ ( 0 ..^ 𝐵 ) ) = ( 𝐵 − 0 ) )
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3	1 2	eleq2s	⊢ ( 𝐵 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝐵 ) ) = ( 𝐵 − 0 ) )
4		nn0cn	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℂ )
5	4	subid1d	⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 − 0 ) = 𝐵 )
6	3 5	eqtrd	⊢ ( 𝐵 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝐵 ) ) = 𝐵 )