Theorem cxpeq0

Description: Complex exponentiation is zero iff the base is zero and the exponent is nonzero. (Contributed by Mario Carneiro, 23-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		cxpne0	|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) =/= 0 )
2	1	3com23	|- ( ( A e. CC /\ B e. CC /\ A =/= 0 ) -> ( A ^c B ) =/= 0 )
3	2	3expia	|- ( ( A e. CC /\ B e. CC ) -> ( A =/= 0 -> ( A ^c B ) =/= 0 ) )
4	3	necon4d	|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^c B ) = 0 -> A = 0 ) )
5		ax-1ne0	|- 1 =/= 0
6		cxp0	|- ( A e. CC -> ( A ^c 0 ) = 1 )
7	6	neeq1d	|- ( A e. CC -> ( ( A ^c 0 ) =/= 0 <-> 1 =/= 0 ) )
8	5 7	mpbiri	|- ( A e. CC -> ( A ^c 0 ) =/= 0 )
9	8	adantr	|- ( ( A e. CC /\ B e. CC ) -> ( A ^c 0 ) =/= 0 )
10		oveq2	|- ( B = 0 -> ( A ^c B ) = ( A ^c 0 ) )
11	10	neeq1d	|- ( B = 0 -> ( ( A ^c B ) =/= 0 <-> ( A ^c 0 ) =/= 0 ) )
12	9 11	syl5ibrcom	|- ( ( A e. CC /\ B e. CC ) -> ( B = 0 -> ( A ^c B ) =/= 0 ) )
13	12	necon2d	|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^c B ) = 0 -> B =/= 0 ) )
14	4 13	jcad	|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^c B ) = 0 -> ( A = 0 /\ B =/= 0 ) ) )
15		0cxp	|- ( ( B e. CC /\ B =/= 0 ) -> ( 0 ^c B ) = 0 )
16		oveq1	|- ( A = 0 -> ( A ^c B ) = ( 0 ^c B ) )
17	16	eqeq1d	|- ( A = 0 -> ( ( A ^c B ) = 0 <-> ( 0 ^c B ) = 0 ) )
18	15 17	syl5ibrcom	|- ( ( B e. CC /\ B =/= 0 ) -> ( A = 0 -> ( A ^c B ) = 0 ) )
19	18	expimpd	|- ( B e. CC -> ( ( B =/= 0 /\ A = 0 ) -> ( A ^c B ) = 0 ) )
20	19	ancomsd	|- ( B e. CC -> ( ( A = 0 /\ B =/= 0 ) -> ( A ^c B ) = 0 ) )
21	20	adantl	|- ( ( A e. CC /\ B e. CC ) -> ( ( A = 0 /\ B =/= 0 ) -> ( A ^c B ) = 0 ) )
22	14 21	impbid	|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^c B ) = 0 <-> ( A = 0 /\ B =/= 0 ) ) )