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