Theorem numexp2x

Description: Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015)

	Ref	Expression
Hypotheses	numexp.1	$$⊢A\in {\mathbb{N}}_0$$
	numexpp1.2	$$⊢M\in {\mathbb{N}}_0$$
	numexp2x.3	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=N$$
	numexp2x.4	$$⊢A^M=D$$
	numexp2x.5	$$⊢DD=C$$
Assertion	numexp2x	$$⊢A^N=C$$

Proof

Step	Hyp	Ref	Expression
1		numexp.1	$$⊢A\in {\mathbb{N}}_0$$
2		numexpp1.2	$$⊢M\in {\mathbb{N}}_0$$
3		numexp2x.3	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=N$$
4		numexp2x.4	$$⊢A^M=D$$
5		numexp2x.5	$$⊢DD=C$$
6	2	nn0cni	$$⊢M\in ℂ$$
7	6	2timesi	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M+M$$
8	3 7	eqtr3i	$$⊢N=M+M$$
9	8	oveq2i	$$⊢A^N=A^{M+M}$$
10	1	nn0cni	$$⊢A\in ℂ$$
11		expadd	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to A^{M+M}=A^M{A}^M$$
12	10 2 2 11	mp3an	$$⊢A^{M+M}=A^M{A}^M$$
13	9 12	eqtri	$$⊢A^N=A^M{A}^M$$
14	4 4	oveq12i	$$⊢A^M{A}^M=DD$$
15	14 5	eqtri	$$⊢A^M{A}^M=C$$
16	13 15	eqtri	$$⊢A^N=C$$