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 ⊢ A ∈ π 3 ⁢ π 2 → sin ⁡ A < 0 ∧ cos ⁡ A < 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 ∈ ℝ * → A ∈ π 3 ⁢ π 2 ↔ A ∈ ℝ ∧ π < A ∧ A < 3 ⁢ π 2
8 5 6 7 syl2an ⊢ π ∈ ℝ ∧ 3 ⁢ π 2 ∈ ℝ → A ∈ π 3 ⁢ π 2 ↔ A ∈ ℝ ∧ π < A ∧ A < 3 ⁢ π 2
9 1 4 8 mp2an ⊢ A ∈ π 3 ⁢ π 2 ↔ A ∈ ℝ ∧ π < A ∧ A < 3 ⁢ π 2
10 pidiv2halves ⊢ π 2 + π 2 = π
11 10 breq1i ⊢ π 2 + π 2 < A ↔ π < A
12 ltaddsub ⊢ π 2 ∈ ℝ ∧ π 2 ∈ ℝ ∧ A ∈ ℝ → π 2 + π 2 < A ↔ π 2 < A − π 2
13 3 3 12 mp3an12 ⊢ A ∈ ℝ → π 2 + π 2 < A ↔ π 2 < A − π 2
14 11 13 bitr3id ⊢ A ∈ ℝ → π < A ↔ π 2 < A − π 2
15 ltsubadd ⊢ A ∈ ℝ ∧ π 2 ∈ ℝ ∧ π ∈ ℝ → A − π 2 < π ↔ A < π + π 2
16 3 1 15 mp3an23 ⊢ A ∈ ℝ → A − π 2 < π ↔ A < π + π 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 ⊢ A < π + π 2 ↔ A < 3 ⁢ π 2
30 16 29 bitr2di ⊢ A ∈ ℝ → A < 3 ⁢ π 2 ↔ A − π 2 < π
31 14 30 anbi12d ⊢ A ∈ ℝ → π < A ∧ A < 3 ⁢ π 2 ↔ π 2 < A − π 2 ∧ A − π 2 < π
32 resubcl ⊢ A ∈ ℝ ∧ π 2 ∈ ℝ → A − π 2 ∈ ℝ
33 3 32 mpan2 ⊢ A ∈ ℝ → A − π 2 ∈ ℝ
34 sincosq2sgn ⊢ A − π 2 ∈ π 2 π → 0 < sin ⁡ A − π 2 ∧ cos ⁡ A − π 2 < 0
35 rexr ⊢ π 2 ∈ ℝ → π 2 ∈ ℝ *
36 elioo2 ⊢ π 2 ∈ ℝ * ∧ π ∈ ℝ * → A − π 2 ∈ π 2 π ↔ A − π 2 ∈ ℝ ∧ π 2 < A − π 2 ∧ A − π 2 < π
37 35 5 36 syl2an ⊢ π 2 ∈ ℝ ∧ π ∈ ℝ → A − π 2 ∈ π 2 π ↔ A − π 2 ∈ ℝ ∧ π 2 < A − π 2 ∧ A − π 2 < π
38 3 1 37 mp2an ⊢ A − π 2 ∈ π 2 π ↔ A − π 2 ∈ ℝ ∧ π 2 < A − π 2 ∧ A − π 2 < π
39 ancom ⊢ 0 < sin ⁡ A − π 2 ∧ cos ⁡ A − π 2 < 0 ↔ cos ⁡ A − π 2 < 0 ∧ 0 < sin ⁡ A − π 2
40 34 38 39 3imtr3i ⊢ A − π 2 ∈ ℝ ∧ π 2 < A − π 2 ∧ A − π 2 < π → cos ⁡ A − π 2 < 0 ∧ 0 < sin ⁡ A − π 2
41 33 40 syl3an1 ⊢ A ∈ ℝ ∧ π 2 < A − π 2 ∧ A − π 2 < π → cos ⁡ A − π 2 < 0 ∧ 0 < sin ⁡ A − π 2
42 41 3expib ⊢ A ∈ ℝ → π 2 < A − π 2 ∧ A − π 2 < π → cos ⁡ A − π 2 < 0 ∧ 0 < sin ⁡ A − π 2
43 31 42 sylbid ⊢ A ∈ ℝ → π < A ∧ A < 3 ⁢ π 2 → cos ⁡ A − π 2 < 0 ∧ 0 < sin ⁡ A − π 2
44 33 resincld ⊢ A ∈ ℝ → sin ⁡ A − π 2 ∈ ℝ
45 44 lt0neg2d ⊢ A ∈ ℝ → 0 < sin ⁡ A − π 2 ↔ − sin ⁡ A − π 2 < 0
46 45 anbi2d ⊢ A ∈ ℝ → cos ⁡ A − π 2 < 0 ∧ 0 < sin ⁡ A − π 2 ↔ cos ⁡ A − π 2 < 0 ∧ − sin ⁡ A − π 2 < 0
47 43 46 sylibd ⊢ A ∈ ℝ → π < A ∧ A < 3 ⁢ π 2 → cos ⁡ A − π 2 < 0 ∧ − sin ⁡ A − π 2 < 0
48 recn ⊢ A ∈ ℝ → A ∈ ℂ
49 pncan3 ⊢ π 2 ∈ ℂ ∧ A ∈ ℂ → π 2 + A - π 2 = A
50 21 48 49 sylancr ⊢ A ∈ ℝ → π 2 + A - π 2 = A
51 50 fveq2d ⊢ A ∈ ℝ → sin ⁡ π 2 + A - π 2 = sin ⁡ A
52 33 recnd ⊢ A ∈ ℝ → A − π 2 ∈ ℂ
53 sinhalfpip ⊢ A − π 2 ∈ ℂ → sin ⁡ π 2 + A - π 2 = cos ⁡ A − π 2
54 52 53 syl ⊢ A ∈ ℝ → sin ⁡ π 2 + A - π 2 = cos ⁡ A − π 2
55 51 54 eqtr3d ⊢ A ∈ ℝ → sin ⁡ A = cos ⁡ A − π 2
56 55 breq1d ⊢ A ∈ ℝ → sin ⁡ A < 0 ↔ cos ⁡ A − π 2 < 0
57 50 fveq2d ⊢ A ∈ ℝ → cos ⁡ π 2 + A - π 2 = cos ⁡ A
58 coshalfpip ⊢ A − π 2 ∈ ℂ → cos ⁡ π 2 + A - π 2 = − sin ⁡ A − π 2
59 52 58 syl ⊢ A ∈ ℝ → cos ⁡ π 2 + A - π 2 = − sin ⁡ A − π 2
60 57 59 eqtr3d ⊢ A ∈ ℝ → cos ⁡ A = − sin ⁡ A − π 2
61 60 breq1d ⊢ A ∈ ℝ → cos ⁡ A < 0 ↔ − sin ⁡ A − π 2 < 0
62 56 61 anbi12d ⊢ A ∈ ℝ → sin ⁡ A < 0 ∧ cos ⁡ A < 0 ↔ cos ⁡ A − π 2 < 0 ∧ − sin ⁡ A − π 2 < 0
63 47 62 sylibrd ⊢ A ∈ ℝ → π < A ∧ A < 3 ⁢ π 2 → sin ⁡ A < 0 ∧ cos ⁡ A < 0
64 63 3impib ⊢ A ∈ ℝ ∧ π < A ∧ A < 3 ⁢ π 2 → sin ⁡ A < 0 ∧ cos ⁡ A < 0
65 9 64 sylbi ⊢ A ∈ π 3 ⁢ π 2 → sin ⁡ A < 0 ∧ cos ⁡ A < 0