Theorem hashfz0

Description: Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018)

	Ref	Expression
Assertion	hashfz0	⊢ ( 𝐵 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝐵 ) ) = ( 𝐵 + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0uz	⊢ ( 𝐵 ∈ ℕ0 ↔ 𝐵 ∈ ( ℤ≥ ‘ 0 ) )
2		hashfz	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ ( 0 ... 𝐵 ) ) = ( ( 𝐵 − 0 ) + 1 ) )
3	1 2	sylbi	⊢ ( 𝐵 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝐵 ) ) = ( ( 𝐵 − 0 ) + 1 ) )
4		nn0cn	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℂ )
5	4	subid1d	⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 − 0 ) = 𝐵 )
6	5	oveq1d	⊢ ( 𝐵 ∈ ℕ0 → ( ( 𝐵 − 0 ) + 1 ) = ( 𝐵 + 1 ) )
7	3 6	eqtrd	⊢ ( 𝐵 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝐵 ) ) = ( 𝐵 + 1 ) )