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 0 π 2 0 < sin A 0 < cos A

Proof

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