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