Metamath Proof Explorer

Theorem cxpexp

Description: Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( B e. NN0 <-> ( B e. NN \/ B = 0 ) )
2 nncn 
 |-  ( B e. NN -> B e. CC )
3 nnne0 
 |-  ( B e. NN -> B =/= 0 )
4 0cxp 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 0 ^c B ) = 0 )
5 2 3 4 syl2anc 
 |-  ( B e. NN -> ( 0 ^c B ) = 0 )
6 0exp 
 |-  ( B e. NN -> ( 0 ^ B ) = 0 )
7 5 6 eqtr4d 
 |-  ( B e. NN -> ( 0 ^c B ) = ( 0 ^ B ) )
8 0cn 
 |-  0 e. CC
9 cxpval 
 |-  ( ( 0 e. CC /\ 0 e. CC ) -> ( 0 ^c 0 ) = if ( 0 = 0 , if ( 0 = 0 , 1 , 0 ) , ( exp ` ( 0 x. ( log ` 0 ) ) ) ) )
10 8 8 9 mp2an 
 |-  ( 0 ^c 0 ) = if ( 0 = 0 , if ( 0 = 0 , 1 , 0 ) , ( exp ` ( 0 x. ( log ` 0 ) ) ) )
11 eqid 
 |-  0 = 0
12 11 iftruei 
 |-  if ( 0 = 0 , if ( 0 = 0 , 1 , 0 ) , ( exp ` ( 0 x. ( log ` 0 ) ) ) ) = if ( 0 = 0 , 1 , 0 )
13 11 iftruei 
 |-  if ( 0 = 0 , 1 , 0 ) = 1
14 10 12 13 3eqtri 
 |-  ( 0 ^c 0 ) = 1
15 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
16 14 15 eqtr4i 
 |-  ( 0 ^c 0 ) = ( 0 ^ 0 )
17 oveq2 
 |-  ( B = 0 -> ( 0 ^c B ) = ( 0 ^c 0 ) )
18 oveq2 
 |-  ( B = 0 -> ( 0 ^ B ) = ( 0 ^ 0 ) )
19 16 17 18 3eqtr4a 
 |-  ( B = 0 -> ( 0 ^c B ) = ( 0 ^ B ) )
20 7 19 jaoi 
 |-  ( ( B e. NN \/ B = 0 ) -> ( 0 ^c B ) = ( 0 ^ B ) )
21 1 20 sylbi 
 |-  ( B e. NN0 -> ( 0 ^c B ) = ( 0 ^ B ) )
22 oveq1 
 |-  ( A = 0 -> ( A ^c B ) = ( 0 ^c B ) )
23 oveq1 
 |-  ( A = 0 -> ( A ^ B ) = ( 0 ^ B ) )
24 22 23 eqeq12d 
 |-  ( A = 0 -> ( ( A ^c B ) = ( A ^ B ) <-> ( 0 ^c B ) = ( 0 ^ B ) ) )
25 21 24 syl5ibrcom 
 |-  ( B e. NN0 -> ( A = 0 -> ( A ^c B ) = ( A ^ B ) ) )
26 25 adantl 
 |-  ( ( A e. CC /\ B e. NN0 ) -> ( A = 0 -> ( A ^c B ) = ( A ^ B ) ) )
27 26 imp 
 |-  ( ( ( A e. CC /\ B e. NN0 ) /\ A = 0 ) -> ( A ^c B ) = ( A ^ B ) )
28 nn0z 
 |-  ( B e. NN0 -> B e. ZZ )
29 cxpexpz 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. ZZ ) -> ( A ^c B ) = ( A ^ B ) )
30 29 3expa 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ZZ ) -> ( A ^c B ) = ( A ^ B ) )
31 28 30 sylan2 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. NN0 ) -> ( A ^c B ) = ( A ^ B ) )
32 31 an32s 
 |-  ( ( ( A e. CC /\ B e. NN0 ) /\ A =/= 0 ) -> ( A ^c B ) = ( A ^ B ) )
33 27 32 pm2.61dane 
 |-  ( ( A e. CC /\ B e. NN0 ) -> ( A ^c B ) = ( A ^ B ) )