Metamath Proof Explorer


Theorem absexpz

Description: Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Assertion absexpz
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )

Proof

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