Metamath Proof Explorer


Theorem expeq0

Description: Positive integer exponentiation is 0 iff its base is 0. (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 ) )