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 ) )