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 ‘ 𝐴 ) ) )