Theorem 0cxp

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

	Ref	Expression
Assertion	0cxp	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to 0^A=0$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		cxpval	$$⊢\left(0\in ℂ\wedge A\in ℂ\right)\to 0^A=if\left(0=0,if\left(A=0,1,0\right),{\mathrm{e}}^{A\log 0}\right)$$
3	1 2	mpan	$$⊢A\in ℂ\to 0^A=if\left(0=0,if\left(A=0,1,0\right),{\mathrm{e}}^{A\log 0}\right)$$
4		eqid	$$⊢0=0$$
5	4	iftruei	$$⊢if\left(0=0,if\left(A=0,1,0\right),{\mathrm{e}}^{A\log 0}\right)=if\left(A=0,1,0\right)$$
6	3 5	eqtrdi	$$⊢A\in ℂ\to 0^A=if\left(A=0,1,0\right)$$
7		ifnefalse	$$⊢A\ne 0\to if\left(A=0,1,0\right)=0$$
8	6 7	sylan9eq	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to 0^A=0$$