Theorem numexpp1

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

	Ref	Expression
Hypotheses	numexp.1	|- A e. NN0
	numexpp1.2	|- M e. NN0
	numexpp1.3	|- ( M + 1 ) = N
	numexpp1.4	|- ( ( A ^ M ) x. A ) = C
Assertion	numexpp1	|- ( A ^ N ) = C

Proof

Step	Hyp	Ref	Expression
1		numexp.1	|- A e. NN0
2		numexpp1.2	|- M e. NN0
3		numexpp1.3	|- ( M + 1 ) = N
4		numexpp1.4	|- ( ( A ^ M ) x. A ) = C
5	1	nn0cni	|- A e. CC
6		expp1	|- ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + 1 ) ) = ( ( A ^ M ) x. A ) )
7	5 2 6	mp2an	|- ( A ^ ( M + 1 ) ) = ( ( A ^ M ) x. A )
8	3	oveq2i	|- ( A ^ ( M + 1 ) ) = ( A ^ N )
9	7 8 4	3eqtr3i	|- ( A ^ N ) = C