Metamath Proof Explorer

Theorem expnnval

Description: Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expnnval 
|- ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( N e. NN -> N e. ZZ )
2 expval 
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( A ^ N ) = if ( N = 0 , 1 , if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = if ( N = 0 , 1 , if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) ) )
4 nnne0 
 |-  ( N e. NN -> N =/= 0 )
5 4 neneqd 
 |-  ( N e. NN -> -. N = 0 )
6 5 iffalsed 
 |-  ( N e. NN -> if ( N = 0 , 1 , if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) ) = if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) )
7 nngt0 
 |-  ( N e. NN -> 0 < N )
8 7 iftrued 
 |-  ( N e. NN -> if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )
9 6 8 eqtrd 
 |-  ( N e. NN -> if ( N = 0 , 1 , if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )
10 9 adantl 
 |-  ( ( A e. CC /\ N e. NN ) -> if ( N = 0 , 1 , if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )
11 3 10 eqtrd 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )