Metamath Proof Explorer

Theorem cxpcl

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

Ref Expression
Assertion cxpcl 
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )

Proof

Step Hyp Ref Expression
1 cxpval 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) )
2 ax-1cn 
 |-  1 e. CC
3 0cn 
 |-  0 e. CC
4 2 3 ifcli 
 |-  if ( B = 0 , 1 , 0 ) e. CC
5 4 a1i 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ A = 0 ) -> if ( B = 0 , 1 , 0 ) e. CC )
6 df-ne 
 |-  ( A =/= 0 <-> -. A = 0 )
7 id 
 |-  ( B e. CC -> B e. CC )
8 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
9 mulcl 
 |-  ( ( B e. CC /\ ( log ` A ) e. CC ) -> ( B x. ( log ` A ) ) e. CC )
10 7 8 9 syl2anr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) -> ( B x. ( log ` A ) ) e. CC )
11 10 an32s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ A =/= 0 ) -> ( B x. ( log ` A ) ) e. CC )
12 efcl 
 |-  ( ( B x. ( log ` A ) ) e. CC -> ( exp ` ( B x. ( log ` A ) ) ) e. CC )
13 11 12 syl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ A =/= 0 ) -> ( exp ` ( B x. ( log ` A ) ) ) e. CC )
14 6 13 sylan2br 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ -. A = 0 ) -> ( exp ` ( B x. ( log ` A ) ) ) e. CC )
15 5 14 ifclda 
 |-  ( ( A e. CC /\ B e. CC ) -> if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) e. CC )
16 1 15 eqeltrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )