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 0 1 1 2 A 2 3 < cos A cos A < 1 A 2 3

Proof

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