Metamath Proof Explorer

Theorem sincosq4sgn

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

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

Proof

Step Hyp Ref Expression
1 3re ⊢ 3 ∈ ℝ
2 halfpire ⊢ ( π / 2 ) ∈ ℝ
3 1 2 remulcli ⊢ ( 3 · ( π / 2 ) ) ∈ ℝ
4 3 rexri ⊢ ( 3 · ( π / 2 ) ) ∈ ℝ*
5 2re ⊢ 2 ∈ ℝ
6 pire ⊢ π ∈ ℝ
7 5 6 remulcli ⊢ ( 2 · π ) ∈ ℝ
8 7 rexri ⊢ ( 2 · π ) ∈ ℝ*
9 elioo2 ⊢ ( ( ( 3 · ( π / 2 ) ) ∈ ℝ* ∧ ( 2 · π ) ∈ ℝ* ) → ( 𝐴 ∈ ( ( 3 · ( π / 2 ) ) (,) ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ ( 3 · ( π / 2 ) ) < 𝐴 ∧ 𝐴 < ( 2 · π ) ) ) )
10 4 8 9 mp2an ⊢ ( 𝐴 ∈ ( ( 3 · ( π / 2 ) ) (,) ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ ( 3 · ( π / 2 ) ) < 𝐴 ∧ 𝐴 < ( 2 · π ) ) )
11 df-3 ⊢ 3 = ( 2 + 1 )
12 11 oveq1i ⊢ ( 3 · ( π / 2 ) ) = ( ( 2 + 1 ) · ( π / 2 ) )
13 2cn ⊢ 2 ∈ ℂ
14 ax-1cn ⊢ 1 ∈ ℂ
15 2 recni ⊢ ( π / 2 ) ∈ ℂ
16 13 14 15 adddiri ⊢ ( ( 2 + 1 ) · ( π / 2 ) ) = ( ( 2 · ( π / 2 ) ) + ( 1 · ( π / 2 ) ) )
17 6 recni ⊢ π ∈ ℂ
18 2ne0 ⊢ 2 ≠ 0
19 17 13 18 divcan2i ⊢ ( 2 · ( π / 2 ) ) = π
20 15 mullidi ⊢ ( 1 · ( π / 2 ) ) = ( π / 2 )
21 19 20 oveq12i ⊢ ( ( 2 · ( π / 2 ) ) + ( 1 · ( π / 2 ) ) ) = ( π + ( π / 2 ) )
22 12 16 21 3eqtrri ⊢ ( π + ( π / 2 ) ) = ( 3 · ( π / 2 ) )
23 22 breq1i ⊢ ( ( π + ( π / 2 ) ) < 𝐴 ↔ ( 3 · ( π / 2 ) ) < 𝐴 )
24 ltaddsub ⊢ ( ( π ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( π + ( π / 2 ) ) < 𝐴 ↔ π < ( 𝐴 − ( π / 2 ) ) ) )
25 6 2 24 mp3an12 ⊢ ( 𝐴 ∈ ℝ → ( ( π + ( π / 2 ) ) < 𝐴 ↔ π < ( 𝐴 − ( π / 2 ) ) ) )
26 23 25 bitr3id ⊢ ( 𝐴 ∈ ℝ → ( ( 3 · ( π / 2 ) ) < 𝐴 ↔ π < ( 𝐴 − ( π / 2 ) ) ) )
27 ltsubadd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ ( 3 · ( π / 2 ) ) ∈ ℝ ) → ( ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ↔ 𝐴 < ( ( 3 · ( π / 2 ) ) + ( π / 2 ) ) ) )
28 2 3 27 mp3an23 ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ↔ 𝐴 < ( ( 3 · ( π / 2 ) ) + ( π / 2 ) ) ) )
29 df-4 ⊢ 4 = ( 3 + 1 )
30 29 oveq1i ⊢ ( 4 · ( π / 2 ) ) = ( ( 3 + 1 ) · ( π / 2 ) )
31 1 recni ⊢ 3 ∈ ℂ
32 31 14 15 adddiri ⊢ ( ( 3 + 1 ) · ( π / 2 ) ) = ( ( 3 · ( π / 2 ) ) + ( 1 · ( π / 2 ) ) )
33 20 oveq2i ⊢ ( ( 3 · ( π / 2 ) ) + ( 1 · ( π / 2 ) ) ) = ( ( 3 · ( π / 2 ) ) + ( π / 2 ) )
34 30 32 33 3eqtrri ⊢ ( ( 3 · ( π / 2 ) ) + ( π / 2 ) ) = ( 4 · ( π / 2 ) )
35 4cn ⊢ 4 ∈ ℂ
36 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
37 div12 ⊢ ( ( 4 ∈ ℂ ∧ π ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( 4 · ( π / 2 ) ) = ( π · ( 4 / 2 ) ) )
38 35 17 36 37 mp3an ⊢ ( 4 · ( π / 2 ) ) = ( π · ( 4 / 2 ) )
39 4d2e2 ⊢ ( 4 / 2 ) = 2
40 39 oveq2i ⊢ ( π · ( 4 / 2 ) ) = ( π · 2 )
41 17 13 mulcomi ⊢ ( π · 2 ) = ( 2 · π )
42 40 41 eqtri ⊢ ( π · ( 4 / 2 ) ) = ( 2 · π )
43 38 42 eqtri ⊢ ( 4 · ( π / 2 ) ) = ( 2 · π )
44 34 43 eqtri ⊢ ( ( 3 · ( π / 2 ) ) + ( π / 2 ) ) = ( 2 · π )
45 44 breq2i ⊢ ( 𝐴 < ( ( 3 · ( π / 2 ) ) + ( π / 2 ) ) ↔ 𝐴 < ( 2 · π ) )
46 28 45 bitr2di ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < ( 2 · π ) ↔ ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ) )
47 26 46 anbi12d ⊢ ( 𝐴 ∈ ℝ → ( ( ( 3 · ( π / 2 ) ) < 𝐴 ∧ 𝐴 < ( 2 · π ) ) ↔ ( π < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ) ) )
48 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 𝐴 − ( π / 2 ) ) ∈ ℝ )
49 2 48 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( π / 2 ) ) ∈ ℝ )
50 6 rexri ⊢ π ∈ ℝ*
51 elioo2 ⊢ ( ( π ∈ ℝ* ∧ ( 3 · ( π / 2 ) ) ∈ ℝ* ) → ( ( 𝐴 − ( π / 2 ) ) ∈ ( π (,) ( 3 · ( π / 2 ) ) ) ↔ ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ π < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ) ) )
52 50 4 51 mp2an ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ( π (,) ( 3 · ( π / 2 ) ) ) ↔ ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ π < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ) )
53 sincosq3sgn ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ( π (,) ( 3 · ( π / 2 ) ) ) → ( ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
54 52 53 sylbir ⊢ ( ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ π < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ) → ( ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
55 49 54 syl3an1 ⊢ ( ( 𝐴 ∈ ℝ ∧ π < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ) → ( ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
56 55 3expib ⊢ ( 𝐴 ∈ ℝ → ( ( π < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( 3 · ( π / 2 ) ) ) → ( ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ) )
57 47 56 sylbid ⊢ ( 𝐴 ∈ ℝ → ( ( ( 3 · ( π / 2 ) ) < 𝐴 ∧ 𝐴 < ( 2 · π ) ) → ( ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ) )
58 49 resincld ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∈ ℝ )
59 58 lt0neg1d ⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ↔ 0 < - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
60 59 anbi1d ⊢ ( 𝐴 ∈ ℝ → ( ( ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ↔ ( 0 < - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ) )
61 57 60 sylibd ⊢ ( 𝐴 ∈ ℝ → ( ( ( 3 · ( π / 2 ) ) < 𝐴 ∧ 𝐴 < ( 2 · π ) ) → ( 0 < - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ) )
62 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
63 pncan3 ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) = 𝐴 )
64 15 62 63 sylancr ⊢ ( 𝐴 ∈ ℝ → ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) = 𝐴 )
65 64 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ 𝐴 ) )
66 49 recnd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( π / 2 ) ) ∈ ℂ )
67 coshalfpip ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
68 66 67 syl ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
69 65 68 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
70 69 breq2d ⊢ ( 𝐴 ∈ ℝ → ( 0 < ( cos ‘ 𝐴 ) ↔ 0 < - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
71 64 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( sin ‘ 𝐴 ) )
72 sinhalfpip ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ℂ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
73 66 72 syl ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
74 71 73 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
75 74 breq1d ⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ 𝐴 ) < 0 ↔ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
76 70 75 anbi12d ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < ( cos ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 0 ) ↔ ( 0 < - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) ) )
77 61 76 sylibrd ⊢ ( 𝐴 ∈ ℝ → ( ( ( 3 · ( π / 2 ) ) < 𝐴 ∧ 𝐴 < ( 2 · π ) ) → ( 0 < ( cos ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 0 ) ) )
78 77 3impib ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 3 · ( π / 2 ) ) < 𝐴 ∧ 𝐴 < ( 2 · π ) ) → ( 0 < ( cos ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 0 ) )
79 78 ancomd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 3 · ( π / 2 ) ) < 𝐴 ∧ 𝐴 < ( 2 · π ) ) → ( ( sin ‘ 𝐴 ) < 0 ∧ 0 < ( cos ‘ 𝐴 ) ) )
80 10 79 sylbi ⊢ ( 𝐴 ∈ ( ( 3 · ( π / 2 ) ) (,) ( 2 · π ) ) → ( ( sin ‘ 𝐴 ) < 0 ∧ 0 < ( cos ‘ 𝐴 ) ) )