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