# Metamath Proof Explorer

## Theorem 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 {\mathrm{e}}^{\stackrel{‾}{{A}}}=\stackrel{‾}{{\mathrm{e}}^{{A}}}$

### Proof

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