Metamath Proof Explorer


Theorem cos01bnd

Description: Bounds on the cosine 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 cos01bnd
|- ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) /\ ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 1re
 |-  1 e. RR
2 0xr
 |-  0 e. RR*
3 elioc2
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) ) )
4 2 1 3 mp2an
 |-  ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) )
5 4 simp1bi
 |-  ( A e. ( 0 (,] 1 ) -> A e. RR )
6 5 resqcld
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 2 ) e. RR )
7 6 rehalfcld
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) / 2 ) e. RR )
8 resubcl
 |-  ( ( 1 e. RR /\ ( ( A ^ 2 ) / 2 ) e. RR ) -> ( 1 - ( ( A ^ 2 ) / 2 ) ) e. RR )
9 1 7 8 sylancr
 |-  ( A e. ( 0 (,] 1 ) -> ( 1 - ( ( A ^ 2 ) / 2 ) ) e. RR )
10 9 recnd
 |-  ( A e. ( 0 (,] 1 ) -> ( 1 - ( ( A ^ 2 ) / 2 ) ) e. CC )
11 ax-icn
 |-  _i e. CC
12 5 recnd
 |-  ( A e. ( 0 (,] 1 ) -> A e. CC )
13 mulcl
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
14 11 12 13 sylancr
 |-  ( A e. ( 0 (,] 1 ) -> ( _i x. A ) e. CC )
15 4nn0
 |-  4 e. NN0
16 eqid
 |-  ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )
17 16 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 )
18 14 15 17 sylancl
 |-  ( A e. ( 0 (,] 1 ) -> sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
19 18 recld
 |-  ( A e. ( 0 (,] 1 ) -> ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. RR )
20 19 recnd
 |-  ( A e. ( 0 (,] 1 ) -> ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. CC )
21 16 recos4p
 |-  ( A e. RR -> ( cos ` A ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
22 5 21 syl
 |-  ( A e. ( 0 (,] 1 ) -> ( cos ` A ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
23 10 20 22 mvrladdd
 |-  ( A e. ( 0 (,] 1 ) -> ( ( cos ` A ) - ( 1 - ( ( A ^ 2 ) / 2 ) ) ) = ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) )
24 23 fveq2d
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( ( cos ` A ) - ( 1 - ( ( A ^ 2 ) / 2 ) ) ) ) = ( abs ` ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
25 20 abscld
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) e. RR )
26 18 abscld
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. RR )
27 6nn
 |-  6 e. NN
28 nndivre
 |-  ( ( ( A ^ 2 ) e. RR /\ 6 e. NN ) -> ( ( A ^ 2 ) / 6 ) e. RR )
29 6 27 28 sylancl
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) / 6 ) e. RR )
30 absrele
 |-  ( sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) e. CC -> ( abs ` ( Re ` 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 18 30 syl
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( Re ` 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 15 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 27 34 sylancl
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) / 6 ) e. RR )
36 16 ef01bndlem
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) < ( ( A ^ 4 ) / 6 ) )
37 2nn0
 |-  2 e. NN0
38 37 a1i
 |-  ( A e. ( 0 (,] 1 ) -> 2 e. NN0 )
39 4z
 |-  4 e. ZZ
40 2re
 |-  2 e. RR
41 4re
 |-  4 e. RR
42 2lt4
 |-  2 < 4
43 40 41 42 ltleii
 |-  2 <_ 4
44 2z
 |-  2 e. ZZ
45 44 eluz1i
 |-  ( 4 e. ( ZZ>= ` 2 ) <-> ( 4 e. ZZ /\ 2 <_ 4 ) )
46 39 43 45 mpbir2an
 |-  4 e. ( ZZ>= ` 2 )
47 46 a1i
 |-  ( A e. ( 0 (,] 1 ) -> 4 e. ( ZZ>= ` 2 ) )
48 4 simp2bi
 |-  ( A e. ( 0 (,] 1 ) -> 0 < A )
49 0re
 |-  0 e. RR
50 ltle
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
51 49 5 50 sylancr
 |-  ( A e. ( 0 (,] 1 ) -> ( 0 < A -> 0 <_ A ) )
52 48 51 mpd
 |-  ( A e. ( 0 (,] 1 ) -> 0 <_ A )
53 4 simp3bi
 |-  ( A e. ( 0 (,] 1 ) -> A <_ 1 )
54 5 38 47 52 53 leexp2rd
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 4 ) <_ ( A ^ 2 ) )
55 6re
 |-  6 e. RR
56 55 a1i
 |-  ( A e. ( 0 (,] 1 ) -> 6 e. RR )
57 6pos
 |-  0 < 6
58 57 a1i
 |-  ( A e. ( 0 (,] 1 ) -> 0 < 6 )
59 lediv1
 |-  ( ( ( A ^ 4 ) e. RR /\ ( A ^ 2 ) e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( A ^ 4 ) <_ ( A ^ 2 ) <-> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 2 ) / 6 ) ) )
60 33 6 56 58 59 syl112anc
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) <_ ( A ^ 2 ) <-> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 2 ) / 6 ) ) )
61 54 60 mpbid
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 2 ) / 6 ) )
62 26 35 29 36 61 ltletrd
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) < ( ( A ^ 2 ) / 6 ) )
63 25 26 29 31 62 lelttrd
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) < ( ( A ^ 2 ) / 6 ) )
64 24 63 eqbrtrd
 |-  ( A e. ( 0 (,] 1 ) -> ( abs ` ( ( cos ` A ) - ( 1 - ( ( A ^ 2 ) / 2 ) ) ) ) < ( ( A ^ 2 ) / 6 ) )
65 5 recoscld
 |-  ( A e. ( 0 (,] 1 ) -> ( cos ` A ) e. RR )
66 65 9 29 absdifltd
 |-  ( A e. ( 0 (,] 1 ) -> ( ( abs ` ( ( cos ` A ) - ( 1 - ( ( A ^ 2 ) / 2 ) ) ) ) < ( ( A ^ 2 ) / 6 ) <-> ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) - ( ( A ^ 2 ) / 6 ) ) < ( cos ` A ) /\ ( cos ` A ) < ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 2 ) / 6 ) ) ) ) )
