Metamath Proof Explorer


Theorem cjexp

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

Ref Expression
Assertion cjexp ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ∗ ‘ ( 𝐴𝑁 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑗 = 0 → ( 𝐴𝑗 ) = ( 𝐴 ↑ 0 ) )
2 1 fveq2d ( 𝑗 = 0 → ( ∗ ‘ ( 𝐴𝑗 ) ) = ( ∗ ‘ ( 𝐴 ↑ 0 ) ) )
3 oveq2 ( 𝑗 = 0 → ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) = ( ( ∗ ‘ 𝐴 ) ↑ 0 ) )
4 2 3 eqeq12d ( 𝑗 = 0 → ( ( ∗ ‘ ( 𝐴𝑗 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( ∗ ‘ ( 𝐴 ↑ 0 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 0 ) ) )
5 oveq2 ( 𝑗 = 𝑘 → ( 𝐴𝑗 ) = ( 𝐴𝑘 ) )
6 5 fveq2d ( 𝑗 = 𝑘 → ( ∗ ‘ ( 𝐴𝑗 ) ) = ( ∗ ‘ ( 𝐴𝑘 ) ) )
7 oveq2 ( 𝑗 = 𝑘 → ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) )
8 6 7 eqeq12d ( 𝑗 = 𝑘 → ( ( ∗ ‘ ( 𝐴𝑗 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( ∗ ‘ ( 𝐴𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) )
9 oveq2 ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
10 9 fveq2d ( 𝑗 = ( 𝑘 + 1 ) → ( ∗ ‘ ( 𝐴𝑗 ) ) = ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
11 oveq2 ( 𝑗 = ( 𝑘 + 1 ) → ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) )
12 10 11 eqeq12d ( 𝑗 = ( 𝑘 + 1 ) → ( ( ∗ ‘ ( 𝐴𝑗 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) )
13 oveq2 ( 𝑗 = 𝑁 → ( 𝐴𝑗 ) = ( 𝐴𝑁 ) )
14 13 fveq2d ( 𝑗 = 𝑁 → ( ∗ ‘ ( 𝐴𝑗 ) ) = ( ∗ ‘ ( 𝐴𝑁 ) ) )
15 oveq2 ( 𝑗 = 𝑁 → ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑁 ) )
16 14 15 eqeq12d ( 𝑗 = 𝑁 → ( ( ∗ ‘ ( 𝐴𝑗 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( ∗ ‘ ( 𝐴𝑁 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑁 ) ) )
17 exp0 ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
18 17 fveq2d ( 𝐴 ∈ ℂ → ( ∗ ‘ ( 𝐴 ↑ 0 ) ) = ( ∗ ‘ 1 ) )
19 cjcl ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
20 exp0 ( ( ∗ ‘ 𝐴 ) ∈ ℂ → ( ( ∗ ‘ 𝐴 ) ↑ 0 ) = 1 )
21 1re 1 ∈ ℝ
22 cjre ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 )
23 21 22 ax-mp ( ∗ ‘ 1 ) = 1
24 20 23 eqtr4di ( ( ∗ ‘ 𝐴 ) ∈ ℂ → ( ( ∗ ‘ 𝐴 ) ↑ 0 ) = ( ∗ ‘ 1 ) )
25 19 24 syl ( 𝐴 ∈ ℂ → ( ( ∗ ‘ 𝐴 ) ↑ 0 ) = ( ∗ ‘ 1 ) )
26 18 25 eqtr4d ( 𝐴 ∈ ℂ → ( ∗ ‘ ( 𝐴 ↑ 0 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 0 ) )
27 expp1 ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴𝑘 ) · 𝐴 ) )
28 27 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ∗ ‘ ( ( 𝐴𝑘 ) · 𝐴 ) ) )
29 expcl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
30 simpl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
31 cjmul ( ( ( 𝐴𝑘 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( ( 𝐴𝑘 ) · 𝐴 ) ) = ( ( ∗ ‘ ( 𝐴𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) )
32 29 30 31 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( ( 𝐴𝑘 ) · 𝐴 ) ) = ( ( ∗ ‘ ( 𝐴𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) )
33 28 32 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ∗ ‘ ( 𝐴𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) )
34 33 adantr ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ∗ ‘ ( 𝐴𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) → ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ∗ ‘ ( 𝐴𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) )
35 oveq1 ( ( ∗ ‘ ( 𝐴𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) → ( ( ∗ ‘ ( 𝐴𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) · ( ∗ ‘ 𝐴 ) ) )
36 expp1 ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) · ( ∗ ‘ 𝐴 ) ) )
37 19 36 sylan ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) · ( ∗ ‘ 𝐴 ) ) )
38 37 eqcomd ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) · ( ∗ ‘ 𝐴 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) )
39 35 38 sylan9eqr ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ∗ ‘ ( 𝐴𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) → ( ( ∗ ‘ ( 𝐴𝑘 ) ) · ( ∗ ‘ 𝐴 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) )
40 34 39 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ∗ ‘ ( 𝐴𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) ) → ( ∗ ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ∗ ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) )
41 4 8 12 16 26 40 nn0indd ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ∗ ‘ ( 𝐴𝑁 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑁 ) )