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
|- ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( sin ` ( A / 2 ) ) =/= 0 )

Proof

Step Hyp Ref Expression
1 elioore
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> A e. RR )
2 1 recnd
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> A e. CC )
3 2cnd
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 2 e. CC )
4 picn
 |-  _pi e. CC
5 4 a1i
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> _pi e. CC )
6 2ne0
 |-  2 =/= 0
7 6 a1i
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 2 =/= 0 )
8 pire
 |-  _pi e. RR
9 pipos
 |-  0 < _pi
10 8 9 gt0ne0ii
 |-  _pi =/= 0
11 10 a1i
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> _pi =/= 0 )
12 2 3 5 7 11 divdiv1d
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( ( A / 2 ) / _pi ) = ( A / ( 2 x. _pi ) ) )
13 0zd
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 e. ZZ )
14 2re
 |-  2 e. RR
15 14 8 remulcli
 |-  ( 2 x. _pi ) e. RR
16 15 a1i
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( 2 x. _pi ) e. RR )
17 0xr
 |-  0 e. RR*
18 17 a1i
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 e. RR* )
19 16 rexrd
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( 2 x. _pi ) e. RR* )
20 id
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> A e. ( 0 (,) ( 2 x. _pi ) ) )
21 ioogtlb
 |-  ( ( 0 e. RR* /\ ( 2 x. _pi ) e. RR* /\ A e. ( 0 (,) ( 2 x. _pi ) ) ) -> 0 < A )
22 18 19 20 21 syl3anc
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 < A )
23 2pos
 |-  0 < 2
24 14 8 23 9 mulgt0ii
 |-  0 < ( 2 x. _pi )
25 24 a1i
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 < ( 2 x. _pi ) )
26 1 16 22 25 divgt0d
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 < ( A / ( 2 x. _pi ) ) )
27 1rp
 |-  1 e. RR+
28 27 a1i
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 1 e. RR+ )
29 16 25 elrpd
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( 2 x. _pi ) e. RR+ )
30 2 div1d
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( A / 1 ) = A )
31 iooltub
 |-  ( ( 0 e. RR* /\ ( 2 x. _pi ) e. RR* /\ A e. ( 0 (,) ( 2 x. _pi ) ) ) -> A < ( 2 x. _pi ) )
32 18 19 20 31 syl3anc
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> A < ( 2 x. _pi ) )
33 30 32 eqbrtrd
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( A / 1 ) < ( 2 x. _pi ) )
34 1 28 29 33 ltdiv23d
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( A / ( 2 x. _pi ) ) < 1 )
35 1e0p1
 |-  1 = ( 0 + 1 )
36 34 35 breqtrdi
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( A / ( 2 x. _pi ) ) < ( 0 + 1 ) )
37 btwnnz
 |-  ( ( 0 e. ZZ /\ 0 < ( A / ( 2 x. _pi ) ) /\ ( A / ( 2 x. _pi ) ) < ( 0 + 1 ) ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
38 13 26 36 37 syl3anc
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
39 12 38 eqneltrd
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> -. ( ( A / 2 ) / _pi ) e. ZZ )
40 2 halfcld
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( A / 2 ) e. CC )
41 sineq0
 |-  ( ( A / 2 ) e. CC -> ( ( sin ` ( A / 2 ) ) = 0 <-> ( ( A / 2 ) / _pi ) e. ZZ ) )
42 40 41 syl
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( ( sin ` ( A / 2 ) ) = 0 <-> ( ( A / 2 ) / _pi ) e. ZZ ) )
43 39 42 mtbird
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> -. ( sin ` ( A / 2 ) ) = 0 )
44 43 neqned
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( sin ` ( A / 2 ) ) =/= 0 )