Metamath Proof Explorer

Theorem 1cxp

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

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

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 ax-1ne0 
 |-  1 =/= 0
3 cxpef 
 |-  ( ( 1 e. CC /\ 1 =/= 0 /\ A e. CC ) -> ( 1 ^c A ) = ( exp ` ( A x. ( log ` 1 ) ) ) )
4 1 2 3 mp3an12 
 |-  ( A e. CC -> ( 1 ^c A ) = ( exp ` ( A x. ( log ` 1 ) ) ) )
5 log1 
 |-  ( log ` 1 ) = 0
6 5 oveq2i 
 |-  ( A x. ( log ` 1 ) ) = ( A x. 0 )
7 mul01 
 |-  ( A e. CC -> ( A x. 0 ) = 0 )
8 6 7 syl5eq 
 |-  ( A e. CC -> ( A x. ( log ` 1 ) ) = 0 )
9 8 fveq2d 
 |-  ( A e. CC -> ( exp ` ( A x. ( log ` 1 ) ) ) = ( exp ` 0 ) )
10 ef0 
 |-  ( exp ` 0 ) = 1
11 9 10 eqtrdi 
 |-  ( A e. CC -> ( exp ` ( A x. ( log ` 1 ) ) ) = 1 )
12 4 11 eqtrd 
 |-  ( A e. CC -> ( 1 ^c A ) = 1 )