Theorem 0expd

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

	Ref	Expression
Hypothesis	0exp.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	0expd	⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		0exp.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		0exp	⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = 0 )
3	1 2	syl	⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) = 0 )