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

Proof

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

Metamath Proof Explorer

Theorem sineq0ALT

Proof