Metamath Proof Explorer

Theorem sin01bnd

Description: Bounds on the sine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion sin01bnd 
|- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < 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 6nn 
 |-  6 e. NN
10 nndivre 
 |-  ( ( ( A ^ 3 ) e. RR /\ 6 e. NN ) -> ( ( A ^ 3 ) / 6 ) e. RR )
11 8 9 10 sylancl 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 6 ) e. RR )
12 5 11 resubcld 
 |-  ( A e. ( 0 (,] 1 ) -> ( A - ( ( A ^ 3 ) / 6 ) ) e. RR )
13 12 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( A - ( ( A ^ 3 ) / 6 ) ) e. CC )
14 ax-icn 
 |-  _i e. CC
15 5 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> A e. CC )
16 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
17 14 15 16 sylancr 
 |-  ( A e. ( 0 (,] 1 ) -> ( _i x. A ) e. CC )
18 4nn0 
 |-  4 e. NN0
19 eqid 
 |-  ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )
20 19 eftlcl 
 |-  ( ( ( _i x. A ) e. CC /\ 4 e. NN0 ) -> sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
21 17 18 20 sylancl 
 |-  ( A e. ( 0 (,] 1 ) -> sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
22 21 imcld 
 |-  ( A e. ( 0 (,] 1 ) -> ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. RR )
23 22 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. CC )
24 19 resin4p 
 |-  ( A e. RR -> ( sin ` A ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
25 5 24 syl 
 |-  ( A e. ( 0 (,] 1 ) -> ( sin ` A ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
26 13 23 25 mvrladdd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) = ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) )
27 26 fveq2d 
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) ) = ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
28 23 abscld 
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) e. RR )
29 21 abscld 
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. RR )
30 absimle 
 |-  ( sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) e. CC -> ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) <_ ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) )
31 21 30 syl 
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) <_ ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) )
32 reexpcl 
 |-  ( ( A e. RR /\ 4 e. NN0 ) -> ( A ^ 4 ) e. RR )
33 5 18 32 sylancl 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 4 ) e. RR )
34 nndivre 
 |-  ( ( ( A ^ 4 ) e. RR /\ 6 e. NN ) -> ( ( A ^ 4 ) / 6 ) e. RR )
35 33 9 34 sylancl 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) / 6 ) e. RR )
36 19 ef01bndlem 
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) < ( ( A ^ 4 ) / 6 ) )
37 6 a1i 
 |-  ( A e. ( 0 (,] 1 ) -> 3 e. NN0 )
38 4z 
 |-  4 e. ZZ
39 3re 
 |-  3 e. RR
40 4re 
 |-  4 e. RR
41 3lt4 
 |-  3 < 4
42 39 40 41 ltleii 
 |-  3 <_ 4
43 3z 
 |-  3 e. ZZ
