# 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( k e. CC /\ m e. CC ) -> ( k + m ) e. CC )`
` |-  ( ( ( 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 ) )`
` |-  ( ( k e. CC /\ m e. CC ) -> ( * ` ( k + m ) ) = ( ( * ` k ) + ( * ` m ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`