Theorem 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$$

Proof

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