Theorem 0expd

Description: Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypothesis	0exp.1	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	0expd	$$⊢\phi \to 0^N=0$$

Proof

Step	Hyp	Ref	Expression
1		0exp.1	$$⊢\phi \to N\in \mathbb{N}$$
2		0exp	$$⊢N\in \mathbb{N}\to 0^N=0$$
3	1 2	syl	$$⊢\phi \to 0^N=0$$