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 syl5eqr 
 |-  ( 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 syl5eqr 
 |-  ( 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 ) ) ) )