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 mullidi ⊢ ( 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 ‘ 𝐴 ) ) )