Metamath Proof Explorer

Theorem cxpval

Description: Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpval 
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( x = A /\ y = B ) -> x = A )
2 1 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( x = 0 <-> A = 0 ) )
3 simpr 
 |-  ( ( x = A /\ y = B ) -> y = B )
4 3 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( y = 0 <-> B = 0 ) )
5 4 ifbid 
 |-  ( ( x = A /\ y = B ) -> if ( y = 0 , 1 , 0 ) = if ( B = 0 , 1 , 0 ) )
6 1 fveq2d 
 |-  ( ( x = A /\ y = B ) -> ( log ` x ) = ( log ` A ) )
7 3 6 oveq12d 
 |-  ( ( x = A /\ y = B ) -> ( y x. ( log ` x ) ) = ( B x. ( log ` A ) ) )
8 7 fveq2d 
 |-  ( ( x = A /\ y = B ) -> ( exp ` ( y x. ( log ` x ) ) ) = ( exp ` ( B x. ( log ` A ) ) ) )
9 2 5 8 ifbieq12d 
 |-  ( ( x = A /\ y = B ) -> if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) )
10 df-cxp 
 |-  ^c = ( x e. CC , y e. CC |-> if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) )
11 ax-1cn 
 |-  1 e. CC
12 0cn 
 |-  0 e. CC
13 11 12 ifcli 
 |-  if ( B = 0 , 1 , 0 ) e. CC
14 13 elexi 
 |-  if ( B = 0 , 1 , 0 ) e. _V
15 fvex 
 |-  ( exp ` ( B x. ( log ` A ) ) ) e. _V
16 14 15 ifex 
 |-  if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) e. _V
17 9 10 16 ovmpoa 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) )