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 {\mathbb{N}}_0\right)\to \overline{A^N}={\bar{A}}^N$$

Proof

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