Theorem expeq0

Description: Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by NM, 23-Feb-2005)

	Ref	Expression
Assertion	expeq0	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to \left(A^N=0\leftrightarrow A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢j=1\to A^j=A^1$$
2	1	eqeq1d	$$⊢j=1\to \left(A^j=0\leftrightarrow A^1=0\right)$$
3	2	bibi1d	$$⊢j=1\to \left(\left(A^j=0\leftrightarrow A=0\right)\leftrightarrow \left(A^1=0\leftrightarrow A=0\right)\right)$$
4	3	imbi2d	$$⊢j=1\to \left(\left(A\in ℂ\to \left(A^j=0\leftrightarrow A=0\right)\right)\leftrightarrow \left(A\in ℂ\to \left(A^1=0\leftrightarrow A=0\right)\right)\right)$$
5		oveq2	$$⊢j=k\to A^j=A^k$$
6	5	eqeq1d	$$⊢j=k\to \left(A^j=0\leftrightarrow A^k=0\right)$$
7	6	bibi1d	$$⊢j=k\to \left(\left(A^j=0\leftrightarrow A=0\right)\leftrightarrow \left(A^k=0\leftrightarrow A=0\right)\right)$$
8	7	imbi2d	$$⊢j=k\to \left(\left(A\in ℂ\to \left(A^j=0\leftrightarrow A=0\right)\right)\leftrightarrow \left(A\in ℂ\to \left(A^k=0\leftrightarrow A=0\right)\right)\right)$$
9		oveq2	$$⊢j=k+1\to A^j=A^{k+1}$$
10	9	eqeq1d	$$⊢j=k+1\to \left(A^j=0\leftrightarrow A^{k+1}=0\right)$$
11	10	bibi1d	$$⊢j=k+1\to \left(\left(A^j=0\leftrightarrow A=0\right)\leftrightarrow \left(A^{k+1}=0\leftrightarrow A=0\right)\right)$$
12	11	imbi2d	$$⊢j=k+1\to \left(\left(A\in ℂ\to \left(A^j=0\leftrightarrow A=0\right)\right)\leftrightarrow \left(A\in ℂ\to \left(A^{k+1}=0\leftrightarrow A=0\right)\right)\right)$$
13		oveq2	$$⊢j=N\to A^j=A^N$$
14	13	eqeq1d	$$⊢j=N\to \left(A^j=0\leftrightarrow A^N=0\right)$$
15	14	bibi1d	$$⊢j=N\to \left(\left(A^j=0\leftrightarrow A=0\right)\leftrightarrow \left(A^N=0\leftrightarrow A=0\right)\right)$$
16	15	imbi2d	$$⊢j=N\to \left(\left(A\in ℂ\to \left(A^j=0\leftrightarrow A=0\right)\right)\leftrightarrow \left(A\in ℂ\to \left(A^N=0\leftrightarrow A=0\right)\right)\right)$$
17		exp1	$$⊢A\in ℂ\to A^1=A$$
18	17	eqeq1d	$$⊢A\in ℂ\to \left(A^1=0\leftrightarrow A=0\right)$$
19		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
20		expp1	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^{k+1}=A^{k}A$$
21	20	eqeq1d	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left(A^{k+1}=0\leftrightarrow A^{k}A=0\right)$$
22		expcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
23		simpl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A\in ℂ$$
24	22 23	mul0ord	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left(A^{k}A=0\leftrightarrow \left(A^k=0\vee A=0\right)\right)$$
25	21 24	bitrd	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left(A^{k+1}=0\leftrightarrow \left(A^k=0\vee A=0\right)\right)$$
26	19 25	sylan2	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to \left(A^{k+1}=0\leftrightarrow \left(A^k=0\vee A=0\right)\right)$$
27		biimp	$$⊢\left(A^k=0\leftrightarrow A=0\right)\to \left(A^k=0\to A=0\right)$$
28		idd	$$⊢\left(A^k=0\leftrightarrow A=0\right)\to \left(A=0\to A=0\right)$$
29	27 28	jaod	$$⊢\left(A^k=0\leftrightarrow A=0\right)\to \left(\left(A^k=0\vee A=0\right)\to A=0\right)$$
30		olc	$$⊢A=0\to \left(A^k=0\vee A=0\right)$$
31	29 30	impbid1	$$⊢\left(A^k=0\leftrightarrow A=0\right)\to \left(\left(A^k=0\vee A=0\right)\leftrightarrow A=0\right)$$
32	26 31	sylan9bb	$$⊢\left(\left(A\in ℂ\wedge k\in \mathbb{N}\right)\wedge \left(A^k=0\leftrightarrow A=0\right)\right)\to \left(A^{k+1}=0\leftrightarrow A=0\right)$$
33	32	exp31	$$⊢A\in ℂ\to \left(k\in \mathbb{N}\to \left(\left(A^k=0\leftrightarrow A=0\right)\to \left(A^{k+1}=0\leftrightarrow A=0\right)\right)\right)$$
34	33	com12	$$⊢k\in \mathbb{N}\to \left(A\in ℂ\to \left(\left(A^k=0\leftrightarrow A=0\right)\to \left(A^{k+1}=0\leftrightarrow A=0\right)\right)\right)$$
35	34	a2d	$$⊢k\in \mathbb{N}\to \left(\left(A\in ℂ\to \left(A^k=0\leftrightarrow A=0\right)\right)\to \left(A\in ℂ\to \left(A^{k+1}=0\leftrightarrow A=0\right)\right)\right)$$
36	4 8 12 16 18 35	nnind	$$⊢N\in \mathbb{N}\to \left(A\in ℂ\to \left(A^N=0\leftrightarrow A=0\right)\right)$$
37	36	impcom	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to \left(A^N=0\leftrightarrow A=0\right)$$