This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )