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

Metamath Proof Explorer

Theorem 0exp

Description: Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004)

		Ref	Expression
	Assertion	0exp	$⊢ N \in ℕ \to 0^{N} = 0$

Step	Hyp	Ref	Expression
1		eqid	$⊢ 0 = 0$
2		0cn	$⊢ 0 \in ℂ$
3		expeq0	$⊢ (0 \in ℂ \land N \in ℕ) \to (0^{N} = 0 \leftrightarrow 0 = 0)$
4	2 3	mpan	$⊢ N \in ℕ \to (0^{N} = 0 \leftrightarrow 0 = 0)$
5	1 4	mpbiri	$⊢ N \in ℕ \to 0^{N} = 0$