Metamath Proof Explorer

Theorem cosq14ge0

Description: The cosine of a number between -upi / 2 and pi / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Assertion cosq14ge0 
|- ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> 0 <_ ( cos ` A ) )

Proof

Step Hyp Ref Expression
1 halfpire 
 |-  ( _pi / 2 ) e. RR
2 neghalfpire 
 |-  -u ( _pi / 2 ) e. RR
3 2 1 elicc2i 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( A e. RR /\ -u ( _pi / 2 ) <_ A /\ A <_ ( _pi / 2 ) ) )
4 3 simp1bi 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> A e. RR )
5 resubcl 
 |-  ( ( ( _pi / 2 ) e. RR /\ A e. RR ) -> ( ( _pi / 2 ) - A ) e. RR )
6 1 4 5 sylancr 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - A ) e. RR )
7 3 simp3bi 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> A <_ ( _pi / 2 ) )
8 subge0 
 |-  ( ( ( _pi / 2 ) e. RR /\ A e. RR ) -> ( 0 <_ ( ( _pi / 2 ) - A ) <-> A <_ ( _pi / 2 ) ) )
9 1 4 8 sylancr 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( 0 <_ ( ( _pi / 2 ) - A ) <-> A <_ ( _pi / 2 ) ) )
10 7 9 mpbird 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> 0 <_ ( ( _pi / 2 ) - A ) )
11 picn 
 |-  _pi e. CC
12 halfcl 
 |-  ( _pi e. CC -> ( _pi / 2 ) e. CC )
13 11 12 ax-mp 
 |-  ( _pi / 2 ) e. CC
14 13 negcli 
 |-  -u ( _pi / 2 ) e. CC
15 11 13 negsubi 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi - ( _pi / 2 ) )
16 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
17 11 13 13 16 subaddrii 
 |-  ( _pi - ( _pi / 2 ) ) = ( _pi / 2 )
18 15 17 eqtri 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi / 2 )
19 13 11 14 18 subaddrii 
 |-  ( ( _pi / 2 ) - _pi ) = -u ( _pi / 2 )
20 3 simp2bi 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> -u ( _pi / 2 ) <_ A )
21 19 20 eqbrtrid 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - _pi ) <_ A )
22 pire 
 |-  _pi e. RR
23 suble 
 |-  ( ( ( _pi / 2 ) e. RR /\ A e. RR /\ _pi e. RR ) -> ( ( ( _pi / 2 ) - A ) <_ _pi <-> ( ( _pi / 2 ) - _pi ) <_ A ) )
24 1 22 23 mp3an13 
 |-  ( A e. RR -> ( ( ( _pi / 2 ) - A ) <_ _pi <-> ( ( _pi / 2 ) - _pi ) <_ A ) )
25 4 24 syl 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( ( _pi / 2 ) - A ) <_ _pi <-> ( ( _pi / 2 ) - _pi ) <_ A ) )
26 21 25 mpbird 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - A ) <_ _pi )
27 0re 
 |-  0 e. RR
28 27 22 elicc2i 
 |-  ( ( ( _pi / 2 ) - A ) e. ( 0 [,] _pi ) <-> ( ( ( _pi / 2 ) - A ) e. RR /\ 0 <_ ( ( _pi / 2 ) - A ) /\ ( ( _pi / 2 ) - A ) <_ _pi ) )
29 6 10 26 28 syl3anbrc 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - A ) e. ( 0 [,] _pi ) )
30 sinq12ge0 
 |-  ( ( ( _pi / 2 ) - A ) e. ( 0 [,] _pi ) -> 0 <_ ( sin ` ( ( _pi / 2 ) - A ) ) )
31 29 30 syl 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> 0 <_ ( sin ` ( ( _pi / 2 ) - A ) ) )
32 4 recnd 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> A e. CC )
33 sinhalfpim 
 |-  ( A e. CC -> ( sin ` ( ( _pi / 2 ) - A ) ) = ( cos ` A ) )
34 32 33 syl 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( sin ` ( ( _pi / 2 ) - A ) ) = ( cos ` A ) )
35 31 34 breqtrd 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> 0 <_ ( cos ` A ) )