This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( 𝐴 ∈ ℂ → ( ( ( 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 bitrid ⊢ ( 𝐴 ∈ ℂ → ( ( 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 biimtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 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 ↔ ( 𝐴 / π ) ∈ ℤ ) )