Metamath Proof Explorer

Theorem absexp

Description: Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006)

Ref Expression
Assertion absexp 
|- ( ( A e. CC /\ N e. NN0 ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = 0 -> ( A ^ j ) = ( A ^ 0 ) )
2 1 fveq2d 
 |-  ( j = 0 -> ( abs ` ( A ^ j ) ) = ( abs ` ( A ^ 0 ) ) )
3 oveq2 
 |-  ( j = 0 -> ( ( abs ` A ) ^ j ) = ( ( abs ` A ) ^ 0 ) )
4 2 3 eqeq12d 
 |-  ( j = 0 -> ( ( abs ` ( A ^ j ) ) = ( ( abs ` A ) ^ j ) <-> ( abs ` ( A ^ 0 ) ) = ( ( abs ` A ) ^ 0 ) ) )
5 oveq2 
 |-  ( j = k -> ( A ^ j ) = ( A ^ k ) )
6 5 fveq2d 
 |-  ( j = k -> ( abs ` ( A ^ j ) ) = ( abs ` ( A ^ k ) ) )
7 oveq2 
 |-  ( j = k -> ( ( abs ` A ) ^ j ) = ( ( abs ` A ) ^ k ) )
8 6 7 eqeq12d 
 |-  ( j = k -> ( ( abs ` ( A ^ j ) ) = ( ( abs ` A ) ^ j ) <-> ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) ) )
9 oveq2 
 |-  ( j = ( k + 1 ) -> ( A ^ j ) = ( A ^ ( k + 1 ) ) )
10 9 fveq2d 
 |-  ( j = ( k + 1 ) -> ( abs ` ( A ^ j ) ) = ( abs ` ( A ^ ( k + 1 ) ) ) )
11 oveq2 
 |-  ( j = ( k + 1 ) -> ( ( abs ` A ) ^ j ) = ( ( abs ` A ) ^ ( k + 1 ) ) )
12 10 11 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( ( abs ` ( A ^ j ) ) = ( ( abs ` A ) ^ j ) <-> ( abs ` ( A ^ ( k + 1 ) ) ) = ( ( abs ` A ) ^ ( k + 1 ) ) ) )
13 oveq2 
 |-  ( j = N -> ( A ^ j ) = ( A ^ N ) )
14 13 fveq2d 
 |-  ( j = N -> ( abs ` ( A ^ j ) ) = ( abs ` ( A ^ N ) ) )
15 oveq2 
 |-  ( j = N -> ( ( abs ` A ) ^ j ) = ( ( abs ` A ) ^ N ) )
16 14 15 eqeq12d 
 |-  ( j = N -> ( ( abs ` ( A ^ j ) ) = ( ( abs ` A ) ^ j ) <-> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) ) )
17 abs1 
 |-  ( abs ` 1 ) = 1
18 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
19 18 fveq2d 
 |-  ( A e. CC -> ( abs ` ( A ^ 0 ) ) = ( abs ` 1 ) )
20 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
21 20 recnd 
 |-  ( A e. CC -> ( abs ` A ) e. CC )
22 21 exp0d 
 |-  ( A e. CC -> ( ( abs ` A ) ^ 0 ) = 1 )
23 17 19 22 3eqtr4a 
 |-  ( A e. CC -> ( abs ` ( A ^ 0 ) ) = ( ( abs ` A ) ^ 0 ) )
24 oveq1 
 |-  ( ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) -> ( ( abs ` ( A ^ k ) ) x. ( abs ` A ) ) = ( ( ( abs ` A ) ^ k ) x. ( abs ` A ) ) )
25 24 adantl 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) ) -> ( ( abs ` ( A ^ k ) ) x. ( abs ` A ) ) = ( ( ( abs ` A ) ^ k ) x. ( abs ` A ) ) )
26 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
27 26 fveq2d 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( abs ` ( A ^ ( k + 1 ) ) ) = ( abs ` ( ( A ^ k ) x. A ) ) )
28 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
29 simpl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> A e. CC )
30 absmul 
 |-  ( ( ( A ^ k ) e. CC /\ A e. CC ) -> ( abs ` ( ( A ^ k ) x. A ) ) = ( ( abs ` ( A ^ k ) ) x. ( abs ` A ) ) )
31 28 29 30 syl2anc 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( abs ` ( ( A ^ k ) x. A ) ) = ( ( abs ` ( A ^ k ) ) x. ( abs ` A ) ) )
32 27 31 eqtrd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( abs ` ( A ^ ( k + 1 ) ) ) = ( ( abs ` ( A ^ k ) ) x. ( abs ` A ) ) )
33 32 adantr 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) ) -> ( abs ` ( A ^ ( k + 1 ) ) ) = ( ( abs ` ( A ^ k ) ) x. ( abs ` A ) ) )
34 expp1 
 |-  ( ( ( abs ` A ) e. CC /\ k e. NN0 ) -> ( ( abs ` A ) ^ ( k + 1 ) ) = ( ( ( abs ` A ) ^ k ) x. ( abs ` A ) ) )
35 21 34 sylan 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( abs ` A ) ^ ( k + 1 ) ) = ( ( ( abs ` A ) ^ k ) x. ( abs ` A ) ) )
36 35 adantr 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) ) -> ( ( abs ` A ) ^ ( k + 1 ) ) = ( ( ( abs ` A ) ^ k ) x. ( abs ` A ) ) )
37 25 33 36 3eqtr4d 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) ) -> ( abs ` ( A ^ ( k + 1 ) ) ) = ( ( abs ` A ) ^ ( k + 1 ) ) )
38 4 8 12 16 23 37 nn0indd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )