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 e. RR+ -> ( sin ` A ) < A )

Proof

Step	Hyp	Ref	Expression
1		rpre	|- ( A e. RR+ -> A e. RR )
2	1	adantr	|- ( ( A e. RR+ /\ 1 < A ) -> A e. RR )
3	2	resincld	|- ( ( A e. RR+ /\ 1 < A ) -> ( sin ` A ) e. RR )
4		1red	|- ( ( A e. RR+ /\ 1 < A ) -> 1 e. RR )
5		sinbnd	|- ( A e. RR -> ( -u 1 <_ ( sin ` A ) /\ ( sin ` A ) <_ 1 ) )
6	5	simprd	|- ( A e. RR -> ( sin ` A ) <_ 1 )
7	1 6	syl	|- ( A e. RR+ -> ( sin ` A ) <_ 1 )
8	7	adantr	|- ( ( A e. RR+ /\ 1 < A ) -> ( sin ` A ) <_ 1 )
9		simpr	|- ( ( A e. RR+ /\ 1 < A ) -> 1 < A )
10	3 4 2 8 9	lelttrd	|- ( ( A e. RR+ /\ 1 < A ) -> ( sin ` A ) < A )
11		df-3an	|- ( ( A e. RR /\ 0 < A /\ A <_ 1 ) <-> ( ( A e. RR /\ 0 < A ) /\ A <_ 1 ) )
12		0xr	|- 0 e. RR*
13		1re	|- 1 e. RR
14		elioc2	|- ( ( 0 e. RR* /\ 1 e. RR ) -> ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) ) )
15	12 13 14	mp2an	|- ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) )
16		elrp	|- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
17	16	anbi1i	|- ( ( A e. RR+ /\ A <_ 1 ) <-> ( ( A e. RR /\ 0 < A ) /\ A <_ 1 ) )
18	11 15 17	3bitr4i	|- ( A e. ( 0 (,] 1 ) <-> ( A e. RR+ /\ A <_ 1 ) )
19		sin01bnd	|- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) )
20	19	simprd	|- ( A e. ( 0 (,] 1 ) -> ( sin ` A ) < A )
21	18 20	sylbir	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( sin ` A ) < A )
22		1red	|- ( A e. RR+ -> 1 e. RR )
23	10 21 22 1	ltlecasei	|- ( A e. RR+ -> ( sin ` A ) < A )