67 1cnd
 |-  ( A e. ( 0 (,] 1 ) -> 1 e. CC )
68 7 recnd
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) / 2 ) e. CC )
69 29 recnd
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) / 6 ) e. CC )
70 67 68 69 subsub4d
 |-  ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( ( A ^ 2 ) / 2 ) ) - ( ( A ^ 2 ) / 6 ) ) = ( 1 - ( ( ( A ^ 2 ) / 2 ) + ( ( A ^ 2 ) / 6 ) ) ) )
71 halfpm6th
 |-  ( ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( 1 / 3 ) /\ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) )
72 71 simpri
 |-  ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 )
73 72 oveq2i
 |-  ( ( A ^ 2 ) x. ( ( 1 / 2 ) + ( 1 / 6 ) ) ) = ( ( A ^ 2 ) x. ( 2 / 3 ) )
74 6 recnd
 |-  ( A e. ( 0 (,] 1 ) -> ( A ^ 2 ) e. CC )
75 2cn
 |-  2 e. CC
76 2ne0
 |-  2 =/= 0
77 75 76 reccli
 |-  ( 1 / 2 ) e. CC
78 6cn
 |-  6 e. CC
79 27 nnne0i
 |-  6 =/= 0
80 78 79 reccli
 |-  ( 1 / 6 ) e. CC
81 adddi
 |-  ( ( ( A ^ 2 ) e. CC /\ ( 1 / 2 ) e. CC /\ ( 1 / 6 ) e. CC ) -> ( ( A ^ 2 ) x. ( ( 1 / 2 ) + ( 1 / 6 ) ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) + ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
82 77 80 81 mp3an23
 |-  ( ( A ^ 2 ) e. CC -> ( ( A ^ 2 ) x. ( ( 1 / 2 ) + ( 1 / 6 ) ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) + ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
83 74 82 syl
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) x. ( ( 1 / 2 ) + ( 1 / 6 ) ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) + ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
84 73 83 eqtr3id
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) x. ( 2 / 3 ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) + ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
85 3cn
 |-  3 e. CC
86 3ne0
 |-  3 =/= 0
87 85 86 pm3.2i
 |-  ( 3 e. CC /\ 3 =/= 0 )
88 div12
 |-  ( ( 2 e. CC /\ ( A ^ 2 ) e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) = ( ( A ^ 2 ) x. ( 2 / 3 ) ) )
89 75 87 88 mp3an13
 |-  ( ( A ^ 2 ) e. CC -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) = ( ( A ^ 2 ) x. ( 2 / 3 ) ) )
90 74 89 syl
 |-  ( A e. ( 0 (,] 1 ) -> ( 2 x. ( ( A ^ 2 ) / 3 ) ) = ( ( A ^ 2 ) x. ( 2 / 3 ) ) )
91 divrec
 |-  ( ( ( A ^ 2 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( A ^ 2 ) / 2 ) = ( ( A ^ 2 ) x. ( 1 / 2 ) ) )
92 75 76 91 mp3an23
 |-  ( ( A ^ 2 ) e. CC -> ( ( A ^ 2 ) / 2 ) = ( ( A ^ 2 ) x. ( 1 / 2 ) ) )
93 74 92 syl
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) / 2 ) = ( ( A ^ 2 ) x. ( 1 / 2 ) ) )
94 divrec
 |-  ( ( ( A ^ 2 ) e. CC /\ 6 e. CC /\ 6 =/= 0 ) -> ( ( A ^ 2 ) / 6 ) = ( ( A ^ 2 ) x. ( 1 / 6 ) ) )
