This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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