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