Metamath Proof Explorer


Theorem sineq0

Description: A complex number whose sine is zero is an integer multiple of _pi . (Contributed by NM, 17-Aug-2008) (Revised by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion sineq0 ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 sinval ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
2 1 eqeq1d ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ) )
3 ax-icn i ∈ ℂ
4 mulcl ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
5 3 4 mpan ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
6 efcl ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
7 5 6 syl ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
8 negicn - i ∈ ℂ
9 mulcl ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
10 8 9 mpan ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
11 efcl ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
12 10 11 syl ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
13 7 12 subcld ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
14 2mulicn ( 2 · i ) ∈ ℂ
15 2muline0 ( 2 · i ) ≠ 0
16 diveq0 ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ∧ ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
17 14 15 16 mp3an23 ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
18 13 17 syl ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
19 7 12 subeq0ad ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ↔ ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) ) )
20 2 18 19 3bitrd ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) ) )
21 oveq2 ( ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
22 2cn 2 ∈ ℂ
23 mul12 ( ( i ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · ( 2 · 𝐴 ) ) = ( 2 · ( i · 𝐴 ) ) )
24 3 22 23 mp3an12 ( 𝐴 ∈ ℂ → ( i · ( 2 · 𝐴 ) ) = ( 2 · ( i · 𝐴 ) ) )
25 5 2timesd ( 𝐴 ∈ ℂ → ( 2 · ( i · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
26 24 25 eqtrd ( 𝐴 ∈ ℂ → ( i · ( 2 · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
27 26 fveq2d ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) )
28 efadd ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
29 5 5 28 syl2anc ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
30 27 29 eqtr2d ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) )
31 efadd ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( - i · 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
32 5 10 31 syl2anc ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
33 3 negidi ( i + - i ) = 0
34 33 oveq1i ( ( i + - i ) · 𝐴 ) = ( 0 · 𝐴 )
35 adddir ( ( i ∈ ℂ ∧ - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( i + - i ) · 𝐴 ) = ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) )
36 3 8 35 mp3an12 ( 𝐴 ∈ ℂ → ( ( i + - i ) · 𝐴 ) = ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) )
37 mul02 ( 𝐴 ∈ ℂ → ( 0 · 𝐴 ) = 0 )
38 34 36 37 3eqtr3a ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) = 0 )
39 38 fveq2d ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( exp ‘ 0 ) )
40 ef0 ( exp ‘ 0 ) = 1
41 39 40 eqtrdi ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = 1 )
42 32 41 eqtr3d ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) = 1 )
43 30 42 eqeq12d ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) ↔ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = 1 ) )
44 fveq2 ( ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = 1 → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) )
45 43 44 syl6bi ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ) )
46 21 45 syl5 ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ) )
47 20 46 sylbid ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ) )
48 abs1 ( abs ‘ 1 ) = 1
49 48 eqeq2i ( ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ↔ ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 )
50 2re 2 ∈ ℝ
51 2ne0 2 ≠ 0
52 mulre ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℝ ∧ 2 ≠ 0 ) → ( 𝐴 ∈ ℝ ↔ ( 2 · 𝐴 ) ∈ ℝ ) )
53 50 51 52 mp3an23 ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( 2 · 𝐴 ) ∈ ℝ ) )
54 mulcl ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · 𝐴 ) ∈ ℂ )
55 22 54 mpan ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) ∈ ℂ )
56 absefib ( ( 2 · 𝐴 ) ∈ ℂ → ( ( 2 · 𝐴 ) ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ) )
57 55 56 syl ( 𝐴 ∈ ℂ → ( ( 2 · 𝐴 ) ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ) )
58 53 57 bitr2d ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ↔ 𝐴 ∈ ℝ ) )
59 49 58 syl5bb ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ↔ 𝐴 ∈ ℝ ) )
60 47 59 sylibd ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 → 𝐴 ∈ ℝ ) )
61 60 imp ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℝ )
62 pirp π ∈ ℝ+
63 modval ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( 𝐴 mod π ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
64 61 62 63 sylancl ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
65 picn π ∈ ℂ
66 pire π ∈ ℝ
67 pipos 0 < π
68 66 67 gt0ne0ii π ≠ 0
69 redivcl ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ∧ π ≠ 0 ) → ( 𝐴 / π ) ∈ ℝ )
70 66 68 69 mp3an23 ( 𝐴 ∈ ℝ → ( 𝐴 / π ) ∈ ℝ )
71 61 70 syl ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 / π ) ∈ ℝ )
72 71 flcld ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ )
73 72 zcnd ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ )
74 mulcl ( ( π ∈ ℂ ∧ ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ )
75 65 73 74 sylancr ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ )
76 negsub ( ( 𝐴 ∈ ℂ ∧ ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ ) → ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
77 75 76 syldan ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
78 mulcom ( ( π ∈ ℂ ∧ ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) = ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
79 65 73 78 sylancr ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) = ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
80 79 negeqd ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) = - ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
81 mulneg1 ( ( ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ ∧ π ∈ ℂ ) → ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
82 73 65 81 sylancl ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
83 80 82 eqtr4d ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) = ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
84 83 oveq2d ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) = ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) )
85 64 77 84 3eqtr2d ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) = ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) )
86 85 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( sin ‘ ( 𝐴 mod π ) ) = ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) )
87 86 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) )
88 72 znegcld ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ )
89 abssinper ( ( 𝐴 ∈ ℂ ∧ - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ ) → ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) = ( abs ‘ ( sin ‘ 𝐴 ) ) )
90 88 89 syldan ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) = ( abs ‘ ( sin ‘ 𝐴 ) ) )
91 simpr ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( sin ‘ 𝐴 ) = 0 )
92 91 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ 0 ) )
93 87 90 92 3eqtrd ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( abs ‘ 0 ) )
94 abs0 ( abs ‘ 0 ) = 0
95 93 94 eqtrdi ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = 0 )
96 modcl ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( 𝐴 mod π ) ∈ ℝ )
97 61 62 96 sylancl ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) ∈ ℝ )
98 modlt ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( 𝐴 mod π ) < π )
99 61 62 98 sylancl ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) < π )
100 97 99 jca ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) )
101 100 biantrurd ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) ↔ ( ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ∧ 0 < ( 𝐴 mod π ) ) ) )
102 0re 0 ∈ ℝ
103 rexr ( 0 ∈ ℝ → 0 ∈ ℝ* )
104 rexr ( π ∈ ℝ → π ∈ ℝ* )
105 elioo2 ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ) )
106 103 104 105 syl2an ( ( 0 ∈ ℝ ∧ π ∈ ℝ ) → ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ) )
107 102 66 106 mp2an ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) )
108 3anan32 ( ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ↔ ( ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ∧ 0 < ( 𝐴 mod π ) ) )
109 107 108 bitri ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ∧ 0 < ( 𝐴 mod π ) ) )
110 101 109 bitr4di ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) ↔ ( 𝐴 mod π ) ∈ ( 0 (,) π ) ) )
111 sinq12gt0 ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → 0 < ( sin ‘ ( 𝐴 mod π ) ) )
112 elioore ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → ( 𝐴 mod π ) ∈ ℝ )
113 112 resincld ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → ( sin ‘ ( 𝐴 mod π ) ) ∈ ℝ )
114 ltle ( ( 0 ∈ ℝ ∧ ( sin ‘ ( 𝐴 mod π ) ) ∈ ℝ ) → ( 0 < ( sin ‘ ( 𝐴 mod π ) ) → 0 ≤ ( sin ‘ ( 𝐴 mod π ) ) ) )
115 102 113 114 sylancr ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → ( 0 < ( sin ‘ ( 𝐴 mod π ) ) → 0 ≤ ( sin ‘ ( 𝐴 mod π ) ) ) )
116 111 115 mpd ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → 0 ≤ ( sin ‘ ( 𝐴 mod π ) ) )
117 113 116 absidd ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( sin ‘ ( 𝐴 mod π ) ) )
118 111 117 breqtrrd ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → 0 < ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) )
119 110 118 syl6bi ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) → 0 < ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ) )
120 ltne ( ( 0 ∈ ℝ ∧ 0 < ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ≠ 0 )
121 102 120 mpan ( 0 < ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ≠ 0 )
122 119 121 syl6 ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ≠ 0 ) )
123 122 necon2bd ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = 0 → ¬ 0 < ( 𝐴 mod π ) ) )
124 95 123 mpd ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ¬ 0 < ( 𝐴 mod π ) )
125 modge0 ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod π ) )
126 61 62 125 sylancl ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 0 ≤ ( 𝐴 mod π ) )
127 leloe ( ( 0 ∈ ℝ ∧ ( 𝐴 mod π ) ∈ ℝ ) → ( 0 ≤ ( 𝐴 mod π ) ↔ ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) ) )
128 102 97 127 sylancr ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 ≤ ( 𝐴 mod π ) ↔ ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) ) )
129 126 128 mpbid ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) )
130 129 ord ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ¬ 0 < ( 𝐴 mod π ) → 0 = ( 𝐴 mod π ) ) )
131 124 130 mpd ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 0 = ( 𝐴 mod π ) )
132 131 eqcomd ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) = 0 )
133 mod0 ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( ( 𝐴 mod π ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )
134 61 62 133 sylancl ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( 𝐴 mod π ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )
135 132 134 mpbid ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 / π ) ∈ ℤ )
136 divcan1 ( ( 𝐴 ∈ ℂ ∧ π ∈ ℂ ∧ π ≠ 0 ) → ( ( 𝐴 / π ) · π ) = 𝐴 )
137 65 68 136 mp3an23 ( 𝐴 ∈ ℂ → ( ( 𝐴 / π ) · π ) = 𝐴 )
138 137 fveq2d ( 𝐴 ∈ ℂ → ( sin ‘ ( ( 𝐴 / π ) · π ) ) = ( sin ‘ 𝐴 ) )
139 sinkpi ( ( 𝐴 / π ) ∈ ℤ → ( sin ‘ ( ( 𝐴 / π ) · π ) ) = 0 )
140 138 139 sylan9req ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 / π ) ∈ ℤ ) → ( sin ‘ 𝐴 ) = 0 )
141 135 140 impbida ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )