cjexp

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

		Ref	Expression
	Assertion	cjexp	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \overline{A^{N}} = {\overline{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 {\overline{A}}^{j} = {\overline{A}}^{0}$
4	2 3	eqeq12d	$⊢ j = 0 \to (\overline{A^{j}} = {\overline{A}}^{j} \leftrightarrow \overline{A^{0}} = {\overline{A}}^{0})$
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 {\overline{A}}^{j} = {\overline{A}}^{k}$
8	6 7	eqeq12d	$⊢ j = k \to (\overline{A^{j}} = {\overline{A}}^{j} \leftrightarrow \overline{A^{k}} = {\overline{A}}^{k})$
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 {\overline{A}}^{j} = {\overline{A}}^{k + 1}$
12	10 11	eqeq12d	$⊢ j = k + 1 \to (\overline{A^{j}} = {\overline{A}}^{j} \leftrightarrow \overline{A^{k + 1}} = {\overline{A}}^{k + 1})$
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 {\overline{A}}^{j} = {\overline{A}}^{N}$
16	14 15	eqeq12d	$⊢ j = N \to (\overline{A^{j}} = {\overline{A}}^{j} \leftrightarrow \overline{A^{N}} = {\overline{A}}^{N})$
17		exp0	$⊢ A \in ℂ \to A^{0} = 1$
18	17	fveq2d	$⊢ A \in ℂ \to \overline{A^{0}} = \overline{1}$
19		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
20		exp0	$⊢ \overline{A} \in ℂ \to {\overline{A}}^{0} = 1$
21		1re	$⊢ 1 \in ℝ$
22		cjre	$⊢ 1 \in ℝ \to \overline{1} = 1$
23	21 22	ax-mp	$⊢ \overline{1} = 1$
24	20 23	syl6eqr	$⊢ \overline{A} \in ℂ \to {\overline{A}}^{0} = \overline{1}$
25	19 24	syl	$⊢ A \in ℂ \to {\overline{A}}^{0} = \overline{1}$
26	18 25	eqtr4d	$⊢ A \in ℂ \to \overline{A^{0}} = {\overline{A}}^{0}$
27		expp1	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k + 1} = A^{k} A$
28	27	fveq2d	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{A^{k + 1}} = \overline{A^{k} A}$
29		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
30		simpl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A \in ℂ$
31		cjmul	$⊢ (A^{k} \in ℂ \land A \in ℂ) \to \overline{A^{k} A} = \overline{A^{k}} \overline{A}$
32	29 30 31	syl2anc	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{A^{k} A} = \overline{A^{k}} \overline{A}$
33	28 32	eqtrd	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{A^{k + 1}} = \overline{A^{k}} \overline{A}$
34	33	adantr	$⊢ ((A \in ℂ \land k \in ℕ_{0}) \land \overline{A^{k}} = {\overline{A}}^{k}) \to \overline{A^{k + 1}} = \overline{A^{k}} \overline{A}$
35		oveq1	$⊢ \overline{A^{k}} = {\overline{A}}^{k} \to \overline{A^{k}} \overline{A} = {\overline{A}}^{k} \overline{A}$
36		expp1	$⊢ (\overline{A} \in ℂ \land k \in ℕ_{0}) \to {\overline{A}}^{k + 1} = {\overline{A}}^{k} \overline{A}$
37	19 36	sylan	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to {\overline{A}}^{k + 1} = {\overline{A}}^{k} \overline{A}$
38	37	eqcomd	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to {\overline{A}}^{k} \overline{A} = {\overline{A}}^{k + 1}$
39	35 38	sylan9eqr	$⊢ ((A \in ℂ \land k \in ℕ_{0}) \land \overline{A^{k}} = {\overline{A}}^{k}) \to \overline{A^{k}} \overline{A} = {\overline{A}}^{k + 1}$
40	34 39	eqtrd	$⊢ ((A \in ℂ \land k \in ℕ_{0}) \land \overline{A^{k}} = {\overline{A}}^{k}) \to \overline{A^{k + 1}} = {\overline{A}}^{k + 1}$
41	4 8 12 16 26 40	nn0indd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \overline{A^{N}} = {\overline{A}}^{N}$

Metamath Proof Explorer

Theorem cjexp

Proof