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

Metamath Proof Explorer

Theorem exprec

Description: Integer exponentiation of a reciprocal. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 expclz ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
2 reccl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 1 / 𝐴 ) ∈ ℂ )
4 recne0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ≠ 0 )
5 4 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 1 / 𝐴 ) ≠ 0 )
6 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
7 expclz ⊢ ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ ( 1 / 𝐴 ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 1 / 𝐴 ) ↑ 𝑁 ) ∈ ℂ )
8 3 5 6 7 syl3anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 1 / 𝐴 ) ↑ 𝑁 ) ∈ ℂ )
9 expne0i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
10 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℂ )
11 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → 𝐴 ≠ 0 )
12 10 11 recidd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 )
13 12 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
14 mulexpz ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ( 1 / 𝐴 ) ∈ ℂ ∧ ( 1 / 𝐴 ) ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( ( 1 / 𝐴 ) ↑ 𝑁 ) ) )
15 10 11 3 5 6 14 syl221anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( ( 1 / 𝐴 ) ↑ 𝑁 ) ) )
16 1exp ⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
17 6 16 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 1 ↑ 𝑁 ) = 1 )
18 13 15 17 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 𝑁 ) · ( ( 1 / 𝐴 ) ↑ 𝑁 ) ) = 1 )
19 1 8 9 18 mvllmuld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 1 / 𝐴 ) ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )