Metamath Proof Explorer

Theorem sinq12ge0

Description: The sine of a number between 0 and _pi is nonnegative. (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Assertion sinq12ge0 ⊢ A ∈ 0 π → 0 ≤ sin ⁡ A

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 pire ⊢ π ∈ ℝ
3 1 2 elicc2i ⊢ A ∈ 0 π ↔ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ π
4 3 simp1bi ⊢ A ∈ 0 π → A ∈ ℝ
5 rexr ⊢ 0 ∈ ℝ → 0 ∈ ℝ *
6 rexr ⊢ π ∈ ℝ → π ∈ ℝ *
7 elioo2 ⊢ 0 ∈ ℝ * ∧ π ∈ ℝ * → A ∈ 0 π ↔ A ∈ ℝ ∧ 0 < A ∧ A < π
8 5 6 7 syl2an ⊢ 0 ∈ ℝ ∧ π ∈ ℝ → A ∈ 0 π ↔ A ∈ ℝ ∧ 0 < A ∧ A < π
9 1 2 8 mp2an ⊢ A ∈ 0 π ↔ A ∈ ℝ ∧ 0 < A ∧ A < π
10 sinq12gt0 ⊢ A ∈ 0 π → 0 < sin ⁡ A
11 9 10 sylbir ⊢ A ∈ ℝ ∧ 0 < A ∧ A < π → 0 < sin ⁡ A
12 11 3expib ⊢ A ∈ ℝ → 0 < A ∧ A < π → 0 < sin ⁡ A
13 4 12 syl ⊢ A ∈ 0 π → 0 < A ∧ A < π → 0 < sin ⁡ A
14 4 resincld ⊢ A ∈ 0 π → sin ⁡ A ∈ ℝ
15 ltle ⊢ 0 ∈ ℝ ∧ sin ⁡ A ∈ ℝ → 0 < sin ⁡ A → 0 ≤ sin ⁡ A
16 1 14 15 sylancr ⊢ A ∈ 0 π → 0 < sin ⁡ A → 0 ≤ sin ⁡ A
17 13 16 syld ⊢ A ∈ 0 π → 0 < A ∧ A < π → 0 ≤ sin ⁡ A
18 17 expd ⊢ A ∈ 0 π → 0 < A → A < π → 0 ≤ sin ⁡ A
19 0le0 ⊢ 0 ≤ 0
20 sin0 ⊢ sin ⁡ 0 = 0
21 19 20 breqtrri ⊢ 0 ≤ sin ⁡ 0
22 fveq2 ⊢ 0 = A → sin ⁡ 0 = sin ⁡ A
23 21 22 breqtrid ⊢ 0 = A → 0 ≤ sin ⁡ A
24 23 a1i13 ⊢ A ∈ 0 π → 0 = A → A < π → 0 ≤ sin ⁡ A
25 3 simp2bi ⊢ A ∈ 0 π → 0 ≤ A
26 leloe ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 ≤ A ↔ 0 < A ∨ 0 = A
27 1 4 26 sylancr ⊢ A ∈ 0 π → 0 ≤ A ↔ 0 < A ∨ 0 = A
28 25 27 mpbid ⊢ A ∈ 0 π → 0 < A ∨ 0 = A
29 18 24 28 mpjaod ⊢ A ∈ 0 π → A < π → 0 ≤ sin ⁡ A
30 sinpi ⊢ sin ⁡ π = 0
31 19 30 breqtrri ⊢ 0 ≤ sin ⁡ π
32 fveq2 ⊢ A = π → sin ⁡ A = sin ⁡ π
33 31 32 breqtrrid ⊢ A = π → 0 ≤ sin ⁡ A
34 33 a1i ⊢ A ∈ 0 π → A = π → 0 ≤ sin ⁡ A
35 3 simp3bi ⊢ A ∈ 0 π → A ≤ π
36 leloe ⊢ A ∈ ℝ ∧ π ∈ ℝ → A ≤ π ↔ A < π ∨ A = π
37 4 2 36 sylancl ⊢ A ∈ 0 π → A ≤ π ↔ A < π ∨ A = π
38 35 37 mpbid ⊢ A ∈ 0 π → A < π ∨ A = π
39 29 34 38 mpjaod ⊢ A ∈ 0 π → 0 ≤ sin ⁡ A