Description: Value of a complex number raised to the zeroth power. (Contributed by Mario Carneiro, 28-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | expcld.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| Assertion | exp0d | ⊢ ( 𝜑 → ( 𝐴 ↑ 0 ) = 1 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | expcld.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| 2 | exp0 | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 ) | |
| 3 | 1 2 | syl | ⊢ ( 𝜑 → ( 𝐴 ↑ 0 ) = 1 ) |