Step |
Hyp |
Ref |
Expression |
1 |
|
elznn0nn |
|- ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) ) |
2 |
|
absexp |
|- ( ( A e. CC /\ N e. NN0 ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) |
3 |
2
|
ex |
|- ( A e. CC -> ( N e. NN0 -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) ) |
4 |
3
|
adantr |
|- ( ( A e. CC /\ A =/= 0 ) -> ( N e. NN0 -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) ) |
5 |
|
1cnd |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> 1 e. CC ) |
6 |
|
simpll |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> A e. CC ) |
7 |
|
nnnn0 |
|- ( -u N e. NN -> -u N e. NN0 ) |
8 |
7
|
ad2antll |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN0 ) |
9 |
6 8
|
expcld |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u N ) e. CC ) |
10 |
|
simplr |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> A =/= 0 ) |
11 |
|
nnz |
|- ( -u N e. NN -> -u N e. ZZ ) |
12 |
11
|
ad2antll |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. ZZ ) |
13 |
6 10 12
|
expne0d |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u N ) =/= 0 ) |
14 |
|
absdiv |
|- ( ( 1 e. CC /\ ( A ^ -u N ) e. CC /\ ( A ^ -u N ) =/= 0 ) -> ( abs ` ( 1 / ( A ^ -u N ) ) ) = ( ( abs ` 1 ) / ( abs ` ( A ^ -u N ) ) ) ) |
15 |
5 9 13 14
|
syl3anc |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( abs ` ( 1 / ( A ^ -u N ) ) ) = ( ( abs ` 1 ) / ( abs ` ( A ^ -u N ) ) ) ) |
16 |
|
abs1 |
|- ( abs ` 1 ) = 1 |
17 |
16
|
oveq1i |
|- ( ( abs ` 1 ) / ( abs ` ( A ^ -u N ) ) ) = ( 1 / ( abs ` ( A ^ -u N ) ) ) |
18 |
|
absexp |
|- ( ( A e. CC /\ -u N e. NN0 ) -> ( abs ` ( A ^ -u N ) ) = ( ( abs ` A ) ^ -u N ) ) |
19 |
6 8 18
|
syl2anc |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( abs ` ( A ^ -u N ) ) = ( ( abs ` A ) ^ -u N ) ) |
20 |
19
|
oveq2d |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( abs ` ( A ^ -u N ) ) ) = ( 1 / ( ( abs ` A ) ^ -u N ) ) ) |
21 |
17 20
|
eqtrid |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( abs ` 1 ) / ( abs ` ( A ^ -u N ) ) ) = ( 1 / ( ( abs ` A ) ^ -u N ) ) ) |
22 |
15 21
|
eqtrd |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( abs ` ( 1 / ( A ^ -u N ) ) ) = ( 1 / ( ( abs ` A ) ^ -u N ) ) ) |
23 |
|
simprl |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. RR ) |
24 |
23
|
recnd |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. CC ) |
25 |
|
expneg2 |
|- ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) ) |
26 |
6 24 8 25
|
syl3anc |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) ) |
27 |
26
|
fveq2d |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( abs ` ( A ^ N ) ) = ( abs ` ( 1 / ( A ^ -u N ) ) ) ) |
28 |
|
abscl |
|- ( A e. CC -> ( abs ` A ) e. RR ) |
29 |
28
|
ad2antrr |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( abs ` A ) e. RR ) |
30 |
29
|
recnd |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( abs ` A ) e. CC ) |
31 |
|
expneg2 |
|- ( ( ( abs ` A ) e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( ( abs ` A ) ^ N ) = ( 1 / ( ( abs ` A ) ^ -u N ) ) ) |
32 |
30 24 8 31
|
syl3anc |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( abs ` A ) ^ N ) = ( 1 / ( ( abs ` A ) ^ -u N ) ) ) |
33 |
22 27 32
|
3eqtr4d |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) |
34 |
33
|
ex |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( N e. RR /\ -u N e. NN ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) ) |
35 |
4 34
|
jaod |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) ) |
36 |
35
|
3impia |
|- ( ( A e. CC /\ A =/= 0 /\ ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) |
37 |
1 36
|
syl3an3b |
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) |