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
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( 1 / A ) ^ N ) = ( 1 / ( A ^ N ) ) )

Proof

Step Hyp Ref Expression
1 expclz
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. CC )
2 reccl
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
3 2 3adant3
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( 1 / A ) e. CC )
4 recne0
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) =/= 0 )
5 4 3adant3
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( 1 / A ) =/= 0 )
6 simp3
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> N e. ZZ )
7 expclz
 |-  ( ( ( 1 / A ) e. CC /\ ( 1 / A ) =/= 0 /\ N e. ZZ ) -> ( ( 1 / A ) ^ N ) e. CC )
8 3 5 6 7 syl3anc
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( 1 / A ) ^ N ) e. CC )
9 expne0i
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) =/= 0 )
10 simp1
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> A e. CC )
11 simp2
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> A =/= 0 )
12 10 11 recidd
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A x. ( 1 / A ) ) = 1 )
13 12 oveq1d
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( A x. ( 1 / A ) ) ^ N ) = ( 1 ^ N ) )
14 mulexpz
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( ( 1 / A ) e. CC /\ ( 1 / A ) =/= 0 ) /\ N e. ZZ ) -> ( ( A x. ( 1 / A ) ) ^ N ) = ( ( A ^ N ) x. ( ( 1 / A ) ^ N ) ) )
15 10 11 3 5 6 14 syl221anc
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( A x. ( 1 / A ) ) ^ N ) = ( ( A ^ N ) x. ( ( 1 / A ) ^ N ) ) )
16 1exp
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
17 6 16 syl
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( 1 ^ N ) = 1 )
18 13 15 17 3eqtr3d
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( A ^ N ) x. ( ( 1 / A ) ^ N ) ) = 1 )
19 1 8 9 18 mvllmuld
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( 1 / A ) ^ N ) = ( 1 / ( A ^ N ) ) )