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 AsinA=0Aπ

Proof

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