# 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 syl6bb
` |-  ( 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 syl6bb
` |-  ( 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 ) ) )`