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 |
1
|
3adant2 |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) ) |
3 |
|
simp2 |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> A =/= 0 ) |
4 |
3
|
neneqd |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> -. A = 0 ) |
5 |
4
|
iffalsed |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) = ( exp ` ( B x. ( log ` A ) ) ) ) |
6 |
2 5
|
eqtrd |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) ) |