This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem expnegz

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

Ref Expression
Assertion expnegz ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elznn0 ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) )
2 expneg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
3 2 ex ⊢ ( 𝐴 ∈ ℂ → ( 𝑁 ∈ ℕ0 → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
4 3 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℝ ) → ( 𝑁 ∈ ℕ0 → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
5 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → 𝐴 ∈ ℂ )
6 simprl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℝ )
7 6 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℂ )
8 simprr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → - 𝑁 ∈ ℕ0 )
9 expneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
10 5 7 8 9 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝐴 ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
11 10 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → ( 1 / ( 𝐴 ↑ 𝑁 ) ) = ( 1 / ( 1 / ( 𝐴 ↑ - 𝑁 ) ) ) )
12 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) ∈ ℂ )
13 12 ad2ant2rl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝐴 ↑ - 𝑁 ) ∈ ℂ )
14 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → 𝐴 ≠ 0 )
15 8 nn0zd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → - 𝑁 ∈ ℤ )
16 expne0i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) ≠ 0 )
17 5 14 15 16 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝐴 ↑ - 𝑁 ) ≠ 0 )
18 13 17 recrecd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → ( 1 / ( 1 / ( 𝐴 ↑ - 𝑁 ) ) ) = ( 𝐴 ↑ - 𝑁 ) )
19 11 18 eqtr2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
20 19 expr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℝ ) → ( - 𝑁 ∈ ℕ0 → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
21 4 20 jaod ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℝ ) → ( ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
22 21 expimpd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
23 1 22 biimtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑁 ∈ ℤ → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
24 23 3impia ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )