Step |
Hyp |
Ref |
Expression |
1 |
|
cxpef |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) ) |
2 |
|
id |
|- ( B e. CC -> B e. CC ) |
3 |
|
logcl |
|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC ) |
4 |
|
mulcl |
|- ( ( B e. CC /\ ( log ` A ) e. CC ) -> ( B x. ( log ` A ) ) e. CC ) |
5 |
2 3 4
|
syl2anr |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) -> ( B x. ( log ` A ) ) e. CC ) |
6 |
5
|
3impa |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( B x. ( log ` A ) ) e. CC ) |
7 |
|
efne0 |
|- ( ( B x. ( log ` A ) ) e. CC -> ( exp ` ( B x. ( log ` A ) ) ) =/= 0 ) |
8 |
6 7
|
syl |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( exp ` ( B x. ( log ` A ) ) ) =/= 0 ) |
9 |
1 8
|
eqnetrd |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) =/= 0 ) |