Theorem exprec

Description: Nonnegative 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 ) ) )