# Metamath Proof Explorer

## Theorem cjexp

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

Ref Expression
Assertion cjexp ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to \stackrel{‾}{{{A}}^{{N}}}={\stackrel{‾}{{A}}}^{{N}}$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{j}=0\to {{A}}^{{j}}={{A}}^{0}$
2 1 fveq2d ${⊢}{j}=0\to \stackrel{‾}{{{A}}^{{j}}}=\stackrel{‾}{{{A}}^{0}}$
3 oveq2 ${⊢}{j}=0\to {\stackrel{‾}{{A}}}^{{j}}={\stackrel{‾}{{A}}}^{0}$
4 2 3 eqeq12d ${⊢}{j}=0\to \left(\stackrel{‾}{{{A}}^{{j}}}={\stackrel{‾}{{A}}}^{{j}}↔\stackrel{‾}{{{A}}^{0}}={\stackrel{‾}{{A}}}^{0}\right)$
5 oveq2 ${⊢}{j}={k}\to {{A}}^{{j}}={{A}}^{{k}}$
6 5 fveq2d ${⊢}{j}={k}\to \stackrel{‾}{{{A}}^{{j}}}=\stackrel{‾}{{{A}}^{{k}}}$
7 oveq2 ${⊢}{j}={k}\to {\stackrel{‾}{{A}}}^{{j}}={\stackrel{‾}{{A}}}^{{k}}$
8 6 7 eqeq12d ${⊢}{j}={k}\to \left(\stackrel{‾}{{{A}}^{{j}}}={\stackrel{‾}{{A}}}^{{j}}↔\stackrel{‾}{{{A}}^{{k}}}={\stackrel{‾}{{A}}}^{{k}}\right)$
9 oveq2 ${⊢}{j}={k}+1\to {{A}}^{{j}}={{A}}^{{k}+1}$
10 9 fveq2d ${⊢}{j}={k}+1\to \stackrel{‾}{{{A}}^{{j}}}=\stackrel{‾}{{{A}}^{{k}+1}}$
11 oveq2 ${⊢}{j}={k}+1\to {\stackrel{‾}{{A}}}^{{j}}={\stackrel{‾}{{A}}}^{{k}+1}$
12 10 11 eqeq12d ${⊢}{j}={k}+1\to \left(\stackrel{‾}{{{A}}^{{j}}}={\stackrel{‾}{{A}}}^{{j}}↔\stackrel{‾}{{{A}}^{{k}+1}}={\stackrel{‾}{{A}}}^{{k}+1}\right)$
13 oveq2 ${⊢}{j}={N}\to {{A}}^{{j}}={{A}}^{{N}}$
14 13 fveq2d ${⊢}{j}={N}\to \stackrel{‾}{{{A}}^{{j}}}=\stackrel{‾}{{{A}}^{{N}}}$
15 oveq2 ${⊢}{j}={N}\to {\stackrel{‾}{{A}}}^{{j}}={\stackrel{‾}{{A}}}^{{N}}$
16 14 15 eqeq12d ${⊢}{j}={N}\to \left(\stackrel{‾}{{{A}}^{{j}}}={\stackrel{‾}{{A}}}^{{j}}↔\stackrel{‾}{{{A}}^{{N}}}={\stackrel{‾}{{A}}}^{{N}}\right)$
17 exp0 ${⊢}{A}\in ℂ\to {{A}}^{0}=1$
18 17 fveq2d ${⊢}{A}\in ℂ\to \stackrel{‾}{{{A}}^{0}}=\stackrel{‾}{1}$
19 cjcl ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}\in ℂ$
20 exp0 ${⊢}\stackrel{‾}{{A}}\in ℂ\to {\stackrel{‾}{{A}}}^{0}=1$
21 1re ${⊢}1\in ℝ$
22 cjre ${⊢}1\in ℝ\to \stackrel{‾}{1}=1$
23 21 22 ax-mp ${⊢}\stackrel{‾}{1}=1$
24 20 23 syl6eqr ${⊢}\stackrel{‾}{{A}}\in ℂ\to {\stackrel{‾}{{A}}}^{0}=\stackrel{‾}{1}$
25 19 24 syl ${⊢}{A}\in ℂ\to {\stackrel{‾}{{A}}}^{0}=\stackrel{‾}{1}$
26 18 25 eqtr4d ${⊢}{A}\in ℂ\to \stackrel{‾}{{{A}}^{0}}={\stackrel{‾}{{A}}}^{0}$
27 expp1 ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}+1}={{A}}^{{k}}{A}$
28 27 fveq2d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \stackrel{‾}{{{A}}^{{k}+1}}=\stackrel{‾}{{{A}}^{{k}}{A}}$
29 expcl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}}\in ℂ$
30 simpl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {A}\in ℂ$
31 cjmul ${⊢}\left({{A}}^{{k}}\in ℂ\wedge {A}\in ℂ\right)\to \stackrel{‾}{{{A}}^{{k}}{A}}=\stackrel{‾}{{{A}}^{{k}}}\stackrel{‾}{{A}}$
32 29 30 31 syl2anc ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \stackrel{‾}{{{A}}^{{k}}{A}}=\stackrel{‾}{{{A}}^{{k}}}\stackrel{‾}{{A}}$
33 28 32 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \stackrel{‾}{{{A}}^{{k}+1}}=\stackrel{‾}{{{A}}^{{k}}}\stackrel{‾}{{A}}$
34 33 adantr ${⊢}\left(\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\wedge \stackrel{‾}{{{A}}^{{k}}}={\stackrel{‾}{{A}}}^{{k}}\right)\to \stackrel{‾}{{{A}}^{{k}+1}}=\stackrel{‾}{{{A}}^{{k}}}\stackrel{‾}{{A}}$
35 oveq1 ${⊢}\stackrel{‾}{{{A}}^{{k}}}={\stackrel{‾}{{A}}}^{{k}}\to \stackrel{‾}{{{A}}^{{k}}}\stackrel{‾}{{A}}={\stackrel{‾}{{A}}}^{{k}}\stackrel{‾}{{A}}$
36 expp1 ${⊢}\left(\stackrel{‾}{{A}}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {\stackrel{‾}{{A}}}^{{k}+1}={\stackrel{‾}{{A}}}^{{k}}\stackrel{‾}{{A}}$
37 19 36 sylan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {\stackrel{‾}{{A}}}^{{k}+1}={\stackrel{‾}{{A}}}^{{k}}\stackrel{‾}{{A}}$
38 37 eqcomd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {\stackrel{‾}{{A}}}^{{k}}\stackrel{‾}{{A}}={\stackrel{‾}{{A}}}^{{k}+1}$
39 35 38 sylan9eqr ${⊢}\left(\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\wedge \stackrel{‾}{{{A}}^{{k}}}={\stackrel{‾}{{A}}}^{{k}}\right)\to \stackrel{‾}{{{A}}^{{k}}}\stackrel{‾}{{A}}={\stackrel{‾}{{A}}}^{{k}+1}$
40 34 39 eqtrd ${⊢}\left(\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\wedge \stackrel{‾}{{{A}}^{{k}}}={\stackrel{‾}{{A}}}^{{k}}\right)\to \stackrel{‾}{{{A}}^{{k}+1}}={\stackrel{‾}{{A}}}^{{k}+1}$
41 4 8 12 16 26 40 nn0indd ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to \stackrel{‾}{{{A}}^{{N}}}={\stackrel{‾}{{A}}}^{{N}}$