This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℕ_{0} \to \|(0 ..^B)\| = B$

Step	Hyp	Ref	Expression
1		hashfzo	$⊢ B \in ℤ_{\geq 0} \to \|(0 ..^B)\| = B - 0$
2		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
3	1 2	eleq2s	$⊢ B \in ℕ_{0} \to \|(0 ..^B)\| = B - 0$
4		nn0cn	$⊢ B \in ℕ_{0} \to B \in ℂ$
5	4	subid1d	$⊢ B \in ℕ_{0} \to B - 0 = B$
6	3 5	eqtrd	$⊢ B \in ℕ_{0} \to \|(0 ..^B)\| = B$