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 ‘ 𝐴 ) ) )