Metamath Proof Explorer

Theorem sinq12gt0

Description: The sine of a number strictly between 0 and _pi is positive. (Contributed by Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion sinq12gt0 
|- ( A e. ( 0 (,) _pi ) -> 0 < ( sin ` A ) )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 pire 
 |-  _pi e. RR
3 2 rexri 
 |-  _pi e. RR*
4 elioo2 
 |-  ( ( 0 e. RR* /\ _pi e. RR* ) -> ( A e. ( 0 (,) _pi ) <-> ( A e. RR /\ 0 < A /\ A < _pi ) ) )
5 1 3 4 mp2an 
 |-  ( A e. ( 0 (,) _pi ) <-> ( A e. RR /\ 0 < A /\ A < _pi ) )
6 rehalfcl 
 |-  ( A e. RR -> ( A / 2 ) e. RR )
7 6 3ad2ant1 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> ( A / 2 ) e. RR )
8 halfpos2 
 |-  ( A e. RR -> ( 0 < A <-> 0 < ( A / 2 ) ) )
9 8 biimpa 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( A / 2 ) )
10 9 3adant3 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( A / 2 ) )
11 2re 
 |-  2 e. RR
12 2pos 
 |-  0 < 2
13 11 12 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
14 ltdiv1 
 |-  ( ( A e. RR /\ _pi e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( A < _pi <-> ( A / 2 ) < ( _pi / 2 ) ) )
15 2 13 14 mp3an23 
 |-  ( A e. RR -> ( A < _pi <-> ( A / 2 ) < ( _pi / 2 ) ) )
16 15 adantr 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A < _pi <-> ( A / 2 ) < ( _pi / 2 ) ) )
17 16 biimp3a 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> ( A / 2 ) < ( _pi / 2 ) )
18 sincosq1lem 
 |-  ( ( ( A / 2 ) e. RR /\ 0 < ( A / 2 ) /\ ( A / 2 ) < ( _pi / 2 ) ) -> 0 < ( sin ` ( A / 2 ) ) )
19 7 10 17 18 syl3anc 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( sin ` ( A / 2 ) ) )
20 resubcl 
 |-  ( ( _pi e. RR /\ A e. RR ) -> ( _pi - A ) e. RR )
21 2 20 mpan 
 |-  ( A e. RR -> ( _pi - A ) e. RR )
22 rehalfcl 
 |-  ( ( _pi - A ) e. RR -> ( ( _pi - A ) / 2 ) e. RR )
23 21 22 syl 
 |-  ( A e. RR -> ( ( _pi - A ) / 2 ) e. RR )
24 23 3ad2ant1 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> ( ( _pi - A ) / 2 ) e. RR )
25 posdif 
 |-  ( ( A e. RR /\ _pi e. RR ) -> ( A < _pi <-> 0 < ( _pi - A ) ) )
26 2 25 mpan2 
 |-  ( A e. RR -> ( A < _pi <-> 0 < ( _pi - A ) ) )
27 halfpos2 
 |-  ( ( _pi - A ) e. RR -> ( 0 < ( _pi - A ) <-> 0 < ( ( _pi - A ) / 2 ) ) )
28 21 27 syl 
 |-  ( A e. RR -> ( 0 < ( _pi - A ) <-> 0 < ( ( _pi - A ) / 2 ) ) )
29 26 28 bitrd 
 |-  ( A e. RR -> ( A < _pi <-> 0 < ( ( _pi - A ) / 2 ) ) )
30 29 adantr 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A < _pi <-> 0 < ( ( _pi - A ) / 2 ) ) )
31 30 biimp3a 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( ( _pi - A ) / 2 ) )
32 ltsubpos 
 |-  ( ( A e. RR /\ _pi e. RR ) -> ( 0 < A <-> ( _pi - A ) < _pi ) )
33 2 32 mpan2 
 |-  ( A e. RR -> ( 0 < A <-> ( _pi - A ) < _pi ) )
34 ltdiv1 
 |-  ( ( ( _pi - A ) e. RR /\ _pi e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( _pi - A ) < _pi <-> ( ( _pi - A ) / 2 ) < ( _pi / 2 ) ) )
35 2 13 34 mp3an23 
 |-  ( ( _pi - A ) e. RR -> ( ( _pi - A ) < _pi <-> ( ( _pi - A ) / 2 ) < ( _pi / 2 ) ) )
36 21 35 syl 
 |-  ( A e. RR -> ( ( _pi - A ) < _pi <-> ( ( _pi - A ) / 2 ) < ( _pi / 2 ) ) )
37 33 36 bitrd 
 |-  ( A e. RR -> ( 0 < A <-> ( ( _pi - A ) / 2 ) < ( _pi / 2 ) ) )
38 37 biimpa 
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( _pi - A ) / 2 ) < ( _pi / 2 ) )
39 38 3adant3 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> ( ( _pi - A ) / 2 ) < ( _pi / 2 ) )
40 sincosq1lem 
 |-  ( ( ( ( _pi - A ) / 2 ) e. RR /\ 0 < ( ( _pi - A ) / 2 ) /\ ( ( _pi - A ) / 2 ) < ( _pi / 2 ) ) -> 0 < ( sin ` ( ( _pi - A ) / 2 ) ) )
