Metamath Proof Explorer

Theorem abssinper

Description: The absolute value of sine has period _pi . (Contributed by NM, 17-Aug-2008)

Ref Expression
Assertion abssinper 
|- ( ( A e. CC /\ K e. ZZ ) -> ( abs ` ( sin ` ( A + ( K x. _pi ) ) ) ) = ( abs ` ( sin ` A ) ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( K e. ZZ -> K e. CC )
2 halfcl 
 |-  ( K e. CC -> ( K / 2 ) e. CC )
3 2cn 
 |-  2 e. CC
4 picn 
 |-  _pi e. CC
5 mulass 
 |-  ( ( ( K / 2 ) e. CC /\ 2 e. CC /\ _pi e. CC ) -> ( ( ( K / 2 ) x. 2 ) x. _pi ) = ( ( K / 2 ) x. ( 2 x. _pi ) ) )
6 3 4 5 mp3an23 
 |-  ( ( K / 2 ) e. CC -> ( ( ( K / 2 ) x. 2 ) x. _pi ) = ( ( K / 2 ) x. ( 2 x. _pi ) ) )
7 2 6 syl 
 |-  ( K e. CC -> ( ( ( K / 2 ) x. 2 ) x. _pi ) = ( ( K / 2 ) x. ( 2 x. _pi ) ) )
8 2ne0 
 |-  2 =/= 0
9 divcan1 
 |-  ( ( K e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( K / 2 ) x. 2 ) = K )
10 3 8 9 mp3an23 
 |-  ( K e. CC -> ( ( K / 2 ) x. 2 ) = K )
11 10 oveq1d 
 |-  ( K e. CC -> ( ( ( K / 2 ) x. 2 ) x. _pi ) = ( K x. _pi ) )
12 7 11 eqtr3d 
 |-  ( K e. CC -> ( ( K / 2 ) x. ( 2 x. _pi ) ) = ( K x. _pi ) )
13 1 12 syl 
 |-  ( K e. ZZ -> ( ( K / 2 ) x. ( 2 x. _pi ) ) = ( K x. _pi ) )
