sinltx

Description: The sine of a positive real number is less than its argument. (Contributed by Mario Carneiro, 29-Jul-2014)

		Ref	Expression
	Assertion	sinltx	$⊢ A \in ℝ^{+} \to \sin A < A$

Step	Hyp	Ref	Expression
1		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
2	1	adantr	$⊢ (A \in ℝ^{+} \land 1 < A) \to A \in ℝ$
3	2	resincld	$⊢ (A \in ℝ^{+} \land 1 < A) \to \sin A \in ℝ$
4		1red	$⊢ (A \in ℝ^{+} \land 1 < A) \to 1 \in ℝ$
5		sinbnd	$⊢ A \in ℝ \to (- 1 \leq \sin A \land \sin A \leq 1)$
6	5	simprd	$⊢ A \in ℝ \to \sin A \leq 1$
7	1 6	syl	$⊢ A \in ℝ^{+} \to \sin A \leq 1$
8	7	adantr	$⊢ (A \in ℝ^{+} \land 1 < A) \to \sin A \leq 1$
9		simpr	$⊢ (A \in ℝ^{+} \land 1 < A) \to 1 < A$
10	3 4 2 8 9	lelttrd	$⊢ (A \in ℝ^{+} \land 1 < A) \to \sin A < A$
11		df-3an	$⊢ (A \in ℝ \land 0 < A \land A \leq 1) \leftrightarrow ((A \in ℝ \land 0 < A) \land A \leq 1)$
12		0xr	$⊢ 0 \in ℝ^{*}$
13		1re	$⊢ 1 \in ℝ$
14		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (A \in (0, 1] \leftrightarrow (A \in ℝ \land 0 < A \land A \leq 1))$
15	12 13 14	mp2an	$⊢ A \in (0, 1] \leftrightarrow (A \in ℝ \land 0 < A \land A \leq 1)$
16		elrp	$⊢ A \in ℝ^{+} \leftrightarrow (A \in ℝ \land 0 < A)$
17	16	anbi1i	$⊢ (A \in ℝ^{+} \land A \leq 1) \leftrightarrow ((A \in ℝ \land 0 < A) \land A \leq 1)$
18	11 15 17	3bitr4i	$⊢ A \in (0, 1] \leftrightarrow (A \in ℝ^{+} \land A \leq 1)$
19		sin01bnd	$⊢ A \in (0, 1] \to (A - (\frac{A^{3}}{3}) < \sin A \land \sin A < A)$
20	19	simprd	$⊢ A \in (0, 1] \to \sin A < A$
21	18 20	sylbir	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \sin A < A$
22		1red	$⊢ A \in ℝ^{+} \to 1 \in ℝ$
23	10 21 22 1	ltlecasei	$⊢ A \in ℝ^{+} \to \sin A < A$

Metamath Proof Explorer