Metamath Proof Explorer


Theorem abssinper

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

Ref Expression
Assertion abssinper ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( sin ‘ ( 𝐴 + ( 𝐾 · π ) ) ) ) = ( abs ‘ ( sin ‘ 𝐴 ) ) )

Proof

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