14 13 adantl 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( ( K / 2 ) x. ( 2 x. _pi ) ) = ( K x. _pi ) )
15 14 oveq2d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( A + ( ( K / 2 ) x. ( 2 x. _pi ) ) ) = ( A + ( K x. _pi ) ) )
16 15 fveq2d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( sin ` ( A + ( ( K / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( A + ( K x. _pi ) ) ) )
17 16 eqcomd 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( sin ` ( A + ( K x. _pi ) ) ) = ( sin ` ( A + ( ( K / 2 ) x. ( 2 x. _pi ) ) ) ) )
18 17 adantr 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( K / 2 ) e. ZZ ) -> ( sin ` ( A + ( K x. _pi ) ) ) = ( sin ` ( A + ( ( K / 2 ) x. ( 2 x. _pi ) ) ) ) )
19 sinper 
 |-  ( ( A e. CC /\ ( K / 2 ) e. ZZ ) -> ( sin ` ( A + ( ( K / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` A ) )
20 19 adantlr 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( K / 2 ) e. ZZ ) -> ( sin ` ( A + ( ( K / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` A ) )
21 18 20 eqtrd 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( K / 2 ) e. ZZ ) -> ( sin ` ( A + ( K x. _pi ) ) ) = ( sin ` A ) )
22 21 fveq2d 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( K / 2 ) e. ZZ ) -> ( abs ` ( sin ` ( A + ( K x. _pi ) ) ) ) = ( abs ` ( sin ` A ) ) )
23 peano2cn 
 |-  ( K e. CC -> ( K + 1 ) e. CC )
24 halfcl 
 |-  ( ( K + 1 ) e. CC -> ( ( K + 1 ) / 2 ) e. CC )
25 23 24 syl 
 |-  ( K e. CC -> ( ( K + 1 ) / 2 ) e. CC )
26 3 4 mulcli 
 |-  ( 2 x. _pi ) e. CC
27 mulcl 
 |-  ( ( ( ( K + 1 ) / 2 ) e. CC /\ ( 2 x. _pi ) e. CC ) -> ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) e. CC )
28 25 26 27 sylancl 
 |-  ( K e. CC -> ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) e. CC )
29 subadd23 
 |-  ( ( A e. CC /\ _pi e. CC /\ ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) e. CC ) -> ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) = ( A + ( ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) - _pi ) ) )
30 4 29 mp3an2 
 |-  ( ( A e. CC /\ ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) e. CC ) -> ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) = ( A + ( ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) - _pi ) ) )
31 28 30 sylan2 
 |-  ( ( A e. CC /\ K e. CC ) -> ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) = ( A + ( ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) - _pi ) ) )
32 divcan1 
 |-  ( ( ( K + 1 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( ( K + 1 ) / 2 ) x. 2 ) = ( K + 1 ) )
33 3 8 32 mp3an23 
 |-  ( ( K + 1 ) e. CC -> ( ( ( K + 1 ) / 2 ) x. 2 ) = ( K + 1 ) )
34 23 33 syl 
 |-  ( K e. CC -> ( ( ( K + 1 ) / 2 ) x. 2 ) = ( K + 1 ) )
35 34 oveq1d 
 |-  ( K e. CC -> ( ( ( ( K + 1 ) / 2 ) x. 2 ) x. _pi ) = ( ( K + 1 ) x. _pi ) )
36 ax-1cn 
 |-  1 e. CC
37 adddir 
 |-  ( ( K e. CC /\ 1 e. CC /\ _pi e. CC ) -> ( ( K + 1 ) x. _pi ) = ( ( K x. _pi ) + ( 1 x. _pi ) ) )
38 36 4 37 mp3an23 
 |-  ( K e. CC -> ( ( K + 1 ) x. _pi ) = ( ( K x. _pi ) + ( 1 x. _pi ) ) )
39 35 38 eqtrd 
 |-  ( K e. CC -> ( ( ( ( K + 1 ) / 2 ) x. 2 ) x. _pi ) = ( ( K x. _pi ) + ( 1 x. _pi ) ) )
40 4 mulid2i 
 |-  ( 1 x. _pi ) = _pi
41 40 oveq2i 
 |-  ( ( K x. _pi ) + ( 1 x. _pi ) ) = ( ( K x. _pi ) + _pi )
42 39 41 eqtr2di 
 |-  ( K e. CC -> ( ( K x. _pi ) + _pi ) = ( ( ( ( K + 1 ) / 2 ) x. 2 ) x. _pi ) )
43 mulass 
 |-  ( ( ( ( K + 1 ) / 2 ) e. CC /\ 2 e. CC /\ _pi e. CC ) -> ( ( ( ( K + 1 ) / 2 ) x. 2 ) x. _pi ) = ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) )
44 3 4 43 mp3an23 
 |-  ( ( ( K + 1 ) / 2 ) e. CC -> ( ( ( ( K + 1 ) / 2 ) x. 2 ) x. _pi ) = ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) )
45 25 44 syl 
 |-  ( K e. CC -> ( ( ( ( K + 1 ) / 2 ) x. 2 ) x. _pi ) = ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) )
46 42 45 eqtr2d 
 |-  ( K e. CC -> ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) = ( ( K x. _pi ) + _pi ) )
47 46 oveq1d 
 |-  ( K e. CC -> ( ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) - _pi ) = ( ( ( K x. _pi ) + _pi ) - _pi ) )
48 mulcl 
 |-  ( ( K e. CC /\ _pi e. CC ) -> ( K x. _pi ) e. CC )
49 4 48 mpan2 
 |-  ( K e. CC -> ( K x. _pi ) e. CC )
50 pncan 
 |-  ( ( ( K x. _pi ) e. CC /\ _pi e. CC ) -> ( ( ( K x. _pi ) + _pi ) - _pi ) = ( K x. _pi ) )
51 49 4 50 sylancl 
 |-  ( K e. CC -> ( ( ( K x. _pi ) + _pi ) - _pi ) = ( K x. _pi ) )
52 47 51 eqtrd 
 |-  ( K e. CC -> ( ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) - _pi ) = ( K x. _pi ) )
53 52 adantl 
 |-  ( ( A e. CC /\ K e. CC ) -> ( ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) - _pi ) = ( K x. _pi ) )
54 53 oveq2d 
 |-  ( ( A e. CC /\ K e. CC ) -> ( A + ( ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) - _pi ) ) = ( A + ( K x. _pi ) ) )
55 31 54 eqtr2d 
 |-  ( ( A e. CC /\ K e. CC ) -> ( A + ( K x. _pi ) ) = ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) )
56 1 55 sylan2 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( A + ( K x. _pi ) ) = ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) )
57 56 fveq2d 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( sin ` ( A + ( K x. _pi ) ) ) = ( sin ` ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) ) )
58 57 adantr 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( sin ` ( A + ( K x. _pi ) ) ) = ( sin ` ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) ) )
59 subcl 
 |-  ( ( A e. CC /\ _pi e. CC ) -> ( A - _pi ) e. CC )
60 4 59 mpan2 
 |-  ( A e. CC -> ( A - _pi ) e. CC )
61 sinper 
 |-  ( ( ( A - _pi ) e. CC /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( sin ` ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( A - _pi ) ) )
62 60 61 sylan 
 |-  ( ( A e. CC /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( sin ` ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( A - _pi ) ) )
63 62 adantlr 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( sin ` ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( A - _pi ) ) )
64 sinmpi 
 |-  ( A e. CC -> ( sin ` ( A - _pi ) ) = -u ( sin ` A ) )
65 64 ad2antrr 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( sin ` ( A - _pi ) ) = -u ( sin ` A ) )
66 63 65 eqtrd 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( sin ` ( ( A - _pi ) + ( ( ( K + 1 ) / 2 ) x. ( 2 x. _pi ) ) ) ) = -u ( sin ` A ) )
67 58 66 eqtrd 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( sin ` ( A + ( K x. _pi ) ) ) = -u ( sin ` A ) )
68 67 fveq2d 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( abs ` ( sin ` ( A + ( K x. _pi ) ) ) ) = ( abs ` -u ( sin ` A ) ) )
69 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
70 69 absnegd 
 |-  ( A e. CC -> ( abs ` -u ( sin ` A ) ) = ( abs ` ( sin ` A ) ) )
71 70 ad2antrr 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( abs ` -u ( sin ` A ) ) = ( abs ` ( sin ` A ) ) )
72 68 71 eqtrd 
 |-  ( ( ( A e. CC /\ K e. ZZ ) /\ ( ( K + 1 ) / 2 ) e. ZZ ) -> ( abs ` ( sin ` ( A + ( K x. _pi ) ) ) ) = ( abs ` ( sin ` A ) ) )
73 zeo 
 |-  ( K e. ZZ -> ( ( K / 2 ) e. ZZ \/ ( ( K + 1 ) / 2 ) e. ZZ ) )
74 73 adantl 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( ( K / 2 ) e. ZZ \/ ( ( K + 1 ) / 2 ) e. ZZ ) )
75 22 72 74 mpjaodan 
 |-  ( ( A e. CC /\ K e. ZZ ) -> ( abs ` ( sin ` ( A + ( K x. _pi ) ) ) ) = ( abs ` ( sin ` A ) ) )