Metamath Proof Explorer

Theorem 0cxp

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

Ref Expression
Assertion 0cxp 
|- ( ( A e. CC /\ A =/= 0 ) -> ( 0 ^c A ) = 0 )

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 cxpval 
 |-  ( ( 0 e. CC /\ A e. CC ) -> ( 0 ^c A ) = if ( 0 = 0 , if ( A = 0 , 1 , 0 ) , ( exp ` ( A x. ( log ` 0 ) ) ) ) )
3 1 2 mpan 
 |-  ( A e. CC -> ( 0 ^c A ) = if ( 0 = 0 , if ( A = 0 , 1 , 0 ) , ( exp ` ( A x. ( log ` 0 ) ) ) ) )
4 eqid 
 |-  0 = 0
5 4 iftruei 
 |-  if ( 0 = 0 , if ( A = 0 , 1 , 0 ) , ( exp ` ( A x. ( log ` 0 ) ) ) ) = if ( A = 0 , 1 , 0 )
6 3 5 eqtrdi 
 |-  ( A e. CC -> ( 0 ^c A ) = if ( A = 0 , 1 , 0 ) )
7 ifnefalse 
 |-  ( A =/= 0 -> if ( A = 0 , 1 , 0 ) = 0 )
8 6 7 sylan9eq 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 0 ^c A ) = 0 )