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

Metamath Proof Explorer

Theorem 0exp0e1

Description: The zeroth power of zero equals one. See comment of exp0 . (Contributed by David A. Wheeler, 8-Dec-2018)

		Ref	Expression
	Assertion	0exp0e1	$⊢ 0^{0} = 1$

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		exp0	$⊢ 0 \in ℂ \to 0^{0} = 1$
3	1 2	ax-mp	$⊢ 0^{0} = 1$