# Metamath Proof Explorer

## Theorem sin02gt0

Description: The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008)

Ref Expression
Assertion sin02gt0 ${⊢}{A}\in \left(0,2\right]\to 0<\mathrm{sin}{A}$

### Proof

Step Hyp Ref Expression
1 0xr ${⊢}0\in {ℝ}^{*}$
2 2re ${⊢}2\in ℝ$
3 elioc2 ${⊢}\left(0\in {ℝ}^{*}\wedge 2\in ℝ\right)\to \left({A}\in \left(0,2\right]↔\left({A}\in ℝ\wedge 0<{A}\wedge {A}\le 2\right)\right)$
4 1 2 3 mp2an ${⊢}{A}\in \left(0,2\right]↔\left({A}\in ℝ\wedge 0<{A}\wedge {A}\le 2\right)$
5 rehalfcl ${⊢}{A}\in ℝ\to \frac{{A}}{2}\in ℝ$
6 5 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}\le 2\right)\to \frac{{A}}{2}\in ℝ$
7 4 6 sylbi ${⊢}{A}\in \left(0,2\right]\to \frac{{A}}{2}\in ℝ$
8 resincl ${⊢}\frac{{A}}{2}\in ℝ\to \mathrm{sin}\left(\frac{{A}}{2}\right)\in ℝ$
9 recoscl ${⊢}\frac{{A}}{2}\in ℝ\to \mathrm{cos}\left(\frac{{A}}{2}\right)\in ℝ$
10 8 9 remulcld ${⊢}\frac{{A}}{2}\in ℝ\to \mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\in ℝ$
11 7 10 syl ${⊢}{A}\in \left(0,2\right]\to \mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\in ℝ$
12 2pos ${⊢}0<2$
13 divgt0 ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to 0<\frac{{A}}{2}$
14 2 12 13 mpanr12 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0<\frac{{A}}{2}$
15 14 3adant3 ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}\le 2\right)\to 0<\frac{{A}}{2}$
16 2 12 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
17 lediv1 ${⊢}\left({A}\in ℝ\wedge 2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left({A}\le 2↔\frac{{A}}{2}\le \frac{2}{2}\right)$
18 2 16 17 mp3an23 ${⊢}{A}\in ℝ\to \left({A}\le 2↔\frac{{A}}{2}\le \frac{2}{2}\right)$
19 18 biimpa ${⊢}\left({A}\in ℝ\wedge {A}\le 2\right)\to \frac{{A}}{2}\le \frac{2}{2}$
20 2div2e1 ${⊢}\frac{2}{2}=1$
21 19 20 breqtrdi ${⊢}\left({A}\in ℝ\wedge {A}\le 2\right)\to \frac{{A}}{2}\le 1$
22 21 3adant2 ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}\le 2\right)\to \frac{{A}}{2}\le 1$
23 6 15 22 3jca ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}\le 2\right)\to \left(\frac{{A}}{2}\in ℝ\wedge 0<\frac{{A}}{2}\wedge \frac{{A}}{2}\le 1\right)$
24 1re ${⊢}1\in ℝ$
25 elioc2 ${⊢}\left(0\in {ℝ}^{*}\wedge 1\in ℝ\right)\to \left(\frac{{A}}{2}\in \left(0,1\right]↔\left(\frac{{A}}{2}\in ℝ\wedge 0<\frac{{A}}{2}\wedge \frac{{A}}{2}\le 1\right)\right)$
26 1 24 25 mp2an ${⊢}\frac{{A}}{2}\in \left(0,1\right]↔\left(\frac{{A}}{2}\in ℝ\wedge 0<\frac{{A}}{2}\wedge \frac{{A}}{2}\le 1\right)$
27 23 4 26 3imtr4i ${⊢}{A}\in \left(0,2\right]\to \frac{{A}}{2}\in \left(0,1\right]$
28 sin01gt0 ${⊢}\frac{{A}}{2}\in \left(0,1\right]\to 0<\mathrm{sin}\left(\frac{{A}}{2}\right)$
29 27 28 syl ${⊢}{A}\in \left(0,2\right]\to 0<\mathrm{sin}\left(\frac{{A}}{2}\right)$
30 cos01gt0 ${⊢}\frac{{A}}{2}\in \left(0,1\right]\to 0<\mathrm{cos}\left(\frac{{A}}{2}\right)$
31 27 30 syl ${⊢}{A}\in \left(0,2\right]\to 0<\mathrm{cos}\left(\frac{{A}}{2}\right)$
32 axmulgt0 ${⊢}\left(\mathrm{sin}\left(\frac{{A}}{2}\right)\in ℝ\wedge \mathrm{cos}\left(\frac{{A}}{2}\right)\in ℝ\right)\to \left(\left(0<\mathrm{sin}\left(\frac{{A}}{2}\right)\wedge 0<\mathrm{cos}\left(\frac{{A}}{2}\right)\right)\to 0<\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\right)$
33 8 9 32 syl2anc ${⊢}\frac{{A}}{2}\in ℝ\to \left(\left(0<\mathrm{sin}\left(\frac{{A}}{2}\right)\wedge 0<\mathrm{cos}\left(\frac{{A}}{2}\right)\right)\to 0<\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\right)$
34 7 33 syl ${⊢}{A}\in \left(0,2\right]\to \left(\left(0<\mathrm{sin}\left(\frac{{A}}{2}\right)\wedge 0<\mathrm{cos}\left(\frac{{A}}{2}\right)\right)\to 0<\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\right)$
35 29 31 34 mp2and ${⊢}{A}\in \left(0,2\right]\to 0<\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)$
36 axmulgt0 ${⊢}\left(2\in ℝ\wedge \mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\in ℝ\right)\to \left(\left(0<2\wedge 0<\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\right)\to 0<2\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\right)$
37 2 36 mpan ${⊢}\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\in ℝ\to \left(\left(0<2\wedge 0<\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\right)\to 0<2\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\right)$
38 12 37 mpani ${⊢}\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\in ℝ\to \left(0<\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\to 0<2\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)\right)$
39 11 35 38 sylc ${⊢}{A}\in \left(0,2\right]\to 0<2\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)$
40 7 recnd ${⊢}{A}\in \left(0,2\right]\to \frac{{A}}{2}\in ℂ$
41 sin2t ${⊢}\frac{{A}}{2}\in ℂ\to \mathrm{sin}2\left(\frac{{A}}{2}\right)=2\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)$
42 40 41 syl ${⊢}{A}\in \left(0,2\right]\to \mathrm{sin}2\left(\frac{{A}}{2}\right)=2\mathrm{sin}\left(\frac{{A}}{2}\right)\mathrm{cos}\left(\frac{{A}}{2}\right)$
43 39 42 breqtrrd ${⊢}{A}\in \left(0,2\right]\to 0<\mathrm{sin}2\left(\frac{{A}}{2}\right)$
44 4 simp1bi ${⊢}{A}\in \left(0,2\right]\to {A}\in ℝ$
45 44 recnd ${⊢}{A}\in \left(0,2\right]\to {A}\in ℂ$
46 2cn ${⊢}2\in ℂ$
47 2ne0 ${⊢}2\ne 0$
48 divcan2 ${⊢}\left({A}\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to 2\left(\frac{{A}}{2}\right)={A}$
49 46 47 48 mp3an23 ${⊢}{A}\in ℂ\to 2\left(\frac{{A}}{2}\right)={A}$
50 45 49 syl ${⊢}{A}\in \left(0,2\right]\to 2\left(\frac{{A}}{2}\right)={A}$
51 50 fveq2d ${⊢}{A}\in \left(0,2\right]\to \mathrm{sin}2\left(\frac{{A}}{2}\right)=\mathrm{sin}{A}$
52 43 51 breqtrd ${⊢}{A}\in \left(0,2\right]\to 0<\mathrm{sin}{A}$