Description: Positive integer exponentiation is nonzero iff its mantissa is nonzero. (Contributed by NM, 6-May-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | expne0 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) ≠ 0 ↔ 𝐴 ≠ 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expeq0 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) = 0 ↔ 𝐴 = 0 ) ) | |
2 | 1 | necon3bid | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) ≠ 0 ↔ 𝐴 ≠ 0 ) ) |