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 mullidi ⊢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