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 ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( sin ‘ 𝐴 ) ∧ 0 < ( cos ‘ 𝐴 ) ) )

Proof

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