sincosq2sgn

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

		Ref	Expression
	Assertion	sincosq2sgn	$⊢ A \in (\frac{π}{2}, π) \to (0 < \sin A \land \cos A < 0)$

Proof

Step	Hyp	Ref	Expression
1		halfpire	$⊢ \frac{π}{2} \in ℝ$
2		pire	$⊢ π \in ℝ$
3		rexr	$⊢ \frac{π}{2} \in ℝ \to \frac{π}{2} \in ℝ^{*}$
4		rexr	$⊢ π \in ℝ \to π \in ℝ^{*}$
5		elioo2	$⊢ (\frac{π}{2} \in ℝ^{} \land π \in ℝ^{}) \to (A \in (\frac{π}{2}, π) \leftrightarrow (A \in ℝ \land \frac{π}{2} < A \land A < π))$
6	3 4 5	syl2an	$⊢ (\frac{π}{2} \in ℝ \land π \in ℝ) \to (A \in (\frac{π}{2}, π) \leftrightarrow (A \in ℝ \land \frac{π}{2} < A \land A < π))$
7	1 2 6	mp2an	$⊢ A \in (\frac{π}{2}, π) \leftrightarrow (A \in ℝ \land \frac{π}{2} < A \land A < π)$
8		resubcl	$⊢ (A \in ℝ \land \frac{π}{2} \in ℝ) \to A - (\frac{π}{2}) \in ℝ$
9	1 8	mpan2	$⊢ A \in ℝ \to A - (\frac{π}{2}) \in ℝ$
10		0xr	$⊢ 0 \in ℝ^{*}$
11	1	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
12		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (A - (\frac{π}{2}) \in (0, \frac{π}{2}) \leftrightarrow (A - (\frac{π}{2}) \in ℝ \land 0 < A - (\frac{π}{2}) \land A - (\frac{π}{2}) < \frac{π}{2}))$
13	10 11 12	mp2an	$⊢ A - (\frac{π}{2}) \in (0, \frac{π}{2}) \leftrightarrow (A - (\frac{π}{2}) \in ℝ \land 0 < A - (\frac{π}{2}) \land A - (\frac{π}{2}) < \frac{π}{2})$
14		sincosq1sgn	$⊢ A - (\frac{π}{2}) \in (0, \frac{π}{2}) \to (0 < \sin (A - (\frac{π}{2})) \land 0 < \cos (A - (\frac{π}{2})))$
15	13 14	sylbir	$⊢ (A - (\frac{π}{2}) \in ℝ \land 0 < A - (\frac{π}{2}) \land A - (\frac{π}{2}) < \frac{π}{2}) \to (0 < \sin (A - (\frac{π}{2})) \land 0 < \cos (A - (\frac{π}{2})))$
16	9 15	syl3an1	$⊢ (A \in ℝ \land 0 < A - (\frac{π}{2}) \land A - (\frac{π}{2}) < \frac{π}{2}) \to (0 < \sin (A - (\frac{π}{2})) \land 0 < \cos (A - (\frac{π}{2})))$
17	16	3expib	$⊢ A \in ℝ \to ((0 < A - (\frac{π}{2}) \land A - (\frac{π}{2}) < \frac{π}{2}) \to (0 < \sin (A - (\frac{π}{2})) \land 0 < \cos (A - (\frac{π}{2}))))$
18		0re	$⊢ 0 \in ℝ$
19		ltsub13	$⊢ (0 \in ℝ \land A \in ℝ \land \frac{π}{2} \in ℝ) \to (0 < A - (\frac{π}{2}) \leftrightarrow \frac{π}{2} < A - 0)$
20	18 1 19	mp3an13	$⊢ A \in ℝ \to (0 < A - (\frac{π}{2}) \leftrightarrow \frac{π}{2} < A - 0)$
21		recn	$⊢ A \in ℝ \to A \in ℂ$
22	21	subid1d	$⊢ A \in ℝ \to A - 0 = A$
23	22	breq2d	$⊢ A \in ℝ \to (\frac{π}{2} < A - 0 \leftrightarrow \frac{π}{2} < A)$
24	20 23	bitrd	$⊢ A \in ℝ \to (0 < A - (\frac{π}{2}) \leftrightarrow \frac{π}{2} < A)$
25		ltsubadd	$⊢ (A \in ℝ \land \frac{π}{2} \in ℝ \land \frac{π}{2} \in ℝ) \to (A - (\frac{π}{2}) < \frac{π}{2} \leftrightarrow A < (\frac{π}{2}) + (\frac{π}{2}))$
26	1 1 25	mp3an23	$⊢ A \in ℝ \to (A - (\frac{π}{2}) < \frac{π}{2} \leftrightarrow A < (\frac{π}{2}) + (\frac{π}{2}))$
27		pidiv2halves	$⊢ (\frac{π}{2}) + (\frac{π}{2}) = π$
28	27	breq2i	$⊢ A < (\frac{π}{2}) + (\frac{π}{2}) \leftrightarrow A < π$
29	26 28	bitrdi	$⊢ A \in ℝ \to (A - (\frac{π}{2}) < \frac{π}{2} \leftrightarrow A < π)$
30	24 29	anbi12d	$⊢ A \in ℝ \to ((0 < A - (\frac{π}{2}) \land A - (\frac{π}{2}) < \frac{π}{2}) \leftrightarrow (\frac{π}{2} < A \land A < π))$
31	9	resincld	$⊢ A \in ℝ \to \sin (A - (\frac{π}{2})) \in ℝ$
32	31	lt0neg2d	$⊢ A \in ℝ \to (0 < \sin (A - (\frac{π}{2})) \leftrightarrow - \sin (A - (\frac{π}{2})) < 0)$
33	32	anbi1d	$⊢ A \in ℝ \to ((0 < \sin (A - (\frac{π}{2})) \land 0 < \cos (A - (\frac{π}{2}))) \leftrightarrow (- \sin (A - (\frac{π}{2})) < 0 \land 0 < \cos (A - (\frac{π}{2}))))$
34	17 30 33	3imtr3d	$⊢ A \in ℝ \to ((\frac{π}{2} < A \land A < π) \to (- \sin (A - (\frac{π}{2})) < 0 \land 0 < \cos (A - (\frac{π}{2}))))$
35	1	recni	$⊢ \frac{π}{2} \in ℂ$
36		pncan3	$⊢ (\frac{π}{2} \in ℂ \land A \in ℂ) \to (\frac{π}{2}) + A - (\frac{π}{2}) = A$
37	35 21 36	sylancr	$⊢ A \in ℝ \to (\frac{π}{2}) + A - (\frac{π}{2}) = A$
38	37	fveq2d	$⊢ A \in ℝ \to \cos ((\frac{π}{2}) + A - (\frac{π}{2})) = \cos A$
39	9	recnd	$⊢ A \in ℝ \to A - (\frac{π}{2}) \in ℂ$
40		coshalfpip	$⊢ A - (\frac{π}{2}) \in ℂ \to \cos ((\frac{π}{2}) + A - (\frac{π}{2})) = - \sin (A - (\frac{π}{2}))$
41	39 40	syl	$⊢ A \in ℝ \to \cos ((\frac{π}{2}) + A - (\frac{π}{2})) = - \sin (A - (\frac{π}{2}))$
42	38 41	eqtr3d	$⊢ A \in ℝ \to \cos A = - \sin (A - (\frac{π}{2}))$
43	42	breq1d	$⊢ A \in ℝ \to (\cos A < 0 \leftrightarrow - \sin (A - (\frac{π}{2})) < 0)$
44	37	fveq2d	$⊢ A \in ℝ \to \sin ((\frac{π}{2}) + A - (\frac{π}{2})) = \sin A$
45		sinhalfpip	$⊢ A - (\frac{π}{2}) \in ℂ \to \sin ((\frac{π}{2}) + A - (\frac{π}{2})) = \cos (A - (\frac{π}{2}))$
46	39 45	syl	$⊢ A \in ℝ \to \sin ((\frac{π}{2}) + A - (\frac{π}{2})) = \cos (A - (\frac{π}{2}))$
47	44 46	eqtr3d	$⊢ A \in ℝ \to \sin A = \cos (A - (\frac{π}{2}))$
48	47	breq2d	$⊢ A \in ℝ \to (0 < \sin A \leftrightarrow 0 < \cos (A - (\frac{π}{2})))$
49	43 48	anbi12d	$⊢ A \in ℝ \to ((\cos A < 0 \land 0 < \sin A) \leftrightarrow (- \sin (A - (\frac{π}{2})) < 0 \land 0 < \cos (A - (\frac{π}{2}))))$
50	34 49	sylibrd	$⊢ A \in ℝ \to ((\frac{π}{2} < A \land A < π) \to (\cos A < 0 \land 0 < \sin A))$
51	50	3impib	$⊢ (A \in ℝ \land \frac{π}{2} < A \land A < π) \to (\cos A < 0 \land 0 < \sin A)$
52	51	ancomd	$⊢ (A \in ℝ \land \frac{π}{2} < A \land A < π) \to (0 < \sin A \land \cos A < 0)$
53	7 52	sylbi	$⊢ A \in (\frac{π}{2}, π) \to (0 < \sin A \land \cos A < 0)$

Metamath Proof Explorer

Theorem sincosq2sgn

Proof