Theorem cxpexp

Description: Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Assertion	cxpexp	$$⊢\left(A\in ℂ\wedge B\in {\mathbb{N}}_0\right)\to A^B=A^B$$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢B\in {\mathbb{N}}_0\leftrightarrow \left(B\in \mathbb{N}\vee B=0\right)$$
2		nncn	$$⊢B\in \mathbb{N}\to B\in ℂ$$
3		nnne0	$$⊢B\in \mathbb{N}\to B\ne 0$$
4		0cxp	$$⊢\left(B\in ℂ\wedge B\ne 0\right)\to 0^B=0$$
5	2 3 4	syl2anc	$$⊢B\in \mathbb{N}\to 0^B=0$$
6		0exp	$$⊢B\in \mathbb{N}\to 0^B=0$$
7	5 6	eqtr4d	$$⊢B\in \mathbb{N}\to 0^B=0^B$$
8		0cn	$$⊢0\in ℂ$$
9		cxpval	$$⊢\left(0\in ℂ\wedge 0\in ℂ\right)\to 0^0=if\left(0=0,if\left(0=0,1,0\right),{\mathrm{e}}^{0\cdot \log 0}\right)$$
10	8 8 9	mp2an	$$⊢0^0=if\left(0=0,if\left(0=0,1,0\right),{\mathrm{e}}^{0\cdot \log 0}\right)$$
11		eqid	$$⊢0=0$$
12	11	iftruei	$$⊢if\left(0=0,if\left(0=0,1,0\right),{\mathrm{e}}^{0\cdot \log 0}\right)=if\left(0=0,1,0\right)$$
13	11	iftruei	$$⊢if\left(0=0,1,0\right)=1$$
14	10 12 13	3eqtri	$$⊢0^0=1$$
15		0exp0e1	$$⊢0^0=1$$
16	14 15	eqtr4i	$$⊢0^0=0^0$$
17		oveq2	$$⊢B=0\to 0^B=0^0$$
18		oveq2	$$⊢B=0\to 0^B=0^0$$
19	16 17 18	3eqtr4a	$$⊢B=0\to 0^B=0^B$$
20	7 19	jaoi	$$⊢\left(B\in \mathbb{N}\vee B=0\right)\to 0^B=0^B$$
21	1 20	sylbi	$$⊢B\in {\mathbb{N}}_0\to 0^B=0^B$$
22		oveq1	$$⊢A=0\to A^B=0^B$$
23		oveq1	$$⊢A=0\to A^B=0^B$$
24	22 23	eqeq12d	$$⊢A=0\to \left(A^B=A^B\leftrightarrow 0^B=0^B\right)$$
25	21 24	syl5ibrcom	$$⊢B\in {\mathbb{N}}_0\to \left(A=0\to A^B=A^B\right)$$
26	25	adantl	$$⊢\left(A\in ℂ\wedge B\in {\mathbb{N}}_0\right)\to \left(A=0\to A^B=A^B\right)$$
27	26	imp	$$⊢\left(\left(A\in ℂ\wedge B\in {\mathbb{N}}_0\right)\wedge A=0\right)\to A^B=A^B$$
28		nn0z	$$⊢B\in {\mathbb{N}}_0\to B\in \mathbb{Z}$$
29		cxpexpz	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in \mathbb{Z}\right)\to A^B=A^B$$
30	29	3expa	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge B\in \mathbb{Z}\right)\to A^B=A^B$$
31	28 30	sylan2	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge B\in {\mathbb{N}}_0\right)\to A^B=A^B$$
32	31	an32s	$$⊢\left(\left(A\in ℂ\wedge B\in {\mathbb{N}}_0\right)\wedge A\ne 0\right)\to A^B=A^B$$
33	27 32	pm2.61dane	$$⊢\left(A\in ℂ\wedge B\in {\mathbb{N}}_0\right)\to A^B=A^B$$