Theorem cos1bnd

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

	Ref	Expression
Assertion	cos1bnd	$$⊢\left(\frac{1}{3}<\cos 1\wedge \cos 1<\frac{2}{3}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sq1	$$⊢1^2=1$$
2	1	oveq1i	$$⊢\frac{1^2}{3}=\frac{1}{3}$$
3	2	oveq2i	$$⊢2\left(\frac{1^2}{3}\right)=2\left(\frac{1}{3}\right)$$
4		2cn	$$⊢2\in ℂ$$
5		3cn	$$⊢3\in ℂ$$
6		3ne0	$$⊢3\ne 0$$
7	4 5 6	divreci	$$⊢\frac{2}{3}=2\left(\frac{1}{3}\right)$$
8	3 7	eqtr4i	$$⊢2\left(\frac{1^2}{3}\right)=\frac{2}{3}$$
9	8	oveq2i	$$⊢1-2\left(\frac{1^2}{3}\right)=1-\left(\frac{2}{3}\right)$$
10		ax-1cn	$$⊢1\in ℂ$$
11	4 5 6	divcli	$$⊢\frac{2}{3}\in ℂ$$
12	5 6	reccli	$$⊢\frac{1}{3}\in ℂ$$
13		df-3	$$⊢3=2+1$$
14	13	oveq1i	$$⊢\frac{3}{3}=\frac{2+1}{3}$$
15	5 6	dividi	$$⊢\frac{3}{3}=1$$
16	4 10 5 6	divdiri	$$⊢\frac{2+1}{3}=\left(\frac{2}{3}\right)+\left(\frac{1}{3}\right)$$
17	14 15 16	3eqtr3ri	$$⊢\left(\frac{2}{3}\right)+\left(\frac{1}{3}\right)=1$$
18	10 11 12 17	subaddrii	$$⊢1-\left(\frac{2}{3}\right)=\frac{1}{3}$$
19	9 18	eqtri	$$⊢1-2\left(\frac{1^2}{3}\right)=\frac{1}{3}$$
20		1re	$$⊢1\in ℝ$$
21		0lt1	$$⊢0<1$$
22		1le1	$$⊢1\le 1$$
23		0xr	$$⊢0\in {ℝ}^{*}$$
24		elioc2	$$⊢\left(0\in {ℝ}^{*}\wedge 1\in ℝ\right)\to \left(1\in \left(0,1\right]\leftrightarrow \left(1\in ℝ\wedge 0<1\wedge 1\le 1\right)\right)$$
25	23 20 24	mp2an	$$⊢1\in \left(0,1\right]\leftrightarrow \left(1\in ℝ\wedge 0<1\wedge 1\le 1\right)$$
26		cos01bnd	$$⊢1\in \left(0,1\right]\to \left(1-2\left(\frac{1^2}{3}\right)<\cos 1\wedge \cos 1<1-\left(\frac{1^2}{3}\right)\right)$$
27	25 26	sylbir	$$⊢\left(1\in ℝ\wedge 0<1\wedge 1\le 1\right)\to \left(1-2\left(\frac{1^2}{3}\right)<\cos 1\wedge \cos 1<1-\left(\frac{1^2}{3}\right)\right)$$
28	20 21 22 27	mp3an	$$⊢\left(1-2\left(\frac{1^2}{3}\right)<\cos 1\wedge \cos 1<1-\left(\frac{1^2}{3}\right)\right)$$
29	28	simpli	$$⊢1-2\left(\frac{1^2}{3}\right)<\cos 1$$
30	19 29	eqbrtrri	$$⊢\frac{1}{3}<\cos 1$$
31	28	simpri	$$⊢\cos 1<1-\left(\frac{1^2}{3}\right)$$
32	2	oveq2i	$$⊢1-\left(\frac{1^2}{3}\right)=1-\left(\frac{1}{3}\right)$$
33	10 12 11	subadd2i	$$⊢1-\left(\frac{1}{3}\right)=\frac{2}{3}\leftrightarrow \left(\frac{2}{3}\right)+\left(\frac{1}{3}\right)=1$$
34	17 33	mpbir	$$⊢1-\left(\frac{1}{3}\right)=\frac{2}{3}$$
35	32 34	eqtri	$$⊢1-\left(\frac{1^2}{3}\right)=\frac{2}{3}$$
36	31 35	breqtri	$$⊢\cos 1<\frac{2}{3}$$
37	30 36	pm3.2i	$$⊢\left(\frac{1}{3}<\cos 1\wedge \cos 1<\frac{2}{3}\right)$$