# Metamath Proof Explorer

## Theorem sincosq1lem

Description: Lemma for sincosq1sgn . (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion sincosq1lem ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\to 0<\mathrm{sin}{A}$

### Proof

Step Hyp Ref Expression
1 halfpire ${⊢}\frac{\mathrm{\pi }}{2}\in ℝ$
2 ltle ${⊢}\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\right)\to \left({A}<\frac{\mathrm{\pi }}{2}\to {A}\le \frac{\mathrm{\pi }}{2}\right)$
3 1 2 mpan2 ${⊢}{A}\in ℝ\to \left({A}<\frac{\mathrm{\pi }}{2}\to {A}\le \frac{\mathrm{\pi }}{2}\right)$
4 pire ${⊢}\mathrm{\pi }\in ℝ$
5 4re ${⊢}4\in ℝ$
6 pigt2lt4 ${⊢}\left(2<\mathrm{\pi }\wedge \mathrm{\pi }<4\right)$
7 6 simpri ${⊢}\mathrm{\pi }<4$
8 4 5 7 ltleii ${⊢}\mathrm{\pi }\le 4$
9 2re ${⊢}2\in ℝ$
10 2pos ${⊢}0<2$
11 9 10 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
12 ledivmul ${⊢}\left(\mathrm{\pi }\in ℝ\wedge 2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{\mathrm{\pi }}{2}\le 2↔\mathrm{\pi }\le 2\cdot 2\right)$
13 4 9 11 12 mp3an ${⊢}\frac{\mathrm{\pi }}{2}\le 2↔\mathrm{\pi }\le 2\cdot 2$
14 2t2e4 ${⊢}2\cdot 2=4$
15 14 breq2i ${⊢}\mathrm{\pi }\le 2\cdot 2↔\mathrm{\pi }\le 4$
16 13 15 bitri ${⊢}\frac{\mathrm{\pi }}{2}\le 2↔\mathrm{\pi }\le 4$
17 8 16 mpbir ${⊢}\frac{\mathrm{\pi }}{2}\le 2$
18 letr ${⊢}\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\wedge 2\in ℝ\right)\to \left(\left({A}\le \frac{\mathrm{\pi }}{2}\wedge \frac{\mathrm{\pi }}{2}\le 2\right)\to {A}\le 2\right)$
19 1 9 18 mp3an23 ${⊢}{A}\in ℝ\to \left(\left({A}\le \frac{\mathrm{\pi }}{2}\wedge \frac{\mathrm{\pi }}{2}\le 2\right)\to {A}\le 2\right)$
20 17 19 mpan2i ${⊢}{A}\in ℝ\to \left({A}\le \frac{\mathrm{\pi }}{2}\to {A}\le 2\right)$
21 3 20 syld ${⊢}{A}\in ℝ\to \left({A}<\frac{\mathrm{\pi }}{2}\to {A}\le 2\right)$
22 21 adantr ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left({A}<\frac{\mathrm{\pi }}{2}\to {A}\le 2\right)$
23 22 3impia ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\to {A}\le 2$
24 0xr ${⊢}0\in {ℝ}^{*}$
25 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)$
26 24 9 25 mp2an ${⊢}{A}\in \left(0,2\right]↔\left({A}\in ℝ\wedge 0<{A}\wedge {A}\le 2\right)$
27 sin02gt0 ${⊢}{A}\in \left(0,2\right]\to 0<\mathrm{sin}{A}$
28 26 27 sylbir ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}\le 2\right)\to 0<\mathrm{sin}{A}$
29 23 28 syld3an3 ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\to 0<\mathrm{sin}{A}$