Theorem cxpeq0

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

	Ref	Expression
Assertion	cxpeq0	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^B=0\leftrightarrow \left(A=0\wedge B\ne 0\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cxpne0	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B\ne 0$$
2	1	3com23	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge A\ne 0\right)\to A^B\ne 0$$
3	2	3expia	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A\ne 0\to A^B\ne 0\right)$$
4	3	necon4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^B=0\to A=0\right)$$
5		ax-1ne0	$$⊢1\ne 0$$
6		cxp0	$$⊢A\in ℂ\to A^0=1$$
7	6	neeq1d	$$⊢A\in ℂ\to \left(A^0\ne 0\leftrightarrow 1\ne 0\right)$$
8	5 7	mpbiri	$$⊢A\in ℂ\to A^0\ne 0$$
9	8	adantr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^0\ne 0$$
10		oveq2	$$⊢B=0\to A^B=A^0$$
11	10	neeq1d	$$⊢B=0\to \left(A^B\ne 0\leftrightarrow A^0\ne 0\right)$$
12	9 11	syl5ibrcom	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(B=0\to A^B\ne 0\right)$$
13	12	necon2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^B=0\to B\ne 0\right)$$
14	4 13	jcad	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^B=0\to \left(A=0\wedge B\ne 0\right)\right)$$
15		0cxp	$$⊢\left(B\in ℂ\wedge B\ne 0\right)\to 0^B=0$$
16		oveq1	$$⊢A=0\to A^B=0^B$$
17	16	eqeq1d	$$⊢A=0\to \left(A^B=0\leftrightarrow 0^B=0\right)$$
18	15 17	syl5ibrcom	$$⊢\left(B\in ℂ\wedge B\ne 0\right)\to \left(A=0\to A^B=0\right)$$
19	18	expimpd	$$⊢B\in ℂ\to \left(\left(B\ne 0\wedge A=0\right)\to A^B=0\right)$$
20	19	ancomsd	$$⊢B\in ℂ\to \left(\left(A=0\wedge B\ne 0\right)\to A^B=0\right)$$
21	20	adantl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\left(A=0\wedge B\ne 0\right)\to A^B=0\right)$$
22	14 21	impbid	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^B=0\leftrightarrow \left(A=0\wedge B\ne 0\right)\right)$$