Theorem 0exp

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

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

Proof

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