95 78 79 94 mp3an23
 |-  ( ( A ^ 2 ) e. CC -> ( ( A ^ 2 ) / 6 ) = ( ( A ^ 2 ) x. ( 1 / 6 ) ) )
96 74 95 syl
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) / 6 ) = ( ( A ^ 2 ) x. ( 1 / 6 ) ) )
97 93 96 oveq12d
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 2 ) / 2 ) + ( ( A ^ 2 ) / 6 ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) + ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
98 84 90 97 3eqtr4rd
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 2 ) / 2 ) + ( ( A ^ 2 ) / 6 ) ) = ( 2 x. ( ( A ^ 2 ) / 3 ) ) )
99 98 oveq2d
 |-  ( A e. ( 0 (,] 1 ) -> ( 1 - ( ( ( A ^ 2 ) / 2 ) + ( ( A ^ 2 ) / 6 ) ) ) = ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) )
100 70 99 eqtrd
 |-  ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( ( A ^ 2 ) / 2 ) ) - ( ( A ^ 2 ) / 6 ) ) = ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) )
101 100 breq1d
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) - ( ( A ^ 2 ) / 6 ) ) < ( cos ` A ) <-> ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) ) )
102 67 68 69 subsubd
 |-  ( A e. ( 0 (,] 1 ) -> ( 1 - ( ( ( A ^ 2 ) / 2 ) - ( ( A ^ 2 ) / 6 ) ) ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 2 ) / 6 ) ) )
103 71 simpli
 |-  ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( 1 / 3 )
104 103 oveq2i
 |-  ( ( A ^ 2 ) x. ( ( 1 / 2 ) - ( 1 / 6 ) ) ) = ( ( A ^ 2 ) x. ( 1 / 3 ) )
105 subdi
 |-  ( ( ( A ^ 2 ) e. CC /\ ( 1 / 2 ) e. CC /\ ( 1 / 6 ) e. CC ) -> ( ( A ^ 2 ) x. ( ( 1 / 2 ) - ( 1 / 6 ) ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) - ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
106 77 80 105 mp3an23
 |-  ( ( A ^ 2 ) e. CC -> ( ( A ^ 2 ) x. ( ( 1 / 2 ) - ( 1 / 6 ) ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) - ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
107 74 106 syl
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) x. ( ( 1 / 2 ) - ( 1 / 6 ) ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) - ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
108 104 107 eqtr3id
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) x. ( 1 / 3 ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) - ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
109 divrec
 |-  ( ( ( A ^ 2 ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( ( A ^ 2 ) / 3 ) = ( ( A ^ 2 ) x. ( 1 / 3 ) ) )
110 85 86 109 mp3an23
 |-  ( ( A ^ 2 ) e. CC -> ( ( A ^ 2 ) / 3 ) = ( ( A ^ 2 ) x. ( 1 / 3 ) ) )
111 74 110 syl
 |-  ( A e. ( 0 (,] 1 ) -> ( ( A ^ 2 ) / 3 ) = ( ( A ^ 2 ) x. ( 1 / 3 ) ) )
112 93 96 oveq12d
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 2 ) / 2 ) - ( ( A ^ 2 ) / 6 ) ) = ( ( ( A ^ 2 ) x. ( 1 / 2 ) ) - ( ( A ^ 2 ) x. ( 1 / 6 ) ) ) )
113 108 111 112 3eqtr4rd
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 2 ) / 2 ) - ( ( A ^ 2 ) / 6 ) ) = ( ( A ^ 2 ) / 3 ) )
114 113 oveq2d
 |-  ( A e. ( 0 (,] 1 ) -> ( 1 - ( ( ( A ^ 2 ) / 2 ) - ( ( A ^ 2 ) / 6 ) ) ) = ( 1 - ( ( A ^ 2 ) / 3 ) ) )
115 102 114 eqtr3d
 |-  ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 2 ) / 6 ) ) = ( 1 - ( ( A ^ 2 ) / 3 ) ) )
116 115 breq2d
 |-  ( A e. ( 0 (,] 1 ) -> ( ( cos ` A ) < ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 2 ) / 6 ) ) <-> ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) )
117 101 116 anbi12d
 |-  ( A e. ( 0 (,] 1 ) -> ( ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) - ( ( A ^ 2 ) / 6 ) ) < ( cos ` A ) /\ ( cos ` A ) < ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 2 ) / 6 ) ) ) <-> ( ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) /\ ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) ) )
118 66 117 bitrd
 |-  ( A e. ( 0 (,] 1 ) -> ( ( abs ` ( ( cos ` A ) - ( 1 - ( ( A ^ 2 ) / 2 ) ) ) ) < ( ( A ^ 2 ) / 6 ) <-> ( ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) /\ ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) ) )
119 64 118 mpbid
 |-  ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) /\ ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) )