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 ⊢ A ∈ π 2 ⁢ π → sin ⁡ A < 0

Proof

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