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

Proof

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