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 
|- ( ( 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 ) ) )