Metamath Proof Explorer

Theorem expval

Description: Value of exponentiation to integer powers. (Contributed by NM, 20-May-2004) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( x = A /\ y = N ) -> y = N )
2 1 eqeq1d 
 |-  ( ( x = A /\ y = N ) -> ( y = 0 <-> N = 0 ) )
3 1 breq2d 
 |-  ( ( x = A /\ y = N ) -> ( 0 < y <-> 0 < N ) )
4 simpl 
 |-  ( ( x = A /\ y = N ) -> x = A )
5 4 sneqd 
 |-  ( ( x = A /\ y = N ) -> { x } = { A } )
6 5 xpeq2d 
 |-  ( ( x = A /\ y = N ) -> ( NN X. { x } ) = ( NN X. { A } ) )
7 6 seqeq3d 
 |-  ( ( x = A /\ y = N ) -> seq 1 ( x. , ( NN X. { x } ) ) = seq 1 ( x. , ( NN X. { A } ) ) )
8 7 1 fveq12d 
 |-  ( ( x = A /\ y = N ) -> ( seq 1 ( x. , ( NN X. { x } ) ) ` y ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )
9 1 negeqd 
 |-  ( ( x = A /\ y = N ) -> -u y = -u N )
10 7 9 fveq12d 
 |-  ( ( x = A /\ y = N ) -> ( seq 1 ( x. , ( NN X. { x } ) ) ` -u y ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) )
11 10 oveq2d 
 |-  ( ( x = A /\ y = N ) -> ( 1 / ( seq 1 ( x. , ( NN X. { x } ) ) ` -u y ) ) = ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) )
12 3 8 11 ifbieq12d 
 |-  ( ( x = A /\ y = N ) -> if ( 0 < y , ( seq 1 ( x. , ( NN X. { x } ) ) ` y ) , ( 1 / ( seq 1 ( x. , ( NN X. { x } ) ) ` -u y ) ) ) = if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) )
13 2 12 ifbieq2d 
 |-  ( ( x = A /\ y = N ) -> if ( y = 0 , 1 , if ( 0 < y , ( seq 1 ( x. , ( NN X. { x } ) ) ` y ) , ( 1 / ( seq 1 ( x. , ( NN X. { x } ) ) ` -u y ) ) ) ) = if ( N = 0 , 1 , if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) ) )
14 df-exp 
 |-  ^ = ( x e. CC , y e. ZZ |-> if ( y = 0 , 1 , if ( 0 < y , ( seq 1 ( x. , ( NN X. { x } ) ) ` y ) , ( 1 / ( seq 1 ( x. , ( NN X. { x } ) ) ` -u y ) ) ) ) )
15 1ex 
 |-  1 e. _V
16 fvex 
 |-  ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) e. _V
17 ovex 
 |-  ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) e. _V
18 16 17 ifex 
 |-  if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) e. _V
19 15 18 ifex 
 |-  if ( N = 0 , 1 , if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) ) ) ) e. _V
20 13 14 19 ovmpoa 
 |-  ( ( 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 ) ) ) ) )