sinq34lt0t

Description: The sine of a number strictly between _pi and 2 x. _pi is negative. (Contributed by NM, 17-Aug-2008)

		Ref	Expression
	Assertion	sinq34lt0t	$⊢ A \in (π, 2 π) \to \sin A < 0$

Step	Hyp	Ref	Expression
1		elioore	$⊢ A \in (π, 2 π) \to A \in ℝ$
2		picn	$⊢ π \in ℂ$
3	2	addlidi	$⊢ 0 + π = π$
4	3	eqcomi	$⊢ π = 0 + π$
5	2	2timesi	$⊢ 2 π = π + π$
6	4 5	oveq12i	$⊢ (π, 2 π) = (0 + π, π + π)$
7	6	eleq2i	$⊢ A \in (π, 2 π) \leftrightarrow A \in (0 + π, π + π)$
8		pire	$⊢ π \in ℝ$
9		0re	$⊢ 0 \in ℝ$
10		iooshf	$⊢ ((A \in ℝ \land π \in ℝ) \land (0 \in ℝ \land π \in ℝ)) \to (A - π \in (0, π) \leftrightarrow A \in (0 + π, π + π))$
11	9 8 10	mpanr12	$⊢ (A \in ℝ \land π \in ℝ) \to (A - π \in (0, π) \leftrightarrow A \in (0 + π, π + π))$
12	8 11	mpan2	$⊢ A \in ℝ \to (A - π \in (0, π) \leftrightarrow A \in (0 + π, π + π))$
13	7 12	bitr4id	$⊢ A \in ℝ \to (A \in (π, 2 π) \leftrightarrow A - π \in (0, π))$
14	1 13	syl	$⊢ A \in (π, 2 π) \to (A \in (π, 2 π) \leftrightarrow A - π \in (0, π))$
15	14	ibi	$⊢ A \in (π, 2 π) \to A - π \in (0, π)$
16		sinq12gt0	$⊢ A - π \in (0, π) \to 0 < \sin (A - π)$
17	15 16	syl	$⊢ A \in (π, 2 π) \to 0 < \sin (A - π)$
18	1	recnd	$⊢ A \in (π, 2 π) \to A \in ℂ$
19		sinmpi	$⊢ A \in ℂ \to \sin (A - π) = - \sin A$
20	18 19	syl	$⊢ A \in (π, 2 π) \to \sin (A - π) = - \sin A$
21	17 20	breqtrd	$⊢ A \in (π, 2 π) \to 0 < - \sin A$
22	1	resincld	$⊢ A \in (π, 2 π) \to \sin A \in ℝ$
23	22	lt0neg1d	$⊢ A \in (π, 2 π) \to (\sin A < 0 \leftrightarrow 0 < - \sin A)$
24	21 23	mpbird	$⊢ A \in (π, 2 π) \to \sin A < 0$

Metamath Proof Explorer