Metamath Proof Explorer

Theorem sin02gt0

Description: The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008)

Ref Expression
Assertion sin02gt0 
|- ( A e. ( 0 (,] 2 ) -> 0 < ( sin ` A ) )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 2re 
 |-  2 e. RR
3 elioc2 
 |-  ( ( 0 e. RR* /\ 2 e. RR ) -> ( A e. ( 0 (,] 2 ) <-> ( A e. RR /\ 0 < A /\ A <_ 2 ) ) )
4 1 2 3 mp2an 
 |-  ( A e. ( 0 (,] 2 ) <-> ( A e. RR /\ 0 < A /\ A <_ 2 ) )
5 rehalfcl 
 |-  ( A e. RR -> ( A / 2 ) e. RR )
6 5 3ad2ant1 
 |-  ( ( A e. RR /\ 0 < A /\ A <_ 2 ) -> ( A / 2 ) e. RR )
7 4 6 sylbi 
 |-  ( A e. ( 0 (,] 2 ) -> ( A / 2 ) e. RR )
8 resincl 
 |-  ( ( A / 2 ) e. RR -> ( sin ` ( A / 2 ) ) e. RR )
9 recoscl 
 |-  ( ( A / 2 ) e. RR -> ( cos ` ( A / 2 ) ) e. RR )
10 8 9 remulcld 
 |-  ( ( A / 2 ) e. RR -> ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) e. RR )
11 7 10 syl 
 |-  ( A e. ( 0 (,] 2 ) -> ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) e. RR )
12 2pos 
 |-  0 < 2
13 divgt0 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( A / 2 ) )
14 2 12 13 mpanr12 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( A / 2 ) )
15 14 3adant3 
 |-  ( ( A e. RR /\ 0 < A /\ A <_ 2 ) -> 0 < ( A / 2 ) )
16 2 12 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
17 lediv1 
 |-  ( ( A e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( A <_ 2 <-> ( A / 2 ) <_ ( 2 / 2 ) ) )
18 2 16 17 mp3an23 
 |-  ( A e. RR -> ( A <_ 2 <-> ( A / 2 ) <_ ( 2 / 2 ) ) )
19 18 biimpa 
 |-  ( ( A e. RR /\ A <_ 2 ) -> ( A / 2 ) <_ ( 2 / 2 ) )
20 2div2e1 
 |-  ( 2 / 2 ) = 1
21 19 20 breqtrdi 
 |-  ( ( A e. RR /\ A <_ 2 ) -> ( A / 2 ) <_ 1 )
22 21 3adant2 
 |-  ( ( A e. RR /\ 0 < A /\ A <_ 2 ) -> ( A / 2 ) <_ 1 )
23 6 15 22 3jca 
 |-  ( ( A e. RR /\ 0 < A /\ A <_ 2 ) -> ( ( A / 2 ) e. RR /\ 0 < ( A / 2 ) /\ ( A / 2 ) <_ 1 ) )
24 1re 
 |-  1 e. RR
25 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( ( A / 2 ) e. ( 0 (,] 1 ) <-> ( ( A / 2 ) e. RR /\ 0 < ( A / 2 ) /\ ( A / 2 ) <_ 1 ) ) )
26 1 24 25 mp2an 
 |-  ( ( A / 2 ) e. ( 0 (,] 1 ) <-> ( ( A / 2 ) e. RR /\ 0 < ( A / 2 ) /\ ( A / 2 ) <_ 1 ) )
27 23 4 26 3imtr4i 
 |-  ( A e. ( 0 (,] 2 ) -> ( A / 2 ) e. ( 0 (,] 1 ) )
28 sin01gt0 
 |-  ( ( A / 2 ) e. ( 0 (,] 1 ) -> 0 < ( sin ` ( A / 2 ) ) )
29 27 28 syl 
 |-  ( A e. ( 0 (,] 2 ) -> 0 < ( sin ` ( A / 2 ) ) )
30 cos01gt0 
 |-  ( ( A / 2 ) e. ( 0 (,] 1 ) -> 0 < ( cos ` ( A / 2 ) ) )
31 27 30 syl 
 |-  ( A e. ( 0 (,] 2 ) -> 0 < ( cos ` ( A / 2 ) ) )
32 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 ) ) ) ) )
33 8 9 32 syl2anc 
 |-  ( ( A / 2 ) e. RR -> ( ( 0 < ( sin ` ( A / 2 ) ) /\ 0 < ( cos ` ( A / 2 ) ) ) -> 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
34 7 33 syl 
 |-  ( A e. ( 0 (,] 2 ) -> ( ( 0 < ( sin ` ( A / 2 ) ) /\ 0 < ( cos ` ( A / 2 ) ) ) -> 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
35 29 31 34 mp2and 
 |-  ( A e. ( 0 (,] 2 ) -> 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) )
36 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 ) ) ) ) ) )
37 2 36 mpan 
 |-  ( ( ( 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 ) ) ) ) ) )
38 12 37 mpani 
 |-  ( ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) e. RR -> ( 0 < ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) -> 0 < ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) ) )
39 11 35 38 sylc 
 |-  ( A e. ( 0 (,] 2 ) -> 0 < ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
40 7 recnd 
 |-  ( A e. ( 0 (,] 2 ) -> ( A / 2 ) e. CC )
41 sin2t 
 |-  ( ( A / 2 ) e. CC -> ( sin ` ( 2 x. ( A / 2 ) ) ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
42 40 41 syl 
 |-  ( A e. ( 0 (,] 2 ) -> ( sin ` ( 2 x. ( A / 2 ) ) ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
43 39 42 breqtrrd 
 |-  ( A e. ( 0 (,] 2 ) -> 0 < ( sin ` ( 2 x. ( A / 2 ) ) ) )
44 4 simp1bi 
 |-  ( A e. ( 0 (,] 2 ) -> A e. RR )
45 44 recnd 
 |-  ( A e. ( 0 (,] 2 ) -> A e. CC )
46 2cn 
 |-  2 e. CC
47 2ne0 
 |-  2 =/= 0
48 divcan2 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( A / 2 ) ) = A )
49 46 47 48 mp3an23 
 |-  ( A e. CC -> ( 2 x. ( A / 2 ) ) = A )
50 45 49 syl 
 |-  ( A e. ( 0 (,] 2 ) -> ( 2 x. ( A / 2 ) ) = A )
51 50 fveq2d 
 |-  ( A e. ( 0 (,] 2 ) -> ( sin ` ( 2 x. ( A / 2 ) ) ) = ( sin ` A ) )
52 43 51 breqtrd 
 |-  ( A e. ( 0 (,] 2 ) -> 0 < ( sin ` A ) )