Metamath Proof Explorer

Theorem sineq0ALT

Description: A complex number whose sine is zero is an integer multiple of _pi . The Virtual Deduction form of the proof is https://us.metamath.org/other/completeusersproof/sineq0altvd.html . The Metamath form of the proof is sineq0ALT . The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 . The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/sineq0altro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sineq0ALT 
|- ( A e. CC -> ( ( sin ` A ) = 0 <-> ( A / _pi ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 pipos 
 |-  0 < _pi
3 1 2 elrpii 
 |-  _pi e. RR+
4 2ne0 
 |-  2 =/= 0
5 4 a1i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> 2 =/= 0 )
6 2cn 
 |-  2 e. CC
7 2re 
 |-  2 e. RR
8 7 a1i 
 |-  ( 2 e. CC -> 2 e. RR )
9 6 8 ax-mp 
 |-  2 e. RR
10 9 a1i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> 2 e. RR )
11 id 
 |-  ( A e. CC -> A e. CC )
12 11 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> A e. CC )
13 6 a1i 
 |-  ( A e. CC -> 2 e. CC )
14 13 11 mulcld 
 |-  ( A e. CC -> ( 2 x. A ) e. CC )
15 ax-icn 
 |-  _i e. CC
16 15 a1i 
 |-  ( A e. CC -> _i e. CC )
17 13 16 11 mul12d 
 |-  ( A e. CC -> ( 2 x. ( _i x. A ) ) = ( _i x. ( 2 x. A ) ) )
18 16 11 mulcld 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
19 18 2timesd 
 |-  ( A e. CC -> ( 2 x. ( _i x. A ) ) = ( ( _i x. A ) + ( _i x. A ) ) )
20 17 19 eqtr3d 
 |-  ( A e. CC -> ( _i x. ( 2 x. A ) ) = ( ( _i x. A ) + ( _i x. A ) ) )
21 20 fveq2d 
 |-  ( A e. CC -> ( exp ` ( _i x. ( 2 x. A ) ) ) = ( exp ` ( ( _i x. A ) + ( _i x. A ) ) ) )
22 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 ) ) ) )
23 18 18 22 syl2anc 
 |-  ( A e. CC -> ( exp ` ( ( _i x. A ) + ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) )
24 21 23 eqtrd 
 |-  ( A e. CC -> ( exp ` ( _i x. ( 2 x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) )
25 24 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( exp ` ( _i x. ( 2 x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) )
26 sinval 
 |-  ( A e. CC -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
27 id 
 |-  ( ( sin ` A ) = 0 -> ( sin ` A ) = 0 )
28 26 27 sylan9req 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) = 0 )
29 efcl 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
30 18 29 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) e. CC )
31 negicn 
 |-  -u _i e. CC
32 31 a1i 
 |-  ( A e. CC -> -u _i e. CC )
33 32 11 mulcld 
 |-  ( A e. CC -> ( -u _i x. A ) e. CC )
34 efcl 
 |-  ( ( -u _i x. A ) e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
35 33 34 syl 
 |-  ( A e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
36 30 35 subcld 
 |-  ( A e. CC -> ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) e. CC )
37 2mulicn 
 |-  ( 2 x. _i ) e. CC
38 37 a1i 
 |-  ( A e. CC -> ( 2 x. _i ) e. CC )
39 2muline0 
 |-  ( 2 x. _i ) =/= 0
40 39 a1i 
 |-  ( A e. CC -> ( 2 x. _i ) =/= 0 )
41 36 38 40 diveq0ad 
 |-  ( 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 ) )
42 41 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) = 0 <-> ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) = 0 ) )
43 28 42 mpbid 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) = 0 )
44 30 35 subeq0ad 
 |-  ( A e. CC -> ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) = 0 <-> ( exp ` ( _i x. A ) ) = ( exp ` ( -u _i x. A ) ) ) )
45 44 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) = 0 <-> ( exp ` ( _i x. A ) ) = ( exp ` ( -u _i x. A ) ) ) )
46 43 45 mpbid 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( exp ` ( _i x. A ) ) = ( exp ` ( -u _i x. A ) ) )
47 46 oveq2d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) )
48 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 ) ) ) )
49 18 33 48 syl2anc 
 |-  ( A e. CC -> ( exp ` ( ( _i x. A ) + ( -u _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) )
50 49 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( exp ` ( ( _i x. A ) + ( -u _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) )
51 47 50 eqtr4d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) = ( exp ` ( ( _i x. A ) + ( -u _i x. A ) ) ) )
52 15 negidi 
 |-  ( _i + -u _i ) = 0
53 52 oveq1i 
 |-  ( ( _i + -u _i ) x. A ) = ( 0 x. A )
54 16 32 11 adddird 
 |-  ( A e. CC -> ( ( _i + -u _i ) x. A ) = ( ( _i x. A ) + ( -u _i x. A ) ) )
55 53 54 syl5reqr 
 |-  ( A e. CC -> ( ( _i x. A ) + ( -u _i x. A ) ) = ( 0 x. A ) )
56 11 mul02d 
 |-  ( A e. CC -> ( 0 x. A ) = 0 )
57 55 56 eqtrd 
 |-  ( A e. CC -> ( ( _i x. A ) + ( -u _i x. A ) ) = 0 )
58 57 fveq2d 
 |-  ( A e. CC -> ( exp ` ( ( _i x. A ) + ( -u _i x. A ) ) ) = ( exp ` 0 ) )
59 58 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( exp ` ( ( _i x. A ) + ( -u _i x. A ) ) ) = ( exp ` 0 ) )
60 ef0 
 |-  ( exp ` 0 ) = 1
61 60 a1i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( exp ` 0 ) = 1 )
62 51 59 61 3eqtrd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) = 1 )
63 25 62 eqtrd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( exp ` ( _i x. ( 2 x. A ) ) ) = 1 )
64 63 fveq2d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( exp ` ( _i x. ( 2 x. A ) ) ) ) = ( abs ` 1 ) )
65 abs1 
 |-  ( abs ` 1 ) = 1
66 64 65 eqtrdi 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( exp ` ( _i x. ( 2 x. A ) ) ) ) = 1 )
67 absefib 
 |-  ( ( 2 x. A ) e. CC -> ( ( 2 x. A ) e. RR <-> ( abs ` ( exp ` ( _i x. ( 2 x. A ) ) ) ) = 1 ) )
68 67 biimparc 
 |-  ( ( ( abs ` ( exp ` ( _i x. ( 2 x. A ) ) ) ) = 1 /\ ( 2 x. A ) e. CC ) -> ( 2 x. A ) e. RR )
69 68 ancoms 
 |-  ( ( ( 2 x. A ) e. CC /\ ( abs ` ( exp ` ( _i x. ( 2 x. A ) ) ) ) = 1 ) -> ( 2 x. A ) e. RR )
70 14 66 69 syl2an2r 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( 2 x. A ) e. RR )
71 mulre 
 |-  ( ( A e. CC /\ 2 e. RR /\ 2 =/= 0 ) -> ( A e. RR <-> ( 2 x. A ) e. RR ) )
72 71 4animp1 
 |-  ( ( ( ( A e. CC /\ 2 e. RR ) /\ 2 =/= 0 ) /\ ( 2 x. A ) e. RR ) -> A e. RR )
73 72 4an31 
 |-  ( ( ( ( 2 =/= 0 /\ 2 e. RR ) /\ A e. CC ) /\ ( 2 x. A ) e. RR ) -> A e. RR )
