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

Proof

Step	Hyp	Ref	Expression
1		hashfzo	$$⊢B\in {\mathbb{Z}}_{\ge 0}\to \left|\left(0..^B\right)\right|=B-0$$
2		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3	1 2	eleq2s	$$⊢B\in {\mathbb{N}}_0\to \left|\left(0..^B\right)\right|=B-0$$
4		nn0cn	$$⊢B\in {\mathbb{N}}_0\to B\in ℂ$$
5	4	subid1d	$$⊢B\in {\mathbb{N}}_0\to B-0=B$$
6	3 5	eqtrd	$$⊢B\in {\mathbb{N}}_0\to \left|\left(0..^B\right)\right|=B$$