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	$⊢ A \in (3 (\frac{π}{2}), 2 π) \to (\sin A < 0 \land 0 < \cos A)$

Proof

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

Metamath Proof Explorer

Theorem sincosq4sgn

Proof