Theorem numexpp1

Description: Calculate 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$$
	numexpp1.3	$$⊢M+1=N$$
	numexpp1.4	$$⊢A^{M}A=C$$
Assertion	numexpp1	$$⊢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		numexpp1.3	$$⊢M+1=N$$
4		numexpp1.4	$$⊢A^{M}A=C$$
5	1	nn0cni	$$⊢A\in ℂ$$
6		expp1	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+1}=A^{M}A$$
7	5 2 6	mp2an	$$⊢A^{M+1}=A^{M}A$$
8	3	oveq2i	$$⊢A^{M+1}=A^N$$
9	7 8 4	3eqtr3i	$$⊢A^N=C$$