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	$$⊢B\in {\mathbb{N}}_0\to \left|\left(0\dots B\right)\right|=B+1$$

Proof

Step	Hyp	Ref	Expression
1		elnn0uz	$$⊢B\in {\mathbb{N}}_0\leftrightarrow B\in {\mathbb{Z}}_{\ge 0}$$
2		hashfz	$$⊢B\in {\mathbb{Z}}_{\ge 0}\to \left|\left(0\dots B\right)\right|=B-0+1$$
3	1 2	sylbi	$$⊢B\in {\mathbb{N}}_0\to \left|\left(0\dots B\right)\right|=B-0+1$$
4		nn0cn	$$⊢B\in {\mathbb{N}}_0\to B\in ℂ$$
5	4	subid1d	$$⊢B\in {\mathbb{N}}_0\to B-0=B$$
6	5	oveq1d	$$⊢B\in {\mathbb{N}}_0\to B-0+1=B+1$$
7	3 6	eqtrd	$$⊢B\in {\mathbb{N}}_0\to \left|\left(0\dots B\right)\right|=B+1$$