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 pire ⊢ π ∈ ℝ
3 0re ⊢ 0 ∈ ℝ
4 iooshf ⊢ A ∈ ℝ ∧ π ∈ ℝ ∧ 0 ∈ ℝ ∧ π ∈ ℝ → A − π ∈ 0 π ↔ A ∈ 0 + π π + π
5 3 2 4 mpanr12 ⊢ A ∈ ℝ ∧ π ∈ ℝ → A − π ∈ 0 π ↔ A ∈ 0 + π π + π
6 2 5 mpan2 ⊢ A ∈ ℝ → A − π ∈ 0 π ↔ A ∈ 0 + π π + π
7 picn ⊢ π ∈ ℂ
8 7 addid2i ⊢ 0 + π = π
9 8 eqcomi ⊢ π = 0 + π
10 7 2timesi ⊢ 2 ⁢ π = π + π
11 9 10 oveq12i ⊢ π 2 ⁢ π = 0 + π π + π
12 11 eleq2i ⊢ A ∈ π 2 ⁢ π ↔ A ∈ 0 + π π + π
13 6 12 syl6rbbr ⊢ 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