Theorem cxp0

Description: Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Assertion	cxp0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 0 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		cxpexp	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 0 ) = ( 𝐴 ↑ 0 ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 0 ) = ( 𝐴 ↑ 0 ) )
4		exp0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
5	3 4	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 0 ) = 1 )