efcj

Description: The exponential of a complex conjugate. Equation 3 of Gleason p. 308. (Contributed by NM, 29-Apr-2005) (Revised by Mario Carneiro, 28-Apr-2014)

		Ref	Expression
	Assertion	efcj	$⊢ A \in ℂ \to e^{\overline{A}} = \overline{e^{A}}$

Proof

Step	Hyp	Ref	Expression
1		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
2		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})$
3	2	efcvg	$⊢ \overline{A} \in ℂ \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) ⇝ e^{\overline{A}}$
4	1 3	syl	$⊢ A \in ℂ \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) ⇝ e^{\overline{A}}$
5		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
6		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
7	6	efcvg	$⊢ A \in ℂ \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})) ⇝ e^{A}$
8		seqex	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) \in V$
9	8	a1i	$⊢ A \in ℂ \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) \in V$
10		0zd	$⊢ A \in ℂ \to 0 \in ℤ$
11	6	eftval	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) (k) = \frac{A^{k}}{k!}$
12	11	adantl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) (k) = \frac{A^{k}}{k!}$
13		eftcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \frac{A^{k}}{k!} \in ℂ$
14	12 13	eqeltrd	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) (k) \in ℂ$
15	5 10 14	serf	$⊢ A \in ℂ \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})) : ℕ_{0} ⟶ ℂ$
16	15	ffvelcdmda	$⊢ (A \in ℂ \land j \in ℕ_{0}) \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})) (j) \in ℂ$
17		addcl	$⊢ (k \in ℂ \land m \in ℂ) \to k + m \in ℂ$
18	17	adantl	$⊢ ((A \in ℂ \land j \in ℕ_{0}) \land (k \in ℂ \land m \in ℂ)) \to k + m \in ℂ$
19		simpl	$⊢ (A \in ℂ \land j \in ℕ_{0}) \to A \in ℂ$
20		elfznn0	$⊢ k \in (0 \dots j) \to k \in ℕ_{0}$
21	19 20 14	syl2an	$⊢ ((A \in ℂ \land j \in ℕ_{0}) \land k \in (0 \dots j)) \to (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) (k) \in ℂ$
22		simpr	$⊢ (A \in ℂ \land j \in ℕ_{0}) \to j \in ℕ_{0}$
23	22 5	eleqtrdi	$⊢ (A \in ℂ \land j \in ℕ_{0}) \to j \in ℤ_{\geq 0}$
24		cjadd	$⊢ (k \in ℂ \land m \in ℂ) \to \overline{k + m} = \overline{k} + \overline{m}$
25	24	adantl	$⊢ ((A \in ℂ \land j \in ℕ_{0}) \land (k \in ℂ \land m \in ℂ)) \to \overline{k + m} = \overline{k} + \overline{m}$
26		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
27		faccl	$⊢ k \in ℕ_{0} \to k! \in ℕ$
28	27	adantl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to k! \in ℕ$
29	28	nncnd	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to k! \in ℂ$
30	28	nnne0d	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to k! \neq 0$
31	26 29 30	cjdivd	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{\frac{A^{k}}{k!}} = \frac{\overline{A^{k}}}{\overline{k!}}$
32		cjexp	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{A^{k}} = {\overline{A}}^{k}$
33	28	nnred	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to k! \in ℝ$
34	33	cjred	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{k!} = k!$
35	32 34	oveq12d	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \frac{\overline{A^{k}}}{\overline{k!}} = \frac{{\overline{A}}^{k}}{k!}$
36	31 35	eqtrd	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{\frac{A^{k}}{k!}} = \frac{{\overline{A}}^{k}}{k!}$
37	12	fveq2d	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{(n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) (k)} = \overline{\frac{A^{k}}{k!}}$
38	2	eftval	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!}) (k) = \frac{{\overline{A}}^{k}}{k!}$
39	38	adantl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!}) (k) = \frac{{\overline{A}}^{k}}{k!}$
40	36 37 39	3eqtr4d	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \overline{(n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) (k)} = (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!}) (k)$
41	19 20 40	syl2an	$⊢ ((A \in ℂ \land j \in ℕ_{0}) \land k \in (0 \dots j)) \to \overline{(n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) (k)} = (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!}) (k)$
42	18 21 23 25 41	seqhomo	$⊢ (A \in ℂ \land j \in ℕ_{0}) \to \overline{seq 0 (+ (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})) (j)} = seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) (j)$
43	42	eqcomd	$⊢ (A \in ℂ \land j \in ℕ_{0}) \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) (j) = \overline{seq 0 (+ (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})) (j)}$
44	5 7 9 10 16 43	climcj	$⊢ A \in ℂ \to seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) ⇝ \overline{e^{A}}$
45		climuni	$⊢ (seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) ⇝ e^{\overline{A}} \land seq 0 (+ (n \in ℕ_{0} ⟼ \frac{{\overline{A}}^{n}}{n!})) ⇝ \overline{e^{A}}) \to e^{\overline{A}} = \overline{e^{A}}$
46	4 44 45	syl2anc	$⊢ A \in ℂ \to e^{\overline{A}} = \overline{e^{A}}$

Metamath Proof Explorer

Theorem efcj

Proof