Metamath Proof Explorer

Theorem cjexp

Description: Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = 0 -> ( A ^ j ) = ( A ^ 0 ) )
2 1 fveq2d 
 |-  ( j = 0 -> ( * ` ( A ^ j ) ) = ( * ` ( A ^ 0 ) ) )
3 oveq2 
 |-  ( j = 0 -> ( ( * ` A ) ^ j ) = ( ( * ` A ) ^ 0 ) )
4 2 3 eqeq12d 
 |-  ( j = 0 -> ( ( * ` ( A ^ j ) ) = ( ( * ` A ) ^ j ) <-> ( * ` ( A ^ 0 ) ) = ( ( * ` A ) ^ 0 ) ) )
5 oveq2 
 |-  ( j = k -> ( A ^ j ) = ( A ^ k ) )
6 5 fveq2d 
 |-  ( j = k -> ( * ` ( A ^ j ) ) = ( * ` ( A ^ k ) ) )
7 oveq2 
 |-  ( j = k -> ( ( * ` A ) ^ j ) = ( ( * ` A ) ^ k ) )
8 6 7 eqeq12d 
 |-  ( j = k -> ( ( * ` ( A ^ j ) ) = ( ( * ` A ) ^ j ) <-> ( * ` ( A ^ k ) ) = ( ( * ` A ) ^ k ) ) )
9 oveq2 
 |-  ( j = ( k + 1 ) -> ( A ^ j ) = ( A ^ ( k + 1 ) ) )
10 9 fveq2d 
 |-  ( j = ( k + 1 ) -> ( * ` ( A ^ j ) ) = ( * ` ( A ^ ( k + 1 ) ) ) )
11 oveq2 
 |-  ( j = ( k + 1 ) -> ( ( * ` A ) ^ j ) = ( ( * ` A ) ^ ( k + 1 ) ) )
12 10 11 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( ( * ` ( A ^ j ) ) = ( ( * ` A ) ^ j ) <-> ( * ` ( A ^ ( k + 1 ) ) ) = ( ( * ` A ) ^ ( k + 1 ) ) ) )
13 oveq2 
 |-  ( j = N -> ( A ^ j ) = ( A ^ N ) )
14 13 fveq2d 
 |-  ( j = N -> ( * ` ( A ^ j ) ) = ( * ` ( A ^ N ) ) )
15 oveq2 
 |-  ( j = N -> ( ( * ` A ) ^ j ) = ( ( * ` A ) ^ N ) )
16 14 15 eqeq12d 
 |-  ( j = N -> ( ( * ` ( A ^ j ) ) = ( ( * ` A ) ^ j ) <-> ( * ` ( A ^ N ) ) = ( ( * ` A ) ^ N ) ) )
17 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
18 17 fveq2d 
 |-  ( A e. CC -> ( * ` ( A ^ 0 ) ) = ( * ` 1 ) )
19 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
20 exp0 
 |-  ( ( * ` A ) e. CC -> ( ( * ` A ) ^ 0 ) = 1 )
21 1re 
 |-  1 e. RR
22 cjre 
 |-  ( 1 e. RR -> ( * ` 1 ) = 1 )
23 21 22 ax-mp 
 |-  ( * ` 1 ) = 1
24 20 23 eqtr4di 
 |-  ( ( * ` A ) e. CC -> ( ( * ` A ) ^ 0 ) = ( * ` 1 ) )
25 19 24 syl 
 |-  ( A e. CC -> ( ( * ` A ) ^ 0 ) = ( * ` 1 ) )
26 18 25 eqtr4d 
 |-  ( A e. CC -> ( * ` ( A ^ 0 ) ) = ( ( * ` A ) ^ 0 ) )
27 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
28 27 fveq2d 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( A ^ ( k + 1 ) ) ) = ( * ` ( ( A ^ k ) x. A ) ) )
29 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
30 simpl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> A e. CC )
31 cjmul 
 |-  ( ( ( A ^ k ) e. CC /\ A e. CC ) -> ( * ` ( ( A ^ k ) x. A ) ) = ( ( * ` ( A ^ k ) ) x. ( * ` A ) ) )
32 29 30 31 syl2anc 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( ( A ^ k ) x. A ) ) = ( ( * ` ( A ^ k ) ) x. ( * ` A ) ) )
33 28 32 eqtrd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( A ^ ( k + 1 ) ) ) = ( ( * ` ( A ^ k ) ) x. ( * ` A ) ) )
34 33 adantr 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( * ` ( A ^ k ) ) = ( ( * ` A ) ^ k ) ) -> ( * ` ( A ^ ( k + 1 ) ) ) = ( ( * ` ( A ^ k ) ) x. ( * ` A ) ) )
35 oveq1 
 |-  ( ( * ` ( A ^ k ) ) = ( ( * ` A ) ^ k ) -> ( ( * ` ( A ^ k ) ) x. ( * ` A ) ) = ( ( ( * ` A ) ^ k ) x. ( * ` A ) ) )
36 expp1 
 |-  ( ( ( * ` A ) e. CC /\ k e. NN0 ) -> ( ( * ` A ) ^ ( k + 1 ) ) = ( ( ( * ` A ) ^ k ) x. ( * ` A ) ) )
37 19 36 sylan 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( * ` A ) ^ ( k + 1 ) ) = ( ( ( * ` A ) ^ k ) x. ( * ` A ) ) )
38 37 eqcomd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( ( * ` A ) ^ k ) x. ( * ` A ) ) = ( ( * ` A ) ^ ( k + 1 ) ) )
39 35 38 sylan9eqr 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( * ` ( A ^ k ) ) = ( ( * ` A ) ^ k ) ) -> ( ( * ` ( A ^ k ) ) x. ( * ` A ) ) = ( ( * ` A ) ^ ( k + 1 ) ) )
40 34 39 eqtrd 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( * ` ( A ^ k ) ) = ( ( * ` A ) ^ k ) ) -> ( * ` ( A ^ ( k + 1 ) ) ) = ( ( * ` A ) ^ ( k + 1 ) ) )
41 4 8 12 16 26 40 nn0indd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( * ` ( A ^ N ) ) = ( ( * ` A ) ^ N ) )