This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 addlidi ⊢ ( 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 )