Metamath Proof Explorer

Theorem cosq14gt0

Description: The cosine of a number strictly between -upi / 2 and pi / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 halfpire 
 |-  ( _pi / 2 ) e. RR
2 elioore 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A e. RR )
3 resubcl 
 |-  ( ( ( _pi / 2 ) e. RR /\ A e. RR ) -> ( ( _pi / 2 ) - A ) e. RR )
4 1 2 3 sylancr 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( ( _pi / 2 ) - A ) e. RR )
5 neghalfpirx 
 |-  -u ( _pi / 2 ) e. RR*
6 1 rexri 
 |-  ( _pi / 2 ) e. RR*
7 elioo2 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( A e. RR /\ -u ( _pi / 2 ) < A /\ A < ( _pi / 2 ) ) ) )
8 5 6 7 mp2an 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( A e. RR /\ -u ( _pi / 2 ) < A /\ A < ( _pi / 2 ) ) )
9 8 simp3bi 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A < ( _pi / 2 ) )
10 posdif 
 |-  ( ( A e. RR /\ ( _pi / 2 ) e. RR ) -> ( A < ( _pi / 2 ) <-> 0 < ( ( _pi / 2 ) - A ) ) )
11 2 1 10 sylancl 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( A < ( _pi / 2 ) <-> 0 < ( ( _pi / 2 ) - A ) ) )
12 9 11 mpbid 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> 0 < ( ( _pi / 2 ) - A ) )
13 picn 
 |-  _pi e. CC
14 halfcl 
 |-  ( _pi e. CC -> ( _pi / 2 ) e. CC )
15 13 14 ax-mp 
 |-  ( _pi / 2 ) e. CC
16 15 negcli 
 |-  -u ( _pi / 2 ) e. CC
17 13 15 negsubi 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi - ( _pi / 2 ) )
18 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
19 13 15 15 18 subaddrii 
 |-  ( _pi - ( _pi / 2 ) ) = ( _pi / 2 )
20 17 19 eqtri 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi / 2 )
21 15 13 16 20 subaddrii 
 |-  ( ( _pi / 2 ) - _pi ) = -u ( _pi / 2 )
22 8 simp2bi 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> -u ( _pi / 2 ) < A )
23 21 22 eqbrtrid 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( ( _pi / 2 ) - _pi ) < A )
24 pire 
 |-  _pi e. RR
25 ltsub23 
 |-  ( ( ( _pi / 2 ) e. RR /\ A e. RR /\ _pi e. RR ) -> ( ( ( _pi / 2 ) - A ) < _pi <-> ( ( _pi / 2 ) - _pi ) < A ) )
26 1 24 25 mp3an13 
 |-  ( A e. RR -> ( ( ( _pi / 2 ) - A ) < _pi <-> ( ( _pi / 2 ) - _pi ) < A ) )
27 2 26 syl 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( ( ( _pi / 2 ) - A ) < _pi <-> ( ( _pi / 2 ) - _pi ) < A ) )
28 23 27 mpbird 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( ( _pi / 2 ) - A ) < _pi )
29 0xr 
 |-  0 e. RR*
30 24 rexri 
 |-  _pi e. RR*
31 elioo2 
 |-  ( ( 0 e. RR* /\ _pi e. RR* ) -> ( ( ( _pi / 2 ) - A ) e. ( 0 (,) _pi ) <-> ( ( ( _pi / 2 ) - A ) e. RR /\ 0 < ( ( _pi / 2 ) - A ) /\ ( ( _pi / 2 ) - A ) < _pi ) ) )
32 29 30 31 mp2an 
 |-  ( ( ( _pi / 2 ) - A ) e. ( 0 (,) _pi ) <-> ( ( ( _pi / 2 ) - A ) e. RR /\ 0 < ( ( _pi / 2 ) - A ) /\ ( ( _pi / 2 ) - A ) < _pi ) )
33 4 12 28 32 syl3anbrc 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( ( _pi / 2 ) - A ) e. ( 0 (,) _pi ) )
34 sinq12gt0 
 |-  ( ( ( _pi / 2 ) - A ) e. ( 0 (,) _pi ) -> 0 < ( sin ` ( ( _pi / 2 ) - A ) ) )
35 33 34 syl 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> 0 < ( sin ` ( ( _pi / 2 ) - A ) ) )
36 2 recnd 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A e. CC )
37 sinhalfpim 
 |-  ( A e. CC -> ( sin ` ( ( _pi / 2 ) - A ) ) = ( cos ` A ) )
38 36 37 syl 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( sin ` ( ( _pi / 2 ) - A ) ) = ( cos ` A ) )
39 35 38 breqtrd 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> 0 < ( cos ` A ) )