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 )