Theorem 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	⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( sin ‘ ( 𝐴 / 2 ) ) ≠ 0 )

Proof

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