Description: A complex number raised to the negative one power is its reciprocal. When A = 0 , both sides have the "value" ( 1 / 0 ) ; relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | expn1 | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ - 1 ) = ( 1 / 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
2 | expneg | ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℕ0 ) → ( 𝐴 ↑ - 1 ) = ( 1 / ( 𝐴 ↑ 1 ) ) ) | |
3 | 1 2 | mpan2 | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ - 1 ) = ( 1 / ( 𝐴 ↑ 1 ) ) ) |
4 | exp1 | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 ) | |
5 | 4 | oveq2d | ⊢ ( 𝐴 ∈ ℂ → ( 1 / ( 𝐴 ↑ 1 ) ) = ( 1 / 𝐴 ) ) |
6 | 3 5 | eqtrd | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ - 1 ) = ( 1 / 𝐴 ) ) |