Theorem 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	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → ( sin ‘ 𝐴 ) < 0 )

Proof

Step	Hyp	Ref	Expression
1		elioore	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → 𝐴 ∈ ℝ )
2		picn	⊢ π ∈ ℂ
3	2	addid2i	⊢ ( 0 + π ) = π
4	3	eqcomi	⊢ π = ( 0 + π )
5	2	2timesi	⊢ ( 2 · π ) = ( π + π )
6	4 5	oveq12i	⊢ ( π (,) ( 2 · π ) ) = ( ( 0 + π ) (,) ( π + π ) )
7	6	eleq2i	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) ↔ 𝐴 ∈ ( ( 0 + π ) (,) ( π + π ) ) )
8		pire	⊢ π ∈ ℝ
9		0re	⊢ 0 ∈ ℝ
10		iooshf	⊢ ( ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ) ∧ ( 0 ∈ ℝ ∧ π ∈ ℝ ) ) → ( ( 𝐴 − π ) ∈ ( 0 (,) π ) ↔ 𝐴 ∈ ( ( 0 + π ) (,) ( π + π ) ) ) )
11	9 8 10	mpanr12	⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ) → ( ( 𝐴 − π ) ∈ ( 0 (,) π ) ↔ 𝐴 ∈ ( ( 0 + π ) (,) ( π + π ) ) ) )
12	8 11	mpan2	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − π ) ∈ ( 0 (,) π ) ↔ 𝐴 ∈ ( ( 0 + π ) (,) ( π + π ) ) ) )
13	7 12	bitr4id	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ( π (,) ( 2 · π ) ) ↔ ( 𝐴 − π ) ∈ ( 0 (,) π ) ) )
14	1 13	syl	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → ( 𝐴 ∈ ( π (,) ( 2 · π ) ) ↔ ( 𝐴 − π ) ∈ ( 0 (,) π ) ) )
15	14	ibi	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → ( 𝐴 − π ) ∈ ( 0 (,) π ) )
16		sinq12gt0	⊢ ( ( 𝐴 − π ) ∈ ( 0 (,) π ) → 0 < ( sin ‘ ( 𝐴 − π ) ) )
17	15 16	syl	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → 0 < ( sin ‘ ( 𝐴 − π ) ) )
18	1	recnd	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → 𝐴 ∈ ℂ )
19		sinmpi	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 𝐴 − π ) ) = - ( sin ‘ 𝐴 ) )
20	18 19	syl	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → ( sin ‘ ( 𝐴 − π ) ) = - ( sin ‘ 𝐴 ) )
21	17 20	breqtrd	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → 0 < - ( sin ‘ 𝐴 ) )
22	1	resincld	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → ( sin ‘ 𝐴 ) ∈ ℝ )
23	22	lt0neg1d	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → ( ( sin ‘ 𝐴 ) < 0 ↔ 0 < - ( sin ‘ 𝐴 ) ) )
24	21 23	mpbird	⊢ ( 𝐴 ∈ ( π (,) ( 2 · π ) ) → ( sin ‘ 𝐴 ) < 0 )