Metamath Proof Explorer

Theorem efimpi

Description: The exponential function at _i times a real number less _pi . (Contributed by Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion efimpi 
|- ( A e. CC -> ( exp ` ( _i x. ( A - _pi ) ) ) = -u ( exp ` ( _i x. A ) ) )

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 subcl 
 |-  ( ( A e. CC /\ _pi e. CC ) -> ( A - _pi ) e. CC )
3 1 2 mpan2 
 |-  ( A e. CC -> ( A - _pi ) e. CC )
4 efival 
 |-  ( ( A - _pi ) e. CC -> ( exp ` ( _i x. ( A - _pi ) ) ) = ( ( cos ` ( A - _pi ) ) + ( _i x. ( sin ` ( A - _pi ) ) ) ) )
5 3 4 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. ( A - _pi ) ) ) = ( ( cos ` ( A - _pi ) ) + ( _i x. ( sin ` ( A - _pi ) ) ) ) )
6 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
7 ax-icn 
 |-  _i e. CC
8 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
9 mulcl 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. ( sin ` A ) ) e. CC )
10 7 8 9 sylancr 
 |-  ( A e. CC -> ( _i x. ( sin ` A ) ) e. CC )
11 6 10 negdid 
 |-  ( A e. CC -> -u ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) = ( -u ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) )
12 cosmpi 
 |-  ( A e. CC -> ( cos ` ( A - _pi ) ) = -u ( cos ` A ) )
13 sinmpi 
 |-  ( A e. CC -> ( sin ` ( A - _pi ) ) = -u ( sin ` A ) )
14 13 oveq2d 
 |-  ( A e. CC -> ( _i x. ( sin ` ( A - _pi ) ) ) = ( _i x. -u ( sin ` A ) ) )
15 mulneg2 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) )
16 7 8 15 sylancr 
 |-  ( A e. CC -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) )
17 14 16 eqtrd 
 |-  ( A e. CC -> ( _i x. ( sin ` ( A - _pi ) ) ) = -u ( _i x. ( sin ` A ) ) )
18 12 17 oveq12d 
 |-  ( A e. CC -> ( ( cos ` ( A - _pi ) ) + ( _i x. ( sin ` ( A - _pi ) ) ) ) = ( -u ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) )
19 11 18 eqtr4d 
 |-  ( A e. CC -> -u ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) = ( ( cos ` ( A - _pi ) ) + ( _i x. ( sin ` ( A - _pi ) ) ) ) )
20 5 19 eqtr4d 
 |-  ( A e. CC -> ( exp ` ( _i x. ( A - _pi ) ) ) = -u ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
21 efival 
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
22 21 negeqd 
 |-  ( A e. CC -> -u ( exp ` ( _i x. A ) ) = -u ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
23 20 22 eqtr4d 
 |-  ( A e. CC -> ( exp ` ( _i x. ( A - _pi ) ) ) = -u ( exp ` ( _i x. A ) ) )