sinaover2ne0

Description: If A in ( 0 , 2 _pi ) then sin ( A / 2 ) is not 0 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	sinaover2ne0	$⊢ A \in (0, 2 π) \to \sin (\frac{A}{2}) \neq 0$

Proof

Step	Hyp	Ref	Expression
1		elioore	$⊢ A \in (0, 2 π) \to A \in ℝ$
2	1	recnd	$⊢ A \in (0, 2 π) \to A \in ℂ$
3		2cnd	$⊢ A \in (0, 2 π) \to 2 \in ℂ$
4		picn	$⊢ π \in ℂ$
5	4	a1i	$⊢ A \in (0, 2 π) \to π \in ℂ$
6		2ne0	$⊢ 2 \neq 0$
7	6	a1i	$⊢ A \in (0, 2 π) \to 2 \neq 0$
8		pire	$⊢ π \in ℝ$
9		pipos	$⊢ 0 < π$
10	8 9	gt0ne0ii	$⊢ π \neq 0$
11	10	a1i	$⊢ A \in (0, 2 π) \to π \neq 0$
12	2 3 5 7 11	divdiv1d	$⊢ A \in (0, 2 π) \to \frac{\frac{A}{2}}{π} = \frac{A}{2 π}$
13		0zd	$⊢ A \in (0, 2 π) \to 0 \in ℤ$
14		2re	$⊢ 2 \in ℝ$
15	14 8	remulcli	$⊢ 2 π \in ℝ$
16	15	a1i	$⊢ A \in (0, 2 π) \to 2 π \in ℝ$
17		0xr	$⊢ 0 \in ℝ^{*}$
18	17	a1i	$⊢ A \in (0, 2 π) \to 0 \in ℝ^{*}$
19	16	rexrd	$⊢ A \in (0, 2 π) \to 2 π \in ℝ^{*}$
20		id	$⊢ A \in (0, 2 π) \to A \in (0, 2 π)$
21		ioogtlb	$⊢ (0 \in ℝ^{} \land 2 π \in ℝ^{} \land A \in (0, 2 π)) \to 0 < A$
22	18 19 20 21	syl3anc	$⊢ A \in (0, 2 π) \to 0 < A$
23		2pos	$⊢ 0 < 2$
24	14 8 23 9	mulgt0ii	$⊢ 0 < 2 π$
25	24	a1i	$⊢ A \in (0, 2 π) \to 0 < 2 π$
26	1 16 22 25	divgt0d	$⊢ A \in (0, 2 π) \to 0 < \frac{A}{2 π}$
27		1rp	$⊢ 1 \in ℝ^{+}$
28	27	a1i	$⊢ A \in (0, 2 π) \to 1 \in ℝ^{+}$
29	16 25	elrpd	$⊢ A \in (0, 2 π) \to 2 π \in ℝ^{+}$
30	2	div1d	$⊢ A \in (0, 2 π) \to \frac{A}{1} = A$
31		iooltub	$⊢ (0 \in ℝ^{} \land 2 π \in ℝ^{} \land A \in (0, 2 π)) \to A < 2 π$
32	18 19 20 31	syl3anc	$⊢ A \in (0, 2 π) \to A < 2 π$
33	30 32	eqbrtrd	$⊢ A \in (0, 2 π) \to \frac{A}{1} < 2 π$
34	1 28 29 33	ltdiv23d	$⊢ A \in (0, 2 π) \to \frac{A}{2 π} < 1$
35		1e0p1	$⊢ 1 = 0 + 1$
36	34 35	breqtrdi	$⊢ A \in (0, 2 π) \to \frac{A}{2 π} < 0 + 1$
37		btwnnz	$⊢ (0 \in ℤ \land 0 < \frac{A}{2 π} \land \frac{A}{2 π} < 0 + 1) \to \neg \frac{A}{2 π} \in ℤ$
38	13 26 36 37	syl3anc	$⊢ A \in (0, 2 π) \to \neg \frac{A}{2 π} \in ℤ$
39	12 38	eqneltrd	$⊢ A \in (0, 2 π) \to \neg \frac{\frac{A}{2}}{π} \in ℤ$
40	2	halfcld	$⊢ A \in (0, 2 π) \to \frac{A}{2} \in ℂ$
41		sineq0	$⊢ \frac{A}{2} \in ℂ \to (\sin (\frac{A}{2}) = 0 \leftrightarrow \frac{\frac{A}{2}}{π} \in ℤ)$
42	40 41	syl	$⊢ A \in (0, 2 π) \to (\sin (\frac{A}{2}) = 0 \leftrightarrow \frac{\frac{A}{2}}{π} \in ℤ)$
43	39 42	mtbird	$⊢ A \in (0, 2 π) \to \neg \sin (\frac{A}{2}) = 0$
44	43	neqned	$⊢ A \in (0, 2 π) \to \sin (\frac{A}{2}) \neq 0$

Metamath Proof Explorer

Theorem sinaover2ne0

Proof