44 43 eluz1i 
 |-  ( 4 e. ( ZZ>= ` 3 ) <-> ( 4 e. ZZ /\ 3 <_ 4 ) )
45 38 42 44 mpbir2an 
 |-  4 e. ( ZZ>= ` 3 )
46 45 a1i 
 |-  ( A e. ( 0 (,] 1 ) -> 4 e. ( ZZ>= ` 3 ) )
47 4 simp2bi 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < A )
48 0re 
 |-  0 e. RR
49 ltle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
50 48 5 49 sylancr 
 |-  ( A e. ( 0 (,] 1 ) -> ( 0 < A -> 0 <_ A ) )
51 47 50 mpd 
 |-  ( A e. ( 0 (,] 1 ) -> 0 <_ A )
52 4 simp3bi 
 |-  ( A e. ( 0 (,] 1 ) -> A <_ 1 )
53 5 37 46 51 52 leexp2rd 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 4 ) <_ ( A ^ 3 ) )
54 6re 
 |-  6 e. RR
55 54 a1i 
 |-  ( A e. ( 0 (,] 1 ) -> 6 e. RR )
56 6pos 
 |-  0 < 6
57 56 a1i 
 |-  ( A e. ( 0 (,] 1 ) -> 0 < 6 )
58 lediv1 
 |-  ( ( ( A ^ 4 ) e. RR /\ ( A ^ 3 ) e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( A ^ 4 ) <_ ( A ^ 3 ) <-> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 3 ) / 6 ) ) )
59 33 8 55 57 58 syl112anc 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) <_ ( A ^ 3 ) <-> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 3 ) / 6 ) ) )
60 53 59 mpbid 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 3 ) / 6 ) )
61 29 35 11 36 60 ltletrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) < ( ( A ^ 3 ) / 6 ) )
62 28 29 11 31 61 lelttrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) < ( ( A ^ 3 ) / 6 ) )
63 27 62 eqbrtrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) ) < ( ( A ^ 3 ) / 6 ) )
64 5 resincld 
 |-  ( A e. ( 0 (,] 1 ) -> ( sin ` A ) e. RR )
65 64 12 11 absdifltd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( abs ` ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) ) < ( ( A ^ 3 ) / 6 ) <-> ( ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) < ( sin ` A ) /\ ( sin ` A ) < ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( ( A ^ 3 ) / 6 ) ) ) ) )
66 11 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 6 ) e. CC )
67 15 66 66 subsub4d 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) = ( A - ( ( ( A ^ 3 ) / 6 ) + ( ( A ^ 3 ) / 6 ) ) ) )
68 8 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 3 ) e. CC )
69 3cn 
 |-  3 e. CC
70 3ne0 
 |-  3 =/= 0
71 69 70 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
72 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
73 divdiv1 
 |-  ( ( ( A ^ 3 ) e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( A ^ 3 ) / 3 ) / 2 ) = ( ( A ^ 3 ) / ( 3 x. 2 ) ) )
74 71 72 73 mp3an23 
 |-  ( ( A ^ 3 ) e. CC -> ( ( ( A ^ 3 ) / 3 ) / 2 ) = ( ( A ^ 3 ) / ( 3 x. 2 ) ) )
75 68 74 syl 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 3 ) / 3 ) / 2 ) = ( ( A ^ 3 ) / ( 3 x. 2 ) ) )
76 3t2e6 
 |-  ( 3 x. 2 ) = 6
77 76 oveq2i 
 |-  ( ( A ^ 3 ) / ( 3 x. 2 ) ) = ( ( A ^ 3 ) / 6 )
78 75 77 eqtr2di 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 6 ) = ( ( ( A ^ 3 ) / 3 ) / 2 ) )
79 78 78 oveq12d 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 3 ) / 6 ) + ( ( A ^ 3 ) / 6 ) ) = ( ( ( ( A ^ 3 ) / 3 ) / 2 ) + ( ( ( A ^ 3 ) / 3 ) / 2 ) ) )
80 3nn 
 |-  3 e. NN
81 nndivre 
 |-  ( ( ( A ^ 3 ) e. RR /\ 3 e. NN ) -> ( ( A ^ 3 ) / 3 ) e. RR )
82 8 80 81 sylancl 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 3 ) e. RR )
83 82 recnd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 3 ) e. CC )
84 83 2halvesd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( ( A ^ 3 ) / 3 ) / 2 ) + ( ( ( A ^ 3 ) / 3 ) / 2 ) ) = ( ( A ^ 3 ) / 3 ) )
85 79 84 eqtrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 3 ) / 6 ) + ( ( A ^ 3 ) / 6 ) ) = ( ( A ^ 3 ) / 3 ) )
86 85 oveq2d 
 |-  ( A e. ( 0 (,] 1 ) -> ( A - ( ( ( A ^ 3 ) / 6 ) + ( ( A ^ 3 ) / 6 ) ) ) = ( A - ( ( A ^ 3 ) / 3 ) ) )
87 67 86 eqtrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) = ( A - ( ( A ^ 3 ) / 3 ) ) )
88 87 breq1d 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) < ( sin ` A ) <-> ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) ) )
89 15 66 npcand 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( ( A ^ 3 ) / 6 ) ) = A )
90 89 breq2d 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( sin ` A ) < ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( ( A ^ 3 ) / 6 ) ) <-> ( sin ` A ) < A ) )
91 88 90 anbi12d 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) < ( sin ` A ) /\ ( sin ` A ) < ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( ( A ^ 3 ) / 6 ) ) ) <-> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) ) )
92 65 91 bitrd 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( abs ` ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) ) < ( ( A ^ 3 ) / 6 ) <-> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) ) )
93 63 92 mpbid 
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) )