74 5 10 12 70 73 syl1111anc 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> A e. RR )
75 3 a1i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> _pi e. RR+ )
76 74 75 modcld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A mod _pi ) e. RR )
77 76 recnd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A mod _pi ) e. CC )
78 77 sincld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( sin ` ( A mod _pi ) ) e. CC )
79 1 a1i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> _pi e. RR )
80 0re 
 |-  0 e. RR
81 80 1 2 ltleii 
 |-  0 <_ _pi
82 gt0ne0 
 |-  ( ( _pi e. RR /\ 0 < _pi ) -> _pi =/= 0 )
83 82 3adant3 
 |-  ( ( _pi e. RR /\ 0 < _pi /\ 0 <_ _pi ) -> _pi =/= 0 )
84 83 3com23 
 |-  ( ( _pi e. RR /\ 0 <_ _pi /\ 0 < _pi ) -> _pi =/= 0 )
85 1 81 2 84 mp3an 
 |-  _pi =/= 0
86 85 a1i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> _pi =/= 0 )
87 74 79 86 redivcld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A / _pi ) e. RR )
88 87 flcld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( |_ ` ( A / _pi ) ) e. ZZ )
89 88 znegcld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -u ( |_ ` ( A / _pi ) ) e. ZZ )
90 abssinper 
 |-  ( ( A e. CC /\ -u ( |_ ` ( A / _pi ) ) e. ZZ ) -> ( abs ` ( sin ` ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) ) ) = ( abs ` ( sin ` A ) ) )
91 90 eqcomd 
 |-  ( ( A e. CC /\ -u ( |_ ` ( A / _pi ) ) e. ZZ ) -> ( abs ` ( sin ` A ) ) = ( abs ` ( sin ` ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) ) ) )
92 91 ex 
 |-  ( A e. CC -> ( -u ( |_ ` ( A / _pi ) ) e. ZZ -> ( abs ` ( sin ` A ) ) = ( abs ` ( sin ` ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) ) ) ) )
93 92 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( -u ( |_ ` ( A / _pi ) ) e. ZZ -> ( abs ` ( sin ` A ) ) = ( abs ` ( sin ` ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) ) ) ) )
94 89 93 mpd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( sin ` A ) ) = ( abs ` ( sin ` ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) ) ) )
95 88 zcnd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( |_ ` ( A / _pi ) ) e. CC )
96 95 negcld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -u ( |_ ` ( A / _pi ) ) e. CC )
97 1 recni 
 |-  _pi e. CC
98 97 a1i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> _pi e. CC )
99 96 98 mulcld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( -u ( |_ ` ( A / _pi ) ) x. _pi ) e. CC )
100 98 95 mulcld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( _pi x. ( |_ ` ( A / _pi ) ) ) e. CC )
101 100 negcld 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -u ( _pi x. ( |_ ` ( A / _pi ) ) ) e. CC )
102 95 98 mulneg1d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( -u ( |_ ` ( A / _pi ) ) x. _pi ) = -u ( ( |_ ` ( A / _pi ) ) x. _pi ) )
103 95 98 mulcomd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( |_ ` ( A / _pi ) ) x. _pi ) = ( _pi x. ( |_ ` ( A / _pi ) ) ) )
104 103 negeqd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -u ( ( |_ ` ( A / _pi ) ) x. _pi ) = -u ( _pi x. ( |_ ` ( A / _pi ) ) ) )
105 102 104 eqtrd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( -u ( |_ ` ( A / _pi ) ) x. _pi ) = -u ( _pi x. ( |_ ` ( A / _pi ) ) ) )
106 oveq2 
 |-  ( ( -u ( |_ ` ( A / _pi ) ) x. _pi ) = -u ( _pi x. ( |_ ` ( A / _pi ) ) ) -> ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) = ( A + -u ( _pi x. ( |_ ` ( A / _pi ) ) ) ) )
107 106 ad3antrrr 
 |-  ( ( ( ( ( -u ( |_ ` ( A / _pi ) ) x. _pi ) = -u ( _pi x. ( |_ ` ( A / _pi ) ) ) /\ -u ( _pi x. ( |_ ` ( A / _pi ) ) ) e. CC ) /\ ( -u ( |_ ` ( A / _pi ) ) x. _pi ) e. CC ) /\ A e. CC ) -> ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) = ( A + -u ( _pi x. ( |_ ` ( A / _pi ) ) ) ) )
108 107 4an4132 
 |-  ( ( ( ( A e. CC /\ ( -u ( |_ ` ( A / _pi ) ) x. _pi ) e. CC ) /\ -u ( _pi x. ( |_ ` ( A / _pi ) ) ) e. CC ) /\ ( -u ( |_ ` ( A / _pi ) ) x. _pi ) = -u ( _pi x. ( |_ ` ( A / _pi ) ) ) ) -> ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) = ( A + -u ( _pi x. ( |_ ` ( A / _pi ) ) ) ) )
109 12 99 101 105 108 syl1111anc 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) = ( A + -u ( _pi x. ( |_ ` ( A / _pi ) ) ) ) )
110 12 100 negsubd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A + -u ( _pi x. ( |_ ` ( A / _pi ) ) ) ) = ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) )
111 109 110 eqtrd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) = ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) )
112 111 fveq2d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( sin ` ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) ) = ( sin ` ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) ) )
113 112 fveq2d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( sin ` ( A + ( -u ( |_ ` ( A / _pi ) ) x. _pi ) ) ) ) = ( abs ` ( sin ` ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) ) ) )
114 94 113 eqtrd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( sin ` A ) ) = ( abs ` ( sin ` ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) ) ) )
115 modval 
 |-  ( ( A e. RR /\ _pi e. RR+ ) -> ( A mod _pi ) = ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) )
116 115 fveq2d 
 |-  ( ( A e. RR /\ _pi e. RR+ ) -> ( sin ` ( A mod _pi ) ) = ( sin ` ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) ) )
117 116 fveq2d 
 |-  ( ( A e. RR /\ _pi e. RR+ ) -> ( abs ` ( sin ` ( A mod _pi ) ) ) = ( abs ` ( sin ` ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) ) ) )
118 3 117 mpan2 
 |-  ( A e. RR -> ( abs ` ( sin ` ( A mod _pi ) ) ) = ( abs ` ( sin ` ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) ) ) )
119 74 118 syl 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( sin ` ( A mod _pi ) ) ) = ( abs ` ( sin ` ( A - ( _pi x. ( |_ ` ( A / _pi ) ) ) ) ) ) )
120 114 119 eqtr4d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( sin ` A ) ) = ( abs ` ( sin ` ( A mod _pi ) ) ) )
121 27 fveq2d 
 |-  ( ( sin ` A ) = 0 -> ( abs ` ( sin ` A ) ) = ( abs ` 0 ) )
122 abs0 
 |-  ( abs ` 0 ) = 0
123 121 122 eqtrdi 
 |-  ( ( sin ` A ) = 0 -> ( abs ` ( sin ` A ) ) = 0 )
124 123 adantl 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( sin ` A ) ) = 0 )
125 120 124 eqtr3d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( abs ` ( sin ` ( A mod _pi ) ) ) = 0 )
126 78 125 abs00d 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( sin ` ( A mod _pi ) ) = 0 )
127 notnotb 
 |-  ( ( sin ` ( A mod _pi ) ) = 0 <-> -. -. ( sin ` ( A mod _pi ) ) = 0 )
128 127 bicomi 
 |-  ( -. -. ( sin ` ( A mod _pi ) ) = 0 <-> ( sin ` ( A mod _pi ) ) = 0 )
129 ltne 
 |-  ( ( 0 e. RR /\ 0 < ( sin ` ( A mod _pi ) ) ) -> ( sin ` ( A mod _pi ) ) =/= 0 )
130 129 neneqd 
 |-  ( ( 0 e. RR /\ 0 < ( sin ` ( A mod _pi ) ) ) -> -. ( sin ` ( A mod _pi ) ) = 0 )
131 130 expcom 
 |-  ( 0 < ( sin ` ( A mod _pi ) ) -> ( 0 e. RR -> -. ( sin ` ( A mod _pi ) ) = 0 ) )
132 80 131 mpi 
 |-  ( 0 < ( sin ` ( A mod _pi ) ) -> -. ( sin ` ( A mod _pi ) ) = 0 )
133 132 con3i 
 |-  ( -. -. ( sin ` ( A mod _pi ) ) = 0 -> -. 0 < ( sin ` ( A mod _pi ) ) )
134 128 133 sylbir 
 |-  ( ( sin ` ( A mod _pi ) ) = 0 -> -. 0 < ( sin ` ( A mod _pi ) ) )
135 126 134 syl 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -. 0 < ( sin ` ( A mod _pi ) ) )
136 sinq12gt0 
 |-  ( ( A mod _pi ) e. ( 0 (,) _pi ) -> 0 < ( sin ` ( A mod _pi ) ) )
137 135 136 nsyl 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -. ( A mod _pi ) e. ( 0 (,) _pi ) )
138 80 rexri 
 |-  0 e. RR*
139 1 rexri 
 |-  _pi e. RR*
140 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 ) ) )
141 138 139 140 mp2an 
 |-  ( ( A mod _pi ) e. ( 0 (,) _pi ) <-> ( ( A mod _pi ) e. RR /\ 0 < ( A mod _pi ) /\ ( A mod _pi ) < _pi ) )
