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 ( 𝐴 ∈ ℂ → ( exp ‘ ( ∗ ‘ 𝐴 ) ) = ( ∗ ‘ ( exp ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 cjcl ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
2 eqid ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
3 2 efcvg ( ( ∗ ‘ 𝐴 ) ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( exp ‘ ( ∗ ‘ 𝐴 ) ) )
4 1 3 syl ( 𝐴 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( exp ‘ ( ∗ ‘ 𝐴 ) ) )
5 nn0uz 0 = ( ℤ ‘ 0 )
6 eqid ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) )
7 6 efcvg ( 𝐴 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( exp ‘ 𝐴 ) )
8 seqex seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ V
9 8 a1i ( 𝐴 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ V )
10 0zd ( 𝐴 ∈ ℂ → 0 ∈ ℤ )
11 6 eftval ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) )
12 11 adantl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) )
13 eftcl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
14 12 13 eqeltrd ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
15 5 10 14 serf ( 𝐴 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) : ℕ0 ⟶ ℂ )
16 15 ffvelrnda ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ∈ ℂ )
17 addcl ( ( 𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝑘 + 𝑚 ) ∈ ℂ )
18 17 adantl ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝑘 + 𝑚 ) ∈ ℂ )
19 simpl ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
20 elfznn0 ( 𝑘 ∈ ( 0 ... 𝑗 ) → 𝑘 ∈ ℕ0 )
21 19 20 14 syl2an ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
22 simpr ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
23 22 5 eleqtrdi ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ( ℤ ‘ 0 ) )
24 cjadd ( ( 𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ∗ ‘ ( 𝑘 + 𝑚 ) ) = ( ( ∗ ‘ 𝑘 ) + ( ∗ ‘ 𝑚 ) ) )
25 24 adantl ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( ∗ ‘ ( 𝑘 + 𝑚 ) ) = ( ( ∗ ‘ 𝑘 ) + ( ∗ ‘ 𝑚 ) ) )
26 expcl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
27 faccl ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
28 27 adantl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℕ )
29 28 nncnd ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℂ )
30 28 nnne0d ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ≠ 0 )
31 26 29 30 cjdivd ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( ( ∗ ‘ ( 𝐴𝑘 ) ) / ( ∗ ‘ ( ! ‘ 𝑘 ) ) ) )
32 cjexp ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( 𝐴𝑘 ) ) = ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) )
33 28 nnred ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℝ )
34 33 cjred ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( ! ‘ 𝑘 ) ) = ( ! ‘ 𝑘 ) )
35 32 34 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ‘ ( 𝐴𝑘 ) ) / ( ∗ ‘ ( ! ‘ 𝑘 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
36 31 35 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
37 12 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) = ( ∗ ‘ ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
38 2 eftval ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
39 38 adantl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
40 36 37 39 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) = ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
41 19 20 40 syl2an ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( ∗ ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) = ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
42 18 21 23 25 41 seqhomo ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( ∗ ‘ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) )
43 42 eqcomd ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) = ( ∗ ‘ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ) )
44 5 7 9 10 16 43 climcj ( 𝐴 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( ∗ ‘ ( exp ‘ 𝐴 ) ) )
45 climuni ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( exp ‘ ( ∗ ‘ 𝐴 ) ) ∧ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( ∗ ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( ∗ ‘ ( exp ‘ 𝐴 ) ) ) → ( exp ‘ ( ∗ ‘ 𝐴 ) ) = ( ∗ ‘ ( exp ‘ 𝐴 ) ) )
46 4 44 45 syl2anc ( 𝐴 ∈ ℂ → ( exp ‘ ( ∗ ‘ 𝐴 ) ) = ( ∗ ‘ ( exp ‘ 𝐴 ) ) )