Metamath Proof Explorer

Theorem expeq0

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