Metamath Proof Explorer


Theorem expn1

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 / 𝐴 ) )

Proof

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 / 𝐴 ) )