Theorem expeq0

Description: A positive integer power is zero if and only if its base is zero. (Contributed by NM, 23-Feb-2005)

	Ref	Expression
Assertion	expeq0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) = 0 ↔ 𝐴 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑗 = 1 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 1 ) )
2	1	eqeq1d	⊢ ( 𝑗 = 1 → ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ ( 𝐴 ↑ 1 ) = 0 ) )
3	2	bibi1d	⊢ ( 𝑗 = 1 → ( ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ 𝐴 = 0 ) ↔ ( ( 𝐴 ↑ 1 ) = 0 ↔ 𝐴 = 0 ) ) )
4	3	imbi2d	⊢ ( 𝑗 = 1 → ( ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ 𝐴 = 0 ) ) ↔ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) = 0 ↔ 𝐴 = 0 ) ) ) )
5		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑘 ) )
6	5	eqeq1d	⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ ( 𝐴 ↑ 𝑘 ) = 0 ) )
7	6	bibi1d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ 𝐴 = 0 ) ↔ ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) ) )
8	7	imbi2d	⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ 𝐴 = 0 ) ) ↔ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) ) ) )
9		oveq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
10	9	eqeq1d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ) )
11	10	bibi1d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ 𝐴 = 0 ) ↔ ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ 𝐴 = 0 ) ) )
12	11	imbi2d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ 𝐴 = 0 ) ) ↔ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ 𝐴 = 0 ) ) ) )
13		oveq2	⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑁 ) )
14	13	eqeq1d	⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ ( 𝐴 ↑ 𝑁 ) = 0 ) )
15	14	bibi1d	⊢ ( 𝑗 = 𝑁 → ( ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ 𝐴 = 0 ) ↔ ( ( 𝐴 ↑ 𝑁 ) = 0 ↔ 𝐴 = 0 ) ) )
16	15	imbi2d	⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 𝑗 ) = 0 ↔ 𝐴 = 0 ) ) ↔ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 𝑁 ) = 0 ↔ 𝐴 = 0 ) ) ) )
17		exp1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
18	17	eqeq1d	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) = 0 ↔ 𝐴 = 0 ) )
19		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
20		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
21	20	eqeq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) = 0 ) )
22		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
23		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
24	22 23	mul0ord	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) = 0 ↔ ( ( 𝐴 ↑ 𝑘 ) = 0 ∨ 𝐴 = 0 ) ) )
25	21 24	bitrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ ( ( 𝐴 ↑ 𝑘 ) = 0 ∨ 𝐴 = 0 ) ) )
26	19 25	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ ( ( 𝐴 ↑ 𝑘 ) = 0 ∨ 𝐴 = 0 ) ) )
27		biimp	⊢ ( ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) → ( ( 𝐴 ↑ 𝑘 ) = 0 → 𝐴 = 0 ) )
28		idd	⊢ ( ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) → ( 𝐴 = 0 → 𝐴 = 0 ) )
29	27 28	jaod	⊢ ( ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) → ( ( ( 𝐴 ↑ 𝑘 ) = 0 ∨ 𝐴 = 0 ) → 𝐴 = 0 ) )
30		olc	⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 𝑘 ) = 0 ∨ 𝐴 = 0 ) )
31	29 30	impbid1	⊢ ( ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) → ( ( ( 𝐴 ↑ 𝑘 ) = 0 ∨ 𝐴 = 0 ) ↔ 𝐴 = 0 ) )
32	26 31	sylan9bb	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ 𝐴 = 0 ) )
33	32	exp31	⊢ ( 𝐴 ∈ ℂ → ( 𝑘 ∈ ℕ → ( ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ 𝐴 = 0 ) ) ) )
34	33	com12	⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ∈ ℂ → ( ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ 𝐴 = 0 ) ) ) )
35	34	a2d	⊢ ( 𝑘 ∈ ℕ → ( ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 𝑘 ) = 0 ↔ 𝐴 = 0 ) ) → ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) = 0 ↔ 𝐴 = 0 ) ) ) )
36	4 8 12 16 18 35	nnind	⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 𝑁 ) = 0 ↔ 𝐴 = 0 ) ) )
37	36	impcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) = 0 ↔ 𝐴 = 0 ) )