142 141 notbii 
 |-  ( -. ( A mod _pi ) e. ( 0 (,) _pi ) <-> -. ( ( A mod _pi ) e. RR /\ 0 < ( A mod _pi ) /\ ( A mod _pi ) < _pi ) )
143 137 142 sylib 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -. ( ( A mod _pi ) e. RR /\ 0 < ( A mod _pi ) /\ ( A mod _pi ) < _pi ) )
144 3anan12 
 |-  ( ( ( A mod _pi ) e. RR /\ 0 < ( A mod _pi ) /\ ( A mod _pi ) < _pi ) <-> ( 0 < ( A mod _pi ) /\ ( ( A mod _pi ) e. RR /\ ( A mod _pi ) < _pi ) ) )
145 144 notbii 
 |-  ( -. ( ( A mod _pi ) e. RR /\ 0 < ( A mod _pi ) /\ ( A mod _pi ) < _pi ) <-> -. ( 0 < ( A mod _pi ) /\ ( ( A mod _pi ) e. RR /\ ( A mod _pi ) < _pi ) ) )
146 143 145 sylib 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -. ( 0 < ( A mod _pi ) /\ ( ( A mod _pi ) e. RR /\ ( A mod _pi ) < _pi ) ) )
147 modlt 
 |-  ( ( A e. RR /\ _pi e. RR+ ) -> ( A mod _pi ) < _pi )
148 147 ancoms 
 |-  ( ( _pi e. RR+ /\ A e. RR ) -> ( A mod _pi ) < _pi )
149 3 74 148 sylancr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A mod _pi ) < _pi )
150 76 149 jca 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( ( A mod _pi ) e. RR /\ ( A mod _pi ) < _pi ) )
151 not12an2impnot1 
 |-  ( ( -. ( 0 < ( A mod _pi ) /\ ( ( A mod _pi ) e. RR /\ ( A mod _pi ) < _pi ) ) /\ ( ( A mod _pi ) e. RR /\ ( A mod _pi ) < _pi ) ) -> -. 0 < ( A mod _pi ) )
152 146 150 151 syl2anc 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> -. 0 < ( A mod _pi ) )
153 modge0 
 |-  ( ( A e. RR /\ _pi e. RR+ ) -> 0 <_ ( A mod _pi ) )
154 153 ancoms 
 |-  ( ( _pi e. RR+ /\ A e. RR ) -> 0 <_ ( A mod _pi ) )
