# Metamath Proof Explorer

## Theorem cos2bnd

Description: Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008)

Ref Expression
Assertion cos2bnd ${⊢}\left(-\frac{7}{9}<\mathrm{cos}2\wedge \mathrm{cos}2<-\frac{1}{9}\right)$

### Proof

Step Hyp Ref Expression
1 7cn ${⊢}7\in ℂ$
2 9cn ${⊢}9\in ℂ$
3 9re ${⊢}9\in ℝ$
4 9pos ${⊢}0<9$
5 3 4 gt0ne0ii ${⊢}9\ne 0$
6 divneg ${⊢}\left(7\in ℂ\wedge 9\in ℂ\wedge 9\ne 0\right)\to -\frac{7}{9}=\frac{-7}{9}$
7 1 2 5 6 mp3an ${⊢}-\frac{7}{9}=\frac{-7}{9}$
8 2cn ${⊢}2\in ℂ$
9 2 5 pm3.2i ${⊢}\left(9\in ℂ\wedge 9\ne 0\right)$
10 divsubdir ${⊢}\left(2\in ℂ\wedge 9\in ℂ\wedge \left(9\in ℂ\wedge 9\ne 0\right)\right)\to \frac{2-9}{9}=\left(\frac{2}{9}\right)-\left(\frac{9}{9}\right)$
11 8 2 9 10 mp3an ${⊢}\frac{2-9}{9}=\left(\frac{2}{9}\right)-\left(\frac{9}{9}\right)$
12 2 8 negsubdi2i ${⊢}-\left(9-2\right)=2-9$
13 7p2e9 ${⊢}7+2=9$
14 2 8 1 subadd2i ${⊢}9-2=7↔7+2=9$
15 13 14 mpbir ${⊢}9-2=7$
16 15 negeqi ${⊢}-\left(9-2\right)=-7$
17 12 16 eqtr3i ${⊢}2-9=-7$
18 17 oveq1i ${⊢}\frac{2-9}{9}=\frac{-7}{9}$
19 11 18 eqtr3i ${⊢}\left(\frac{2}{9}\right)-\left(\frac{9}{9}\right)=\frac{-7}{9}$
20 2 5 dividi ${⊢}\frac{9}{9}=1$
21 20 oveq2i ${⊢}\left(\frac{2}{9}\right)-\left(\frac{9}{9}\right)=\left(\frac{2}{9}\right)-1$
22 7 19 21 3eqtr2ri ${⊢}\left(\frac{2}{9}\right)-1=-\frac{7}{9}$
23 ax-1cn ${⊢}1\in ℂ$
24 8 23 2 5 divassi ${⊢}\frac{2\cdot 1}{9}=2\left(\frac{1}{9}\right)$
25 2t1e2 ${⊢}2\cdot 1=2$
26 25 oveq1i ${⊢}\frac{2\cdot 1}{9}=\frac{2}{9}$
27 24 26 eqtr3i ${⊢}2\left(\frac{1}{9}\right)=\frac{2}{9}$
28 3cn ${⊢}3\in ℂ$
29 3ne0 ${⊢}3\ne 0$
30 23 28 29 sqdivi ${⊢}{\left(\frac{1}{3}\right)}^{2}=\frac{{1}^{2}}{{3}^{2}}$
31 sq1 ${⊢}{1}^{2}=1$
32 sq3 ${⊢}{3}^{2}=9$
33 31 32 oveq12i ${⊢}\frac{{1}^{2}}{{3}^{2}}=\frac{1}{9}$
34 30 33 eqtri ${⊢}{\left(\frac{1}{3}\right)}^{2}=\frac{1}{9}$
35 cos1bnd ${⊢}\left(\frac{1}{3}<\mathrm{cos}1\wedge \mathrm{cos}1<\frac{2}{3}\right)$
36 35 simpli ${⊢}\frac{1}{3}<\mathrm{cos}1$
37 0le1 ${⊢}0\le 1$
38 3pos ${⊢}0<3$
39 1re ${⊢}1\in ℝ$
40 3re ${⊢}3\in ℝ$
41 39 40 divge0i ${⊢}\left(0\le 1\wedge 0<3\right)\to 0\le \frac{1}{3}$
42 37 38 41 mp2an ${⊢}0\le \frac{1}{3}$
43 0re ${⊢}0\in ℝ$
44 recoscl ${⊢}1\in ℝ\to \mathrm{cos}1\in ℝ$
45 39 44 ax-mp ${⊢}\mathrm{cos}1\in ℝ$
46 40 29 rereccli ${⊢}\frac{1}{3}\in ℝ$
47 43 46 45 lelttri ${⊢}\left(0\le \frac{1}{3}\wedge \frac{1}{3}<\mathrm{cos}1\right)\to 0<\mathrm{cos}1$
48 42 36 47 mp2an ${⊢}0<\mathrm{cos}1$
49 43 45 48 ltleii ${⊢}0\le \mathrm{cos}1$
50 46 45 lt2sqi ${⊢}\left(0\le \frac{1}{3}\wedge 0\le \mathrm{cos}1\right)\to \left(\frac{1}{3}<\mathrm{cos}1↔{\left(\frac{1}{3}\right)}^{2}<{\mathrm{cos}1}^{2}\right)$
51 42 49 50 mp2an ${⊢}\frac{1}{3}<\mathrm{cos}1↔{\left(\frac{1}{3}\right)}^{2}<{\mathrm{cos}1}^{2}$
52 36 51 mpbi ${⊢}{\left(\frac{1}{3}\right)}^{2}<{\mathrm{cos}1}^{2}$
53 34 52 eqbrtrri ${⊢}\frac{1}{9}<{\mathrm{cos}1}^{2}$
54 2pos ${⊢}0<2$
55 3 5 rereccli ${⊢}\frac{1}{9}\in ℝ$
56 45 resqcli ${⊢}{\mathrm{cos}1}^{2}\in ℝ$
57 2re ${⊢}2\in ℝ$
58 55 56 57 ltmul2i ${⊢}0<2\to \left(\frac{1}{9}<{\mathrm{cos}1}^{2}↔2\left(\frac{1}{9}\right)<2{\mathrm{cos}1}^{2}\right)$
59 54 58 ax-mp ${⊢}\frac{1}{9}<{\mathrm{cos}1}^{2}↔2\left(\frac{1}{9}\right)<2{\mathrm{cos}1}^{2}$
60 53 59 mpbi ${⊢}2\left(\frac{1}{9}\right)<2{\mathrm{cos}1}^{2}$
61 27 60 eqbrtrri ${⊢}\frac{2}{9}<2{\mathrm{cos}1}^{2}$
62 57 3 5 redivcli ${⊢}\frac{2}{9}\in ℝ$
63 57 56 remulcli ${⊢}2{\mathrm{cos}1}^{2}\in ℝ$
64 ltsub1 ${⊢}\left(\frac{2}{9}\in ℝ\wedge 2{\mathrm{cos}1}^{2}\in ℝ\wedge 1\in ℝ\right)\to \left(\frac{2}{9}<2{\mathrm{cos}1}^{2}↔\left(\frac{2}{9}\right)-1<2{\mathrm{cos}1}^{2}-1\right)$
65 62 63 39 64 mp3an ${⊢}\frac{2}{9}<2{\mathrm{cos}1}^{2}↔\left(\frac{2}{9}\right)-1<2{\mathrm{cos}1}^{2}-1$
66 61 65 mpbi ${⊢}\left(\frac{2}{9}\right)-1<2{\mathrm{cos}1}^{2}-1$
67 22 66 eqbrtrri ${⊢}-\frac{7}{9}<2{\mathrm{cos}1}^{2}-1$
68 25 fveq2i ${⊢}\mathrm{cos}2\cdot 1=\mathrm{cos}2$
69 cos2t ${⊢}1\in ℂ\to \mathrm{cos}2\cdot 1=2{\mathrm{cos}1}^{2}-1$
70 23 69 ax-mp ${⊢}\mathrm{cos}2\cdot 1=2{\mathrm{cos}1}^{2}-1$
71 68 70 eqtr3i ${⊢}\mathrm{cos}2=2{\mathrm{cos}1}^{2}-1$
72 67 71 breqtrri ${⊢}-\frac{7}{9}<\mathrm{cos}2$
73 35 simpri ${⊢}\mathrm{cos}1<\frac{2}{3}$
74 0le2 ${⊢}0\le 2$
75 57 40 divge0i ${⊢}\left(0\le 2\wedge 0<3\right)\to 0\le \frac{2}{3}$
76 74 38 75 mp2an ${⊢}0\le \frac{2}{3}$
77 57 40 29 redivcli ${⊢}\frac{2}{3}\in ℝ$
78 45 77 lt2sqi ${⊢}\left(0\le \mathrm{cos}1\wedge 0\le \frac{2}{3}\right)\to \left(\mathrm{cos}1<\frac{2}{3}↔{\mathrm{cos}1}^{2}<{\left(\frac{2}{3}\right)}^{2}\right)$
79 49 76 78 mp2an ${⊢}\mathrm{cos}1<\frac{2}{3}↔{\mathrm{cos}1}^{2}<{\left(\frac{2}{3}\right)}^{2}$
80 73 79 mpbi ${⊢}{\mathrm{cos}1}^{2}<{\left(\frac{2}{3}\right)}^{2}$
81 8 28 29 sqdivi ${⊢}{\left(\frac{2}{3}\right)}^{2}=\frac{{2}^{2}}{{3}^{2}}$
82 sq2 ${⊢}{2}^{2}=4$
83 82 32 oveq12i ${⊢}\frac{{2}^{2}}{{3}^{2}}=\frac{4}{9}$
84 81 83 eqtri ${⊢}{\left(\frac{2}{3}\right)}^{2}=\frac{4}{9}$
85 80 84 breqtri ${⊢}{\mathrm{cos}1}^{2}<\frac{4}{9}$
86 4re ${⊢}4\in ℝ$
87 86 3 5 redivcli ${⊢}\frac{4}{9}\in ℝ$
88 56 87 57 ltmul2i ${⊢}0<2\to \left({\mathrm{cos}1}^{2}<\frac{4}{9}↔2{\mathrm{cos}1}^{2}<2\left(\frac{4}{9}\right)\right)$
89 54 88 ax-mp ${⊢}{\mathrm{cos}1}^{2}<\frac{4}{9}↔2{\mathrm{cos}1}^{2}<2\left(\frac{4}{9}\right)$
90 85 89 mpbi ${⊢}2{\mathrm{cos}1}^{2}<2\left(\frac{4}{9}\right)$
91 4cn ${⊢}4\in ℂ$
92 8 91 2 5 divassi ${⊢}\frac{2\cdot 4}{9}=2\left(\frac{4}{9}\right)$
93 4t2e8 ${⊢}4\cdot 2=8$
94 91 8 93 mulcomli ${⊢}2\cdot 4=8$
95 94 oveq1i ${⊢}\frac{2\cdot 4}{9}=\frac{8}{9}$
96 92 95 eqtr3i ${⊢}2\left(\frac{4}{9}\right)=\frac{8}{9}$
97 90 96 breqtri ${⊢}2{\mathrm{cos}1}^{2}<\frac{8}{9}$
98 8re ${⊢}8\in ℝ$
99 98 3 5 redivcli ${⊢}\frac{8}{9}\in ℝ$
100 ltsub1 ${⊢}\left(2{\mathrm{cos}1}^{2}\in ℝ\wedge \frac{8}{9}\in ℝ\wedge 1\in ℝ\right)\to \left(2{\mathrm{cos}1}^{2}<\frac{8}{9}↔2{\mathrm{cos}1}^{2}-1<\left(\frac{8}{9}\right)-1\right)$
101 63 99 39 100 mp3an ${⊢}2{\mathrm{cos}1}^{2}<\frac{8}{9}↔2{\mathrm{cos}1}^{2}-1<\left(\frac{8}{9}\right)-1$
102 97 101 mpbi ${⊢}2{\mathrm{cos}1}^{2}-1<\left(\frac{8}{9}\right)-1$
103 20 oveq2i ${⊢}\left(\frac{8}{9}\right)-\left(\frac{9}{9}\right)=\left(\frac{8}{9}\right)-1$
104 divneg ${⊢}\left(1\in ℂ\wedge 9\in ℂ\wedge 9\ne 0\right)\to -\frac{1}{9}=\frac{-1}{9}$
105 23 2 5 104 mp3an ${⊢}-\frac{1}{9}=\frac{-1}{9}$
106 8cn ${⊢}8\in ℂ$
107 2 106 negsubdi2i ${⊢}-\left(9-8\right)=8-9$
108 8p1e9 ${⊢}8+1=9$
109 2 106 23 108 subaddrii ${⊢}9-8=1$
110 109 negeqi ${⊢}-\left(9-8\right)=-1$
111 107 110 eqtr3i ${⊢}8-9=-1$
112 111 oveq1i ${⊢}\frac{8-9}{9}=\frac{-1}{9}$
113 divsubdir ${⊢}\left(8\in ℂ\wedge 9\in ℂ\wedge \left(9\in ℂ\wedge 9\ne 0\right)\right)\to \frac{8-9}{9}=\left(\frac{8}{9}\right)-\left(\frac{9}{9}\right)$
114 106 2 9 113 mp3an ${⊢}\frac{8-9}{9}=\left(\frac{8}{9}\right)-\left(\frac{9}{9}\right)$
115 105 112 114 3eqtr2ri ${⊢}\left(\frac{8}{9}\right)-\left(\frac{9}{9}\right)=-\frac{1}{9}$
116 103 115 eqtr3i ${⊢}\left(\frac{8}{9}\right)-1=-\frac{1}{9}$
117 102 116 breqtri ${⊢}2{\mathrm{cos}1}^{2}-1<-\frac{1}{9}$
118 71 117 eqbrtri ${⊢}\mathrm{cos}2<-\frac{1}{9}$
119 72 118 pm3.2i ${⊢}\left(-\frac{7}{9}<\mathrm{cos}2\wedge \mathrm{cos}2<-\frac{1}{9}\right)$