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 e. CC -> ( exp ` ( * ` A ) ) = ( * ` ( exp ` A ) ) )

Proof

Step Hyp Ref Expression
1 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
2 eqid 
 |-  ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) )
3 2 efcvg 
 |-  ( ( * ` A ) e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) ~~> ( exp ` ( * ` A ) ) )
4 1 3 syl 
 |-  ( A e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) ~~> ( exp ` ( * ` A ) ) )
5 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
6 eqid 
 |-  ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
7 6 efcvg 
 |-  ( A e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ~~> ( exp ` A ) )
8 seqex 
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) e. _V
9 8 a1i 
 |-  ( A e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) e. _V )
10 0zd 
 |-  ( A e. CC -> 0 e. ZZ )
11 6 eftval 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
12 11 adantl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
13 eftcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
14 12 13 eqeltrd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
15 5 10 14 serf 
 |-  ( A e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) : NN0 --> CC )
16 15 ffvelrnda 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` j ) e. CC )
17 addcl 
 |-  ( ( k e. CC /\ m e. CC ) -> ( k + m ) e. CC )
18 17 adantl 
 |-  ( ( ( A e. CC /\ j e. NN0 ) /\ ( k e. CC /\ m e. CC ) ) -> ( k + m ) e. CC )
19 simpl 
 |-  ( ( A e. CC /\ j e. NN0 ) -> A e. CC )
20 elfznn0 
 |-  ( k e. ( 0 ... j ) -> k e. NN0 )
21 19 20 14 syl2an 
 |-  ( ( ( A e. CC /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
22 simpr 
 |-  ( ( A e. CC /\ j e. NN0 ) -> j e. NN0 )
23 22 5 eleqtrdi 
 |-  ( ( A e. CC /\ j e. NN0 ) -> j e. ( ZZ>= ` 0 ) )
24 cjadd 
 |-  ( ( k e. CC /\ m e. CC ) -> ( * ` ( k + m ) ) = ( ( * ` k ) + ( * ` m ) ) )
25 24 adantl 
 |-  ( ( ( A e. CC /\ j e. NN0 ) /\ ( k e. CC /\ m e. CC ) ) -> ( * ` ( k + m ) ) = ( ( * ` k ) + ( * ` m ) ) )
26 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
27 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
28 27 adantl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ! ` k ) e. NN )
29 28 nncnd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ! ` k ) e. CC )
30 28 nnne0d 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ! ` k ) =/= 0 )
31 26 29 30 cjdivd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( ( A ^ k ) / ( ! ` k ) ) ) = ( ( * ` ( A ^ k ) ) / ( * ` ( ! ` k ) ) ) )
32 cjexp 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( A ^ k ) ) = ( ( * ` A ) ^ k ) )
33 28 nnred 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ! ` k ) e. RR )
34 33 cjred 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( ! ` k ) ) = ( ! ` k ) )
35 32 34 oveq12d 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( * ` ( A ^ k ) ) / ( * ` ( ! ` k ) ) ) = ( ( ( * ` A ) ^ k ) / ( ! ` k ) ) )
36 31 35 eqtrd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( ( A ^ k ) / ( ! ` k ) ) ) = ( ( ( * ` A ) ^ k ) / ( ! ` k ) ) )
37 12 fveq2d 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) ) = ( * ` ( ( A ^ k ) / ( ! ` k ) ) ) )
38 2 eftval 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( ( * ` A ) ^ k ) / ( ! ` k ) ) )
39 38 adantl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( ( * ` A ) ^ k ) / ( ! ` k ) ) )
40 36 37 39 3eqtr4d 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( * ` ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) ) = ( ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ` k ) )
41 19 20 40 syl2an 
 |-  ( ( ( A e. CC /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> ( * ` ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) ) = ( ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ` k ) )
42 18 21 23 25 41 seqhomo 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( * ` ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` j ) ) = ( seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) ` j ) )
43 42 eqcomd 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) ` j ) = ( * ` ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` j ) ) )
44 5 7 9 10 16 43 climcj 
 |-  ( A e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) ~~> ( * ` ( exp ` A ) ) )
45 climuni 
 |-  ( ( seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) ~~> ( exp ` ( * ` A ) ) /\ seq 0 ( + , ( n e. NN0 |-> ( ( ( * ` A ) ^ n ) / ( ! ` n ) ) ) ) ~~> ( * ` ( exp ` A ) ) ) -> ( exp ` ( * ` A ) ) = ( * ` ( exp ` A ) ) )
46 4 44 45 syl2anc 
 |-  ( A e. CC -> ( exp ` ( * ` A ) ) = ( * ` ( exp ` A ) ) )