Metamath Proof Explorer


Theorem sincosq1sgn

Description: The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion sincosq1sgn
|- ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )

Proof

Step Hyp Ref Expression
1 0xr
 |-  0 e. RR*
2 halfpire
 |-  ( _pi / 2 ) e. RR
3 2 rexri
 |-  ( _pi / 2 ) e. RR*
4 elioo2
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( A e. ( 0 (,) ( _pi / 2 ) ) <-> ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) ) )
5 1 3 4 mp2an
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) <-> ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) )
6 sincosq1lem
 |-  ( ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) -> 0 < ( sin ` A ) )
7 resubcl
 |-  ( ( ( _pi / 2 ) e. RR /\ A e. RR ) -> ( ( _pi / 2 ) - A ) e. RR )
8 2 7 mpan
 |-  ( A e. RR -> ( ( _pi / 2 ) - A ) e. RR )
9 sincosq1lem
 |-  ( ( ( ( _pi / 2 ) - A ) e. RR /\ 0 < ( ( _pi / 2 ) - A ) /\ ( ( _pi / 2 ) - A ) < ( _pi / 2 ) ) -> 0 < ( sin ` ( ( _pi / 2 ) - A ) ) )
10 8 9 syl3an1
 |-  ( ( A e. RR /\ 0 < ( ( _pi / 2 ) - A ) /\ ( ( _pi / 2 ) - A ) < ( _pi / 2 ) ) -> 0 < ( sin ` ( ( _pi / 2 ) - A ) ) )
11 10 3expib
 |-  ( A e. RR -> ( ( 0 < ( ( _pi / 2 ) - A ) /\ ( ( _pi / 2 ) - A ) < ( _pi / 2 ) ) -> 0 < ( sin ` ( ( _pi / 2 ) - A ) ) ) )
12 0re
 |-  0 e. RR
13 ltsub13
 |-  ( ( 0 e. RR /\ ( _pi / 2 ) e. RR /\ A e. RR ) -> ( 0 < ( ( _pi / 2 ) - A ) <-> A < ( ( _pi / 2 ) - 0 ) ) )
14 12 2 13 mp3an12
 |-  ( A e. RR -> ( 0 < ( ( _pi / 2 ) - A ) <-> A < ( ( _pi / 2 ) - 0 ) ) )
15 2 recni
 |-  ( _pi / 2 ) e. CC
16 15 subid1i
 |-  ( ( _pi / 2 ) - 0 ) = ( _pi / 2 )
17 16 breq2i
 |-  ( A < ( ( _pi / 2 ) - 0 ) <-> A < ( _pi / 2 ) )
18 14 17 bitrdi
 |-  ( A e. RR -> ( 0 < ( ( _pi / 2 ) - A ) <-> A < ( _pi / 2 ) ) )
19 ltsub23
 |-  ( ( ( _pi / 2 ) e. RR /\ A e. RR /\ ( _pi / 2 ) e. RR ) -> ( ( ( _pi / 2 ) - A ) < ( _pi / 2 ) <-> ( ( _pi / 2 ) - ( _pi / 2 ) ) < A ) )
20 2 2 19 mp3an13
 |-  ( A e. RR -> ( ( ( _pi / 2 ) - A ) < ( _pi / 2 ) <-> ( ( _pi / 2 ) - ( _pi / 2 ) ) < A ) )
21 15 subidi
 |-  ( ( _pi / 2 ) - ( _pi / 2 ) ) = 0
22 21 breq1i
 |-  ( ( ( _pi / 2 ) - ( _pi / 2 ) ) < A <-> 0 < A )
23 20 22 bitrdi
 |-  ( A e. RR -> ( ( ( _pi / 2 ) - A ) < ( _pi / 2 ) <-> 0 < A ) )
24 18 23 anbi12d
 |-  ( A e. RR -> ( ( 0 < ( ( _pi / 2 ) - A ) /\ ( ( _pi / 2 ) - A ) < ( _pi / 2 ) ) <-> ( A < ( _pi / 2 ) /\ 0 < A ) ) )
25 24 biancomd
 |-  ( A e. RR -> ( ( 0 < ( ( _pi / 2 ) - A ) /\ ( ( _pi / 2 ) - A ) < ( _pi / 2 ) ) <-> ( 0 < A /\ A < ( _pi / 2 ) ) ) )
26 recn
 |-  ( A e. RR -> A e. CC )
27 sinhalfpim
 |-  ( A e. CC -> ( sin ` ( ( _pi / 2 ) - A ) ) = ( cos ` A ) )
28 26 27 syl
 |-  ( A e. RR -> ( sin ` ( ( _pi / 2 ) - A ) ) = ( cos ` A ) )
29 28 breq2d
 |-  ( A e. RR -> ( 0 < ( sin ` ( ( _pi / 2 ) - A ) ) <-> 0 < ( cos ` A ) ) )
30 11 25 29 3imtr3d
 |-  ( A e. RR -> ( ( 0 < A /\ A < ( _pi / 2 ) ) -> 0 < ( cos ` A ) ) )
31 30 3impib
 |-  ( ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) -> 0 < ( cos ` A ) )
32 6 31 jca
 |-  ( ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
33 5 32 sylbi
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )