Theorem efcj 7336

Description: Exponential function of a complex conjugate. Equation 3 of [Gleason] p. 308.

Hypothesis

Ref	Expression
efcj.1	|- A e. CC

Assertion

Ref	Expression
efcj	|- (exp` (*` A)) = (*` (exp` A))

Proof of Theorem efcj

Step	Hyp	Ref	Expression
1		efcj.1	. . . 4 |- A e. CC
2	1	cjcl 6767	. . 3 |- (*` A) e. CC
3		efvalt 7308	. . 3 |- ((*` A) e. CC -> (exp` (*` A)) = sum_k e. NN0 (((*` A)^k) / (!` k)))
4	2, 3	ax-mp 7	. 2 |- (exp` (*` A)) = sum_k e. NN0 (((*` A)^k) / (!` k))
5		nn0uz 6438	. . 3 |- NN0 = (ZZ>` 0)
6	5	sumeq1i 6987	. 2 |- sum_k e. NN0 (((*` A)^k) / (!` k)) = sum_k e. (ZZ>` 0)(((*` A)^k) / (!` k))
7		0z 6146	. . 3 |- 0 e. ZZ
8		addex 5317	. . . . 5 |- + e. V
9		nn0ex 6105	. . . . . 6 |- NN0 e. V
10	9	opabex2 3610	. . . . 5 |- {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))} e. V
11	8, 10	seq0seqz 6542	. . . 4 |- ( + seq0 {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))}) = (<.0, + >. seq {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))})
12		fvex 3732	. . . . 5 |- (exp` A) e. V
13		oprex 3983	. . . . 5 |- ( + seq0 {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))}) e. V
14		eqid 1475	. . . . . . 7 |- {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))} = {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}
15	14	efcvg 7314	. . . . . 6 |- (A e. CC -> ( + seq0 {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}) ~~> (exp` A))
16	1, 15	ax-mp 7	. . . . 5 |- ( + seq0 {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}) ~~> (exp` A)
17		elnn0uz 6441	. . . . . 6 |- (j e. NN0 <-> j e. (ZZ>` 0))
18		eftclt 7303	. . . . . . . . . 10 |- ((A e. CC /\ k e. NN0) -> ((A^k) / (!` k)) e. CC)
19	1, 18	mpan 695	. . . . . . . . 9 |- (k e. NN0 -> ((A^k) / (!` k)) e. CC)
20	14, 19	fopab 3827	. . . . . . . 8 |- {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}:NN0-->CC
21	20	ser0cl1 6564	. . . . . . 7 |- (j e. NN0 -> (( + seq0 {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))})` j) e. CC)
22	9	opabex2 3610	. . . . . . . 8 |- {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))} e. V
23	14	eftval 7316	. . . . . . . . . 10 |- (m e. NN0 -> ({<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}` m) = ((A^m) / (!` m)))
24		eftclt 7303	. . . . . . . . . . 11 |- ((A e. CC /\ m e. NN0) -> ((A^m) / (!` m)) e. CC)
25	1, 24	mpan 695	. . . . . . . . . 10 |- (m e. NN0 -> ((A^m) / (!` m)) e. CC)
26	23, 25	eqeltrd 1548	. . . . . . . . 9 |- (m e. NN0 -> ({<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}` m) e. CC)
27		cjdivt 6889	. . . . . . . . . . . 12 |- (((A^m) e. CC /\ (!` m) e. CC /\ (!` m) =/= 0) -> (*` ((A^m) / (!` m))) = ((*` (A^m)) / (*` (!` m))))
28		expclt 6581	. . . . . . . . . . . . 13 |- ((A e. CC /\ m e. NN0) -> (A^m) e. CC)
29	1, 28	mpan 695	. . . . . . . . . . . 12 |- (m e. NN0 -> (A^m) e. CC)
30		facclt 6940	. . . . . . . . . . . . . 14 |- (m e. NN0 -> (!` m) e. NN)
31		nnret 5929	. . . . . . . . . . . . . 14 |- ((!` m) e. NN -> (!` m) e. RR)
32	30, 31	syl 10	. . . . . . . . . . . . 13 |- (m e. NN0 -> (!` m) e. RR)
33	32	recnd 5315	. . . . . . . . . . . 12 |- (m e. NN0 -> (!` m) e. CC)
34		facne0t 6941	. . . . . . . . . . . 12 |- (m e. NN0 -> (!` m) =/= 0)
35	27, 29, 33, 34	syl3anc 858	. . . . . . . . . . 11 |- (m e. NN0 -> (*` ((A^m) / (!` m))) = ((*` (A^m)) / (*` (!` m))))
36		cjexpt 6817	. . . . . . . . . . . . 13 |- ((A e. CC /\ m e. NN0) -> (*` (A^m)) = ((*` A)^m))
37	1, 36	mpan 695	. . . . . . . . . . . 12 |- (m e. NN0 -> (*` (A^m)) = ((*` A)^m))
38		cjret 6810	. . . . . . . . . . . . 13 |- ((!` m) e. RR -> (*` (!` m)) = (!` m))
39	32, 38	syl 10	. . . . . . . . . . . 12 |- (m e. NN0 -> (*` (!` m)) = (!` m))
40	37, 39	opreq12d 3978	. . . . . . . . . . 11 |- (m e. NN0 -> ((*` (A^m)) / (*` (!` m))) = (((*` A)^m) / (!` m)))
41	35, 40	eqtr2d 1508	. . . . . . . . . 10 |- (m e. NN0 -> (((*` A)^m) / (!` m)) = (*` ((A^m) / (!` m))))
42		eqid 1475	. . . . . . . . . . 11 |- {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))} = {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))}
43	42	eftval 7316	. . . . . . . . . 10 |- (m e. NN0 -> ({<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))}` m) = (((*` A)^m) / (!` m)))
44	23	fveq2d 3728	. . . . . . . . . 10 |- (m e. NN0 -> (*` ({<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}` m)) = (*` ((A^m) / (!` m))))
45	41, 43, 44	3eqtr4d 1517	. . . . . . . . 9 |- (m e. NN0 -> ({<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))}` m) = (*` ({<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}` m)))
46	26, 45	jca 288	. . . . . . . 8 |- (m e. NN0 -> (({<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}` m) e. CC /\ ({<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))}` m) = (*` ({<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))}` m))))
47	22, 10, 46	ser0cj 7065	. . . . . . 7 |- (j e. NN0 -> (( + seq0 {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))})` j) = (*` (( + seq0 {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))})` j)))
48	21, 47	jca 288	. . . . . 6 |- (j e. NN0 -> ((( + seq0 {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))})` j) e. CC /\ (( + seq0 {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))})` j) = (*` (( + seq0 {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))})` j))))
49	17, 48	sylbir 201	. . . . 5 |- (j e. (ZZ>` 0) -> ((( + seq0 {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))})` j) e. CC /\ (( + seq0 {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))})` j) = (*` (( + seq0 {<.k, y>. | (k e. NN0 /\ y = ((A^k) / (!` k)))})` j))))
50	12, 13, 7, 16, 49	climcj 7150	. . . 4 |- ( + seq0 {<.k, y>. | (k e. NN0 /\ y = (((*` A)^k) / (!` k)))}) ~~> (*` (exp` A))
51	11, 50	eqbrtrr 2636	. . 3 |- (<.0, + >. seq {<.k, y>. | (