Theorem cxpne0

Description: Complex exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 2-Aug-2014)

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

Proof

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 )