Metamath Proof Explorer

Theorem sincosq3sgn

Description: The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion sincosq3sgn ( 𝐴 ∈ ( π (,) ( 3 · ( π / 2 ) ) ) → ( ( sin ‘ 𝐴 ) < 0 ∧ ( cos ‘ 𝐴 ) < 0 ) )

Proof

Step Hyp Ref Expression
1 pire ⊢ π ∈ ℝ
2 3re ⊢ 3 ∈ ℝ
3 halfpire ⊢ ( π / 2 ) ∈ ℝ
4 2 3 remulcli ⊢ ( 3 · ( π / 2 ) ) ∈ ℝ
5 rexr ⊢ ( π ∈ ℝ → π ∈ ℝ* )
6 rexr ⊢ ( ( 3 · ( π / 2 ) ) ∈ ℝ → ( 3 · ( π / 2 ) ) ∈ ℝ* )
7 elioo2 ⊢ ( ( π ∈ ℝ* ∧ ( 3 · ( π / 2 ) ) ∈ ℝ* ) → ( 𝐴 ∈ ( π (,) ( 3 · ( π / 2 ) ) ) ↔ ( 𝐴 ∈ ℝ ∧ π < 𝐴 ∧ 𝐴 < ( 3 · ( π / 2 ) ) ) ) )
8 5 6 7 syl2an ⊢ ( ( π ∈ ℝ ∧ ( 3 · ( π / 2 ) ) ∈ ℝ ) → ( 𝐴 ∈ ( π (,) ( 3 · ( π / 2 ) ) ) ↔ ( 𝐴 ∈ ℝ ∧ π < 𝐴 ∧ 𝐴 < ( 3 · ( π / 2 ) ) ) ) )
9 1 4 8 mp2an ⊢ ( 𝐴 ∈ ( π (,) ( 3 · ( π / 2 ) ) ) ↔ ( 𝐴 ∈ ℝ ∧ π < 𝐴 ∧ 𝐴 < ( 3 · ( π / 2 ) ) ) )
10 pidiv2halves ⊢ ( ( π / 2 ) + ( π / 2 ) ) = π
11 10 breq1i ⊢ ( ( ( π / 2 ) + ( π / 2 ) ) < 𝐴 ↔ π < 𝐴 )
12 ltaddsub ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( ( π / 2 ) + ( π / 2 ) ) < 𝐴 ↔ ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ) )
13 3 3 12 mp3an12 ⊢ ( 𝐴 ∈ ℝ → ( ( ( π / 2 ) + ( π / 2 ) ) < 𝐴 ↔ ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ) )
14 11 13 bitr3id ⊢ ( 𝐴 ∈ ℝ → ( π < 𝐴 ↔ ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ) )
15 ltsubadd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( 𝐴 − ( π / 2 ) ) < π ↔ 𝐴 < ( π + ( π / 2 ) ) ) )
16 3 1 15 mp3an23 ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( π / 2 ) ) < π ↔ 𝐴 < ( π + ( π / 2 ) ) ) )
17 df-3 ⊢ 3 = ( 2 + 1 )
18 17 oveq1i ⊢ ( 3 · ( π / 2 ) ) = ( ( 2 + 1 ) · ( π / 2 ) )
19 2cn ⊢ 2 ∈ ℂ
20 ax-1cn ⊢ 1 ∈ ℂ
21 3 recni ⊢ ( π / 2 ) ∈ ℂ
22 19 20 21 adddiri ⊢ ( ( 2 + 1 ) · ( π / 2 ) ) = ( ( 2 · ( π / 2 ) ) + ( 1 · ( π / 2 ) ) )
23 1 recni ⊢ π ∈ ℂ
24 2ne0 ⊢ 2 ≠ 0
25 23 19 24 divcan2i ⊢ ( 2 · ( π / 2 ) ) = π
26 21 mulid2i ⊢ ( 1 · ( π / 2 ) ) = ( π / 2 )
27 25 26 oveq12i ⊢ ( ( 2 · ( π / 2 ) ) + ( 1 · ( π / 2 ) ) ) = ( π + ( π / 2 ) )
28 18 22 27 3eqtrri ⊢ ( π + ( π / 2 ) ) = ( 3 · ( π / 2 ) )
29 28 breq2i ⊢ ( 𝐴 < ( π + ( π / 2 ) ) ↔ 𝐴 < ( 3 · ( π / 2 ) ) )
30 16 29 bitr2di ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < ( 3 · ( π / 2 ) ) ↔ ( 𝐴 − ( π / 2 ) ) < π ) )
31 14 30 anbi12d ⊢ ( 𝐴 ∈ ℝ → ( ( π < 𝐴 ∧ 𝐴 < ( 3 · ( π / 2 ) ) ) ↔ ( ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < π ) ) )
32 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 𝐴 − ( π / 2 ) ) ∈ ℝ )
33 3 32 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( π / 2 ) ) ∈ ℝ )
34 sincosq2sgn ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ( ( π / 2 ) (,) π ) → ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
35 rexr ⊢ ( ( π / 2 ) ∈ ℝ → ( π / 2 ) ∈ ℝ* )
36 elioo2 ⊢ ( ( ( π / 2 ) ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( 𝐴 − ( π / 2 ) ) ∈ ( ( π / 2 ) (,) π ) ↔ ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < π ) ) )
37 35 5 36 syl2an ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( 𝐴 − ( π / 2 ) ) ∈ ( ( π / 2 ) (,) π ) ↔ ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < π ) ) )
38 3 1 37 mp2an ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ( ( π / 2 ) (,) π ) ↔ ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < π ) )
39 ancom ⊢ ( ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ↔ ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
40 34 38 39 3imtr3i ⊢ ( ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < π ) → ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
41 33 40 syl3an1 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < π ) → ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
42 41 3expib ⊢ ( 𝐴 ∈ ℝ → ( ( ( π / 2 ) < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < π ) → ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ) ) )
43 31 42 sylbid ⊢ ( 𝐴 ∈ ℝ → ( ( π < 𝐴 ∧ 𝐴 < ( 3 · ( π / 2 ) ) ) → ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ) ) )
44 33 resincld ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∈ ℝ )
45 44 lt0neg2d ⊢ ( 𝐴 ∈ ℝ → ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ↔ - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
46 45 anbi2d ⊢ ( 𝐴 ∈ ℝ → ( ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ) ↔ ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ) )
47 43 46 sylibd ⊢ ( 𝐴 ∈ ℝ → ( ( π < 𝐴 ∧ 𝐴 < ( 3 · ( π / 2 ) ) ) → ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ) )
48 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
49 pncan3 ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) = 𝐴 )
50 21 48 49 sylancr ⊢ ( 𝐴 ∈ ℝ → ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) = 𝐴 )
51 50 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( sin ‘ 𝐴 ) )
52 33 recnd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( π / 2 ) ) ∈ ℂ )
53 sinhalfpip ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ℂ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
54 52 53 syl ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
55 51 54 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
56 55 breq1d ⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ 𝐴 ) < 0 ↔ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
57 50 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ 𝐴 ) )
58 coshalfpip ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
59 52 58 syl ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
60 57 59 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
61 60 breq1d ⊢ ( 𝐴 ∈ ℝ → ( ( cos ‘ 𝐴 ) < 0 ↔ - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
62 56 61 anbi12d ⊢ ( 𝐴 ∈ ℝ → ( ( ( sin ‘ 𝐴 ) < 0 ∧ ( cos ‘ 𝐴 ) < 0 ) ↔ ( ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ) )
63 47 62 sylibrd ⊢ ( 𝐴 ∈ ℝ → ( ( π < 𝐴 ∧ 𝐴 < ( 3 · ( π / 2 ) ) ) → ( ( sin ‘ 𝐴 ) < 0 ∧ ( cos ‘ 𝐴 ) < 0 ) ) )
64 63 3impib ⊢ ( ( 𝐴 ∈ ℝ ∧ π < 𝐴 ∧ 𝐴 < ( 3 · ( π / 2 ) ) ) → ( ( sin ‘ 𝐴 ) < 0 ∧ ( cos ‘ 𝐴 ) < 0 ) )
65 9 64 sylbi ⊢ ( 𝐴 ∈ ( π (,) ( 3 · ( π / 2 ) ) ) → ( ( sin ‘ 𝐴 ) < 0 ∧ ( cos ‘ 𝐴 ) < 0 ) )