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 ( 𝐴 ∈ ( 0 [,] π ) → 0 ≤ ( sin ‘ 𝐴 ) )

Proof

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