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 \in ℂ \to (\sin A = 0 \leftrightarrow \frac{A}{π} \in ℤ)$

Proof

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

Metamath Proof Explorer

Theorem sineq0

Proof