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