Metamath Proof Explorer


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 )