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
|- ( A e. CC -> ( ( sin ` A ) = 0 <-> ( A / _pi ) e. ZZ ) )

Proof

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