41 24 31 39 40 syl3anc 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( sin ` ( ( _pi - A ) / 2 ) ) )
42 recn 
 |-  ( A e. RR -> A e. CC )
43 picn 
 |-  _pi e. CC
44 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
45 divsubdir 
 |-  ( ( _pi e. CC /\ A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( _pi - A ) / 2 ) = ( ( _pi / 2 ) - ( A / 2 ) ) )
46 43 44 45 mp3an13 
 |-  ( A e. CC -> ( ( _pi - A ) / 2 ) = ( ( _pi / 2 ) - ( A / 2 ) ) )
47 42 46 syl 
 |-  ( A e. RR -> ( ( _pi - A ) / 2 ) = ( ( _pi / 2 ) - ( A / 2 ) ) )
48 47 fveq2d 
 |-  ( A e. RR -> ( sin ` ( ( _pi - A ) / 2 ) ) = ( sin ` ( ( _pi / 2 ) - ( A / 2 ) ) ) )
49 6 recnd 
 |-  ( A e. RR -> ( A / 2 ) e. CC )
50 sinhalfpim 
 |-  ( ( A / 2 ) e. CC -> ( sin ` ( ( _pi / 2 ) - ( A / 2 ) ) ) = ( cos ` ( A / 2 ) ) )
51 49 50 syl 
 |-  ( A e. RR -> ( sin ` ( ( _pi / 2 ) - ( A / 2 ) ) ) = ( cos ` ( A / 2 ) ) )
52 48 51 eqtrd 
 |-  ( A e. RR -> ( sin ` ( ( _pi - A ) / 2 ) ) = ( cos ` ( A / 2 ) ) )
53 52 3ad2ant1 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> ( sin ` ( ( _pi - A ) / 2 ) ) = ( cos ` ( A / 2 ) ) )
54 41 53 breqtrd 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( cos ` ( A / 2 ) ) )
55 resincl 
 |-  ( ( A / 2 ) e. RR -> ( sin ` ( A / 2 ) ) e. RR )
56 recoscl 
 |-  ( ( A / 2 ) e. RR -> ( cos ` ( A / 2 ) ) e. RR )
57 55 56 jca 
 |-  ( ( A / 2 ) e. RR -> ( ( sin ` ( A / 2 ) ) e. RR /\ ( cos ` ( A / 2 ) ) e. RR ) )
58 axmulgt0 
 |-  ( ( ( sin ` ( A / 2 ) ) e. RR /\ ( cos ` ( A / 2 ) ) e. RR ) -> ( ( 0 < ( sin ` ( A / 2 ) ) /\ 0 < ( cos ` ( A / 2 ) ) ) -> 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
59 6 57 58 3syl 
 |-  ( A e. RR -> ( ( 0 < ( sin ` ( A / 2 ) ) /\ 0 < ( cos ` ( A / 2 ) ) ) -> 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
60 remulcl 
 |-  ( ( ( sin ` ( A / 2 ) ) e. RR /\ ( cos ` ( A / 2 ) ) e. RR ) -> ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) e. RR )
61 6 57 60 3syl 
 |-  ( A e. RR -> ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) e. RR )
62 axmulgt0 
 |-  ( ( 2 e. RR /\ ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) e. RR ) -> ( ( 0 < 2 /\ 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) -> 0 < ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) ) )
63 11 61 62 sylancr 
 |-  ( A e. RR -> ( ( 0 < 2 /\ 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) -> 0 < ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) ) )
64 12 63 mpani 
 |-  ( A e. RR -> ( 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) -> 0 < ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) ) )
65 59 64 syld 
 |-  ( A e. RR -> ( ( 0 < ( sin ` ( A / 2 ) ) /\ 0 < ( cos ` ( A / 2 ) ) ) -> 0 < ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) ) )
66 65 3ad2ant1 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> ( ( 0 < ( sin ` ( A / 2 ) ) /\ 0 < ( cos ` ( A / 2 ) ) ) -> 0 < ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) ) )
67 19 54 66 mp2and 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
68 2cn 
 |-  2 e. CC
69 2ne0 
 |-  2 =/= 0
70 divcan2 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( A / 2 ) ) = A )
71 68 69 70 mp3an23 
 |-  ( A e. CC -> ( 2 x. ( A / 2 ) ) = A )
72 42 71 syl 
 |-  ( A e. RR -> ( 2 x. ( A / 2 ) ) = A )
73 72 fveq2d 
 |-  ( A e. RR -> ( sin ` ( 2 x. ( A / 2 ) ) ) = ( sin ` A ) )
74 sin2t 
 |-  ( ( A / 2 ) e. CC -> ( sin ` ( 2 x. ( A / 2 ) ) ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
75 49 74 syl 
 |-  ( A e. RR -> ( sin ` ( 2 x. ( A / 2 ) ) ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
76 73 75 eqtr3d 
 |-  ( A e. RR -> ( sin ` A ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
77 76 3ad2ant1 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> ( sin ` A ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
78 67 77 breqtrrd 
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( sin ` A ) )
79 5 78 sylbi 
 |-  ( A e. ( 0 (,) _pi ) -> 0 < ( sin ` A ) )