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 ) → ( ∗ ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑁 ) )