Theorem numexp2x

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

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

Proof

Step	Hyp	Ref	Expression
1		numexp.1	|- A e. NN0
2		numexpp1.2	|- M e. NN0
3		numexp2x.3	|- ( 2 x. M ) = N
4		numexp2x.4	|- ( A ^ M ) = D
5		numexp2x.5	|- ( D x. D ) = C
6	2	nn0cni	|- M e. CC
7	6	2timesi	|- ( 2 x. M ) = ( M + M )
8	3 7	eqtr3i	|- N = ( M + M )
9	8	oveq2i	|- ( A ^ N ) = ( A ^ ( M + M ) )
10	1	nn0cni	|- A e. CC
11		expadd	|- ( ( A e. CC /\ M e. NN0 /\ M e. NN0 ) -> ( A ^ ( M + M ) ) = ( ( A ^ M ) x. ( A ^ M ) ) )
12	10 2 2 11	mp3an	|- ( A ^ ( M + M ) ) = ( ( A ^ M ) x. ( A ^ M ) )
13	9 12	eqtri	|- ( A ^ N ) = ( ( A ^ M ) x. ( A ^ M ) )
14	4 4	oveq12i	|- ( ( A ^ M ) x. ( A ^ M ) ) = ( D x. D )
15	14 5	eqtri	|- ( ( A ^ M ) x. ( A ^ M ) ) = C
16	13 15	eqtri	|- ( A ^ N ) = C