This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )