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