Metamath Proof Explorer


Theorem sinq12ge0

Description: The sine of a number between 0 and _pi is nonnegative. (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Assertion sinq12ge0
|- ( A e. ( 0 [,] _pi ) -> 0 <_ ( sin ` A ) )

Proof

Step Hyp Ref Expression
1 0re
 |-  0 e. RR
2 pire
 |-  _pi e. RR
3 1 2 elicc2i
 |-  ( A e. ( 0 [,] _pi ) <-> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) )
4 3 simp1bi
 |-  ( A e. ( 0 [,] _pi ) -> A e. RR )
5 rexr
 |-  ( 0 e. RR -> 0 e. RR* )
6 rexr
 |-  ( _pi e. RR -> _pi e. RR* )
7 elioo2
 |-  ( ( 0 e. RR* /\ _pi e. RR* ) -> ( A e. ( 0 (,) _pi ) <-> ( A e. RR /\ 0 < A /\ A < _pi ) ) )
8 5 6 7 syl2an
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( A e. ( 0 (,) _pi ) <-> ( A e. RR /\ 0 < A /\ A < _pi ) ) )
9 1 2 8 mp2an
 |-  ( A e. ( 0 (,) _pi ) <-> ( A e. RR /\ 0 < A /\ A < _pi ) )
10 sinq12gt0
 |-  ( A e. ( 0 (,) _pi ) -> 0 < ( sin ` A ) )
11 9 10 sylbir
 |-  ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( sin ` A ) )
12 11 3expib
 |-  ( A e. RR -> ( ( 0 < A /\ A < _pi ) -> 0 < ( sin ` A ) ) )
13 4 12 syl
 |-  ( A e. ( 0 [,] _pi ) -> ( ( 0 < A /\ A < _pi ) -> 0 < ( sin ` A ) ) )
14 4 resincld
 |-  ( A e. ( 0 [,] _pi ) -> ( sin ` A ) e. RR )
15 ltle
 |-  ( ( 0 e. RR /\ ( sin ` A ) e. RR ) -> ( 0 < ( sin ` A ) -> 0 <_ ( sin ` A ) ) )
16 1 14 15 sylancr
 |-  ( A e. ( 0 [,] _pi ) -> ( 0 < ( sin ` A ) -> 0 <_ ( sin ` A ) ) )
17 13 16 syld
 |-  ( A e. ( 0 [,] _pi ) -> ( ( 0 < A /\ A < _pi ) -> 0 <_ ( sin ` A ) ) )
18 17 expd
 |-  ( A e. ( 0 [,] _pi ) -> ( 0 < A -> ( A < _pi -> 0 <_ ( sin ` A ) ) ) )
19 0le0
 |-  0 <_ 0
20 sin0
 |-  ( sin ` 0 ) = 0
21 19 20 breqtrri
 |-  0 <_ ( sin ` 0 )
22 fveq2
 |-  ( 0 = A -> ( sin ` 0 ) = ( sin ` A ) )
23 21 22 breqtrid
 |-  ( 0 = A -> 0 <_ ( sin ` A ) )
24 23 a1i13
 |-  ( A e. ( 0 [,] _pi ) -> ( 0 = A -> ( A < _pi -> 0 <_ ( sin ` A ) ) ) )
25 3 simp2bi
 |-  ( A e. ( 0 [,] _pi ) -> 0 <_ A )
26 leloe
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
27 1 4 26 sylancr
 |-  ( A e. ( 0 [,] _pi ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
28 25 27 mpbid
 |-  ( A e. ( 0 [,] _pi ) -> ( 0 < A \/ 0 = A ) )
29 18 24 28 mpjaod
 |-  ( A e. ( 0 [,] _pi ) -> ( A < _pi -> 0 <_ ( sin ` A ) ) )
30 sinpi
 |-  ( sin ` _pi ) = 0
31 19 30 breqtrri
 |-  0 <_ ( sin ` _pi )
32 fveq2
 |-  ( A = _pi -> ( sin ` A ) = ( sin ` _pi ) )
33 31 32 breqtrrid
 |-  ( A = _pi -> 0 <_ ( sin ` A ) )
34 33 a1i
 |-  ( A e. ( 0 [,] _pi ) -> ( A = _pi -> 0 <_ ( sin ` A ) ) )
35 3 simp3bi
 |-  ( A e. ( 0 [,] _pi ) -> A <_ _pi )
36 leloe
 |-  ( ( A e. RR /\ _pi e. RR ) -> ( A <_ _pi <-> ( A < _pi \/ A = _pi ) ) )
37 4 2 36 sylancl
 |-  ( A e. ( 0 [,] _pi ) -> ( A <_ _pi <-> ( A < _pi \/ A = _pi ) ) )
38 35 37 mpbid
 |-  ( A e. ( 0 [,] _pi ) -> ( A < _pi \/ A = _pi ) )
39 29 34 38 mpjaod
 |-  ( A e. ( 0 [,] _pi ) -> 0 <_ ( sin ` A ) )