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 ) )