155 3 74 154 sylancr 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> 0 <_ ( A mod _pi ) )
156 leloe 
 |-  ( ( 0 e. RR /\ ( A mod _pi ) e. RR ) -> ( 0 <_ ( A mod _pi ) <-> ( 0 < ( A mod _pi ) \/ 0 = ( A mod _pi ) ) ) )
157 156 biimp3a 
 |-  ( ( 0 e. RR /\ ( A mod _pi ) e. RR /\ 0 <_ ( A mod _pi ) ) -> ( 0 < ( A mod _pi ) \/ 0 = ( A mod _pi ) ) )
158 157 idiALT 
 |-  ( ( 0 e. RR /\ ( A mod _pi ) e. RR /\ 0 <_ ( A mod _pi ) ) -> ( 0 < ( A mod _pi ) \/ 0 = ( A mod _pi ) ) )
159 80 76 155 158 mp3an2i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( 0 < ( A mod _pi ) \/ 0 = ( A mod _pi ) ) )
160 pm2.53 
 |-  ( ( 0 < ( A mod _pi ) \/ 0 = ( A mod _pi ) ) -> ( -. 0 < ( A mod _pi ) -> 0 = ( A mod _pi ) ) )
161 160 imp 
 |-  ( ( ( 0 < ( A mod _pi ) \/ 0 = ( A mod _pi ) ) /\ -. 0 < ( A mod _pi ) ) -> 0 = ( A mod _pi ) )
162 161 ancoms 
 |-  ( ( -. 0 < ( A mod _pi ) /\ ( 0 < ( A mod _pi ) \/ 0 = ( A mod _pi ) ) ) -> 0 = ( A mod _pi ) )
163 152 159 162 syl2anc 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> 0 = ( A mod _pi ) )
164 163 eqcomd 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A mod _pi ) = 0 )
165 mod0 
 |-  ( ( A e. RR /\ _pi e. RR+ ) -> ( ( A mod _pi ) = 0 <-> ( A / _pi ) e. ZZ ) )
166 165 biimp3a 
 |-  ( ( A e. RR /\ _pi e. RR+ /\ ( A mod _pi ) = 0 ) -> ( A / _pi ) e. ZZ )
167 166 3com12 
 |-  ( ( _pi e. RR+ /\ A e. RR /\ ( A mod _pi ) = 0 ) -> ( A / _pi ) e. ZZ )
168 3 74 164 167 mp3an2i 
 |-  ( ( A e. CC /\ ( sin ` A ) = 0 ) -> ( A / _pi ) e. ZZ )
169 168 ex 
 |-  ( A e. CC -> ( ( sin ` A ) = 0 -> ( A / _pi ) e. ZZ ) )
170 97 a1i 
 |-  ( A e. CC -> _pi e. CC )
171 85 a1i 
 |-  ( A e. CC -> _pi =/= 0 )
172 11 170 171 divcan1d 
 |-  ( A e. CC -> ( ( A / _pi ) x. _pi ) = A )
173 172 fveq2d 
 |-  ( A e. CC -> ( sin ` ( ( A / _pi ) x. _pi ) ) = ( sin ` A ) )
174 id 
 |-  ( ( A / _pi ) e. ZZ -> ( A / _pi ) e. ZZ )
175 sinkpi 
 |-  ( ( A / _pi ) e. ZZ -> ( sin ` ( ( A / _pi ) x. _pi ) ) = 0 )
176 174 175 syl 
 |-  ( ( A / _pi ) e. ZZ -> ( sin ` ( ( A / _pi ) x. _pi ) ) = 0 )
177 173 176 sylan9req 
 |-  ( ( A e. CC /\ ( A / _pi ) e. ZZ ) -> ( sin ` A ) = 0 )
178 177 ex 
 |-  ( A e. CC -> ( ( A / _pi ) e. ZZ -> ( sin ` A ) = 0 ) )
179 169 178 impbid 
 |-  ( A e. CC -> ( ( sin ` A ) = 0 <-> ( A / _pi ) e. ZZ ) )