Metamath Proof Explorer

Theorem sin01gt0

Description: The sine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Wolf Lammen, 25-Sep-2020)

Ref Expression
Assertion sin01gt0 
|- ( A e. ( 0 (,] 1 ) -> 0 < ( sin ` A ) )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 1re 
 |-  1 e. RR
3 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) ) )
4 1 2 3 mp2an 
 |-  ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) )
5 4 simp1bi 
 |-  ( A e. ( 0 (,] 1 ) -> A e. RR )
6 3nn0 
 |-  3 e. NN0
7 reexpcl 
 |-  ( ( A e. RR /\ 3 e. NN0 ) -> ( A ^ 3 ) e. RR )
8 5 6 7 sylancl 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 3 ) e. RR )
9 3re 
 |-  3 e. RR
10 3ne0 
 |-  3 =/= 0
11 redivcl 
 |-  ( ( ( A ^ 3 ) e. RR /\ 3 e. RR /\ 3 =/= 0 ) -> ( ( A ^ 3 ) / 3 ) e. RR )
12 9 10 11 mp3an23 
 |-  ( ( A ^ 3 ) e. RR -> ( ( A ^ 3 ) / 3 ) e. RR )
13 8 12 syl 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 3 ) e. RR )
14 3z 
 |-  3 e. ZZ
15 expgt0 
 |-  ( ( A e. RR /\ 3 e. ZZ /\ 0 < A ) -> 0 < ( A ^ 3 ) )
16 14 15 mp3an2 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( A ^ 3 ) )
17 16 3adant3 
 |-  ( ( A e. RR /\ 0 < A /\ A <_ 1 ) -> 0 < ( A ^ 3 ) )
18 4 17 sylbi 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < ( A ^ 3 ) )
19 0lt1 
 |-  0 < 1
20 2 19 pm3.2i 
 |-  ( 1 e. RR /\ 0 < 1 )
21 3pos 
 |-  0 < 3
22 9 21 pm3.2i 
 |-  ( 3 e. RR /\ 0 < 3 )
23 1lt3 
 |-  1 < 3
24 ltdiv2 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( 3 e. RR /\ 0 < 3 ) /\ ( ( A ^ 3 ) e. RR /\ 0 < ( A ^ 3 ) ) ) -> ( 1 < 3 <-> ( ( A ^ 3 ) / 3 ) < ( ( A ^ 3 ) / 1 ) ) )
25 23 24 mpbii 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( 3 e. RR /\ 0 < 3 ) /\ ( ( A ^ 3 ) e. RR /\ 0 < ( A ^ 3 ) ) ) -> ( ( A ^ 3 ) / 3 ) < ( ( A ^ 3 ) / 1 ) )
26 20 22 25 mp3an12 
 |-  ( ( ( A ^ 3 ) e. RR /\ 0 < ( A ^ 3 ) ) -> ( ( A ^ 3 ) / 3 ) < ( ( A ^ 3 ) / 1 ) )
27 8 18 26 syl2anc 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 3 ) < ( ( A ^ 3 ) / 1 ) )
28 8 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 3 ) e. CC )
29 28 div1d 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 1 ) = ( A ^ 3 ) )
30 27 29 breqtrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 3 ) < ( A ^ 3 ) )
31 1nn0 
 |-  1 e. NN0
32 31 a1i 
 |-  ( A e. ( 0 (,] 1 ) -> 1 e. NN0 )
33 1le3 
 |-  1 <_ 3
34 1z 
 |-  1 e. ZZ
35 34 eluz1i 
 |-  ( 3 e. ( ZZ>= ` 1 ) <-> ( 3 e. ZZ /\ 1 <_ 3 ) )
36 14 33 35 mpbir2an 
 |-  3 e. ( ZZ>= ` 1 )
37 36 a1i 
 |-  ( A e. ( 0 (,] 1 ) -> 3 e. ( ZZ>= ` 1 ) )
38 4 simp2bi 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < A )
39 0re 
 |-  0 e. RR
40 ltle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
41 39 5 40 sylancr 
 |-  ( A e. ( 0 (,] 1 ) -> ( 0 < A -> 0 <_ A ) )
42 38 41 mpd 
 |-  ( A e. ( 0 (,] 1 ) -> 0 <_ A )
43 4 simp3bi 
 |-  ( A e. ( 0 (,] 1 ) -> A <_ 1 )
44 5 32 37 42 43 leexp2rd 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 3 ) <_ ( A ^ 1 ) )
45 5 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> A e. CC )
46 45 exp1d 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 1 ) = A )
47 44 46 breqtrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 3 ) <_ A )
48 13 8 5 30 47 ltletrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 3 ) < A )
49 13 5 posdifd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 3 ) / 3 ) < A <-> 0 < ( A - ( ( A ^ 3 ) / 3 ) ) ) )
50 48 49 mpbid 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < ( A - ( ( A ^ 3 ) / 3 ) ) )
51 sin01bnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) )
52 51 simpld 
 |-  ( A e. ( 0 (,] 1 ) -> ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) )
53 5 13 resubcld 
 |-  ( A e. ( 0 (,] 1 ) -> ( A - ( ( A ^ 3 ) / 3 ) ) e. RR )
54 5 resincld 
 |-  ( A e. ( 0 (,] 1 ) -> ( sin ` A ) e. RR )
55 lttr 
 |-  ( ( 0 e. RR /\ ( A - ( ( A ^ 3 ) / 3 ) ) e. RR /\ ( sin ` A ) e. RR ) -> ( ( 0 < ( A - ( ( A ^ 3 ) / 3 ) ) /\ ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) ) -> 0 < ( sin ` A ) ) )
56 39 53 54 55 mp3an2i 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( 0 < ( A - ( ( A ^ 3 ) / 3 ) ) /\ ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) ) -> 0 < ( sin ` A ) ) )
57 50 52 56 mp2and 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < ( sin ` A ) )