Theorem expneg2

Description: Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		negneg	⊢ ( 𝑁 ∈ ℂ → - - 𝑁 = 𝑁 )
2	1	3ad2ant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → - - 𝑁 = 𝑁 )
3	2	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - - 𝑁 ) = ( 𝐴 ↑ 𝑁 ) )
4		expneg	⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - - 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
5	4	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - - 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
6	3 5	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )