sincosq1lem

		Ref	Expression
	Assertion	sincosq1lem	$⊢ (A \in ℝ \land 0 < A \land A < \frac{π}{2}) \to 0 < \sin A$

Proof

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

Metamath Proof Explorer

Theorem sincosq1lem

Proof