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