# 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`