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