Metamath Proof Explorer

Theorem sinperlem

Description: Lemma for sinper and cosper . (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

Ref Expression
Hypotheses sinperlem.1 
|- ( A e. CC -> ( F ` A ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )
sinperlem.2 
|- ( ( A + ( K x. ( 2 x. _pi ) ) ) e. CC -> ( F ` ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) ) / D ) )
Assertion sinperlem 
|- ( ( A e. CC /\ K e. ZZ ) -> ( F ` ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( F ` A ) )

Proof

Step Hyp Ref Expression
1 sinperlem.1 
 |-  ( A e. CC -> ( F ` A ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )
2 sinperlem.2 
 |-  ( ( A + ( K x. ( 2 x. _pi ) ) ) e. CC -> ( F ` ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) ) / D ) )
3 zcn 
 |-  ( K e. ZZ -> K e. CC )
4 2cn 
 |-  2 e. CC
5 picn 
 |-  _pi e. CC
6 4 5 mulcli 
 |-  ( 2 x. _pi ) e. CC
7 mulcl 
 |-  ( ( K e. CC /\ ( 2 x. _pi ) e. CC ) -> ( K x. ( 2 x. _pi ) ) e. CC )
8 3 6 7 sylancl 
 |-  ( K e. ZZ -> ( K x. ( 2 x. _pi ) ) e. CC )
9 ax-icn 
 |-  _i e. CC
10 adddi 
 |-  ( ( _i e. CC /\ A e. CC /\ ( K x. ( 2 x. _pi ) ) e. CC ) -> ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( _i x. A ) + ( _i x. ( K x. ( 2 x. _pi ) ) ) ) )
11 9 10 mp3an1 
 |-  ( ( A e. CC /\ ( K x. ( 2 x. _pi ) ) e. CC ) -> ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( _i x. A ) + ( _i x. ( K x. ( 2 x. _pi ) ) ) ) )
12 8 11 sylan2 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( _i x. A ) + ( _i x. ( K x. ( 2 x. _pi ) ) ) ) )
13 mul12 
 |-  ( ( _i e. CC /\ K e. CC /\ ( 2 x. _pi ) e. CC ) -> ( _i x. ( K x. ( 2 x. _pi ) ) ) = ( K x. ( _i x. ( 2 x. _pi ) ) ) )
14 9 6 13 mp3an13 
 |-  ( K e. CC -> ( _i x. ( K x. ( 2 x. _pi ) ) ) = ( K x. ( _i x. ( 2 x. _pi ) ) ) )
15 3 14 syl 
 |-  ( K e. ZZ -> ( _i x. ( K x. ( 2 x. _pi ) ) ) = ( K x. ( _i x. ( 2 x. _pi ) ) ) )
16 9 6 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
17 mulcom 
 |-  ( ( K e. CC /\ ( _i x. ( 2 x. _pi ) ) e. CC ) -> ( K x. ( _i x. ( 2 x. _pi ) ) ) = ( ( _i x. ( 2 x. _pi ) ) x. K ) )
18 3 16 17 sylancl 
 |-  ( K e. ZZ -> ( K x. ( _i x. ( 2 x. _pi ) ) ) = ( ( _i x. ( 2 x. _pi ) ) x. K ) )
19 15 18 eqtrd 
 |-  ( K e. ZZ -> ( _i x. ( K x. ( 2 x. _pi ) ) ) = ( ( _i x. ( 2 x. _pi ) ) x. K ) )
20 19 adantl 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( _i x. ( K x. ( 2 x. _pi ) ) ) = ( ( _i x. ( 2 x. _pi ) ) x. K ) )
21 20 oveq2d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( ( _i x. A ) + ( _i x. ( K x. ( 2 x. _pi ) ) ) ) = ( ( _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) )
22 12 21 eqtrd 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) )
23 22 fveq2d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) = ( exp ` ( ( _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) )
24 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
25 9 24 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
26 efper 
 |-  ( ( ( _i x. A ) e. CC /\ K e. ZZ ) -> ( exp ` ( ( _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) = ( exp ` ( _i x. A ) ) )
27 25 26 sylan 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( ( _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. K ) ) ) = ( exp ` ( _i x. A ) ) )
28 23 27 eqtrd 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) = ( exp ` ( _i x. A ) ) )
29 negicn 
 |-  -u _i e. CC
30 adddi 
 |-  ( ( -u _i e. CC /\ A e. CC /\ ( K x. ( 2 x. _pi ) ) e. CC ) -> ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( -u _i x. A ) + ( -u _i x. ( K x. ( 2 x. _pi ) ) ) ) )
31 29 30 mp3an1 
 |-  ( ( A e. CC /\ ( K x. ( 2 x. _pi ) ) e. CC ) -> ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( -u _i x. A ) + ( -u _i x. ( K x. ( 2 x. _pi ) ) ) ) )
32 8 31 sylan2 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( -u _i x. A ) + ( -u _i x. ( K x. ( 2 x. _pi ) ) ) ) )
33 19 negeqd 
 |-  ( K e. ZZ -> -u ( _i x. ( K x. ( 2 x. _pi ) ) ) = -u ( ( _i x. ( 2 x. _pi ) ) x. K ) )
34 mulneg1 
 |-  ( ( _i e. CC /\ ( K x. ( 2 x. _pi ) ) e. CC ) -> ( -u _i x. ( K x. ( 2 x. _pi ) ) ) = -u ( _i x. ( K x. ( 2 x. _pi ) ) ) )
35 9 8 34 sylancr 
 |-  ( K e. ZZ -> ( -u _i x. ( K x. ( 2 x. _pi ) ) ) = -u ( _i x. ( K x. ( 2 x. _pi ) ) ) )
36 mulneg2 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) e. CC /\ K e. CC ) -> ( ( _i x. ( 2 x. _pi ) ) x. -u K ) = -u ( ( _i x. ( 2 x. _pi ) ) x. K ) )
37 16 3 36 sylancr 
 |-  ( K e. ZZ -> ( ( _i x. ( 2 x. _pi ) ) x. -u K ) = -u ( ( _i x. ( 2 x. _pi ) ) x. K ) )
38 33 35 37 3eqtr4d 
 |-  ( K e. ZZ -> ( -u _i x. ( K x. ( 2 x. _pi ) ) ) = ( ( _i x. ( 2 x. _pi ) ) x. -u K ) )
39 38 adantl 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( -u _i x. ( K x. ( 2 x. _pi ) ) ) = ( ( _i x. ( 2 x. _pi ) ) x. -u K ) )
40 39 oveq2d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( ( -u _i x. A ) + ( -u _i x. ( K x. ( 2 x. _pi ) ) ) ) = ( ( -u _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. -u K ) ) )
41 32 40 eqtrd 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( -u _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. -u K ) ) )
42 41 fveq2d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) = ( exp ` ( ( -u _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. -u K ) ) ) )
43 mulcl 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
44 29 43 mpan 
 |-  ( A e. CC -> ( -u _i x. A ) e. CC )
45 znegcl 
 |-  ( K e. ZZ -> -u K e. ZZ )
46 efper 
 |-  ( ( ( -u _i x. A ) e. CC /\ -u K e. ZZ ) -> ( exp ` ( ( -u _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. -u K ) ) ) = ( exp ` ( -u _i x. A ) ) )
47 44 45 46 syl2an 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( ( -u _i x. A ) + ( ( _i x. ( 2 x. _pi ) ) x. -u K ) ) ) = ( exp ` ( -u _i x. A ) ) )
48 42 47 eqtrd 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) = ( exp ` ( -u _i x. A ) ) )
49 28 48 oveq12d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) ) = ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) )
50 49 oveq1d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) ) / D ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )
51 addcl 
 |-  ( ( A e. CC /\ ( K x. ( 2 x. _pi ) ) e. CC ) -> ( A + ( K x. ( 2 x. _pi ) ) ) e. CC )
52 8 51 sylan2 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( A + ( K x. ( 2 x. _pi ) ) ) e. CC )
53 52 2 syl 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( F ` ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. _pi ) ) ) ) ) ) / D ) )
54 1 adantr 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( F ` A ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )
55 50 53 54 3eqtr4d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( F ` ( A + ( K x. ( 2 x. _pi ) ) ) ) = ( F ` A ) )