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