Theorem cos2bnd

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

	Ref	Expression
Assertion	cos2bnd	$$⊢\left(-\frac{7}{9}<\cos 2\wedge \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\leftrightarrow 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}<\cos 1\wedge \cos 1<\frac{2}{3}\right)$$
36	35	simpli	$$⊢\frac{1}{3}<\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 \cos 1\in ℝ$$
45	39 44	ax-mp	$$⊢\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}<\cos 1\right)\to 0<\cos 1$$
48	42 36 47	mp2an	$$⊢0<\cos 1$$
49	43 45 48	ltleii	$$⊢0\le \cos 1$$
50	46 45	lt2sqi	$$⊢\left(0\le \frac{1}{3}\wedge 0\le \cos 1\right)\to \left(\frac{1}{3}<\cos 1\leftrightarrow {\left(\frac{1}{3}\right)}^2<{\cos 1}^2\right)$$
51	42 49 50	mp2an	$$⊢\frac{1}{3}<\cos 1\leftrightarrow {\left(\frac{1}{3}\right)}^2<{\cos 1}^2$$
52	36 51	mpbi	$$⊢{\left(\frac{1}{3}\right)}^2<{\cos 1}^2$$
53	34 52	eqbrtrri	$$⊢\frac{1}{9}<{\cos 1}^2$$
54		2pos	$$⊢0<2$$
55	3 5	rereccli	$$⊢\frac{1}{9}\in ℝ$$
56	45	resqcli	$$⊢{\cos 1}^2\in ℝ$$
57		2re	$$⊢2\in ℝ$$
58	55 56 57	ltmul2i	$$⊢0<2\to \left(\frac{1}{9}<{\cos 1}^2\leftrightarrow 2\left(\frac{1}{9}\right)<2{\cos 1}^2\right)$$
59	54 58	ax-mp	$$⊢\frac{1}{9}<{\cos 1}^2\leftrightarrow 2\left(\frac{1}{9}\right)<2{\cos 1}^2$$
60	53 59	mpbi	$$⊢2\left(\frac{1}{9}\right)<2{\cos 1}^2$$
61	27 60	eqbrtrri	$$⊢\frac{2}{9}<2{\cos 1}^2$$
62	57 3 5	redivcli	$$⊢\frac{2}{9}\in ℝ$$
63	57 56	remulcli	$$⊢2{\cos 1}^2\in ℝ$$
64		ltsub1	$$⊢\left(\frac{2}{9}\in ℝ\wedge 2{\cos 1}^2\in ℝ\wedge 1\in ℝ\right)\to \left(\frac{2}{9}<2{\cos 1}^2\leftrightarrow \left(\frac{2}{9}\right)-1<2{\cos 1}^2-1\right)$$
65	62 63 39 64	mp3an	$$⊢\frac{2}{9}<2{\cos 1}^2\leftrightarrow \left(\frac{2}{9}\right)-1<2{\cos 1}^2-1$$
66	61 65	mpbi	$$⊢\left(\frac{2}{9}\right)-1<2{\cos 1}^2-1$$
67	22 66	eqbrtrri	$$⊢-\frac{7}{9}<2{\cos 1}^2-1$$
68	25	fveq2i	$$⊢\cos 2\cdot 1=\cos 2$$
69		cos2t	$$⊢1\in ℂ\to \cos 2\cdot 1=2{\cos 1}^2-1$$
70	23 69	ax-mp	$$⊢\cos 2\cdot 1=2{\cos 1}^2-1$$
71	68 70	eqtr3i	$$⊢\cos 2=2{\cos 1}^2-1$$
72	67 71	breqtrri	$$⊢-\frac{7}{9}<\cos 2$$
73	35	simpri	$$⊢\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 \cos 1\wedge 0\le \frac{2}{3}\right)\to \left(\cos 1<\frac{2}{3}\leftrightarrow {\cos 1}^2<{\left(\frac{2}{3}\right)}^2\right)$$
79	49 76 78	mp2an	$$⊢\cos 1<\frac{2}{3}\leftrightarrow {\cos 1}^2<{\left(\frac{2}{3}\right)}^2$$
80	73 79	mpbi	$$⊢{\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	$$⊢{\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({\cos 1}^2<\frac{4}{9}\leftrightarrow 2{\cos 1}^2<2\left(\frac{4}{9}\right)\right)$$
89	54 88	ax-mp	$$⊢{\cos 1}^2<\frac{4}{9}\leftrightarrow 2{\cos 1}^2<2\left(\frac{4}{9}\right)$$
90	85 89	mpbi	$$⊢2{\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{\cos 1}^2<\frac{8}{9}$$
98		8re	$$⊢8\in ℝ$$
99	98 3 5	redivcli	$$⊢\frac{8}{9}\in ℝ$$
100		ltsub1	$$⊢\left(2{\cos 1}^2\in ℝ\wedge \frac{8}{9}\in ℝ\wedge 1\in ℝ\right)\to \left(2{\cos 1}^2<\frac{8}{9}\leftrightarrow 2{\cos 1}^2-1<\left(\frac{8}{9}\right)-1\right)$$
101	63 99 39 100	mp3an	$$⊢2{\cos 1}^2<\frac{8}{9}\leftrightarrow 2{\cos 1}^2-1<\left(\frac{8}{9}\right)-1$$
102	97 101	mpbi	$$⊢2{\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{\cos 1}^2-1<-\frac{1}{9}$$
118	71 117	eqbrtri	$$⊢\cos 2<-\frac{1}{9}$$
119	72 118	pm3.2i	$$⊢\left(-\frac{7}{9}<\cos 2\wedge \cos 2<-\frac{1}{9}\right)$$