Theorem cos2bnd 7475

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

Assertion

Ref	Expression
cos2bnd	|- (-u(7 / 9) < (cos` 2) /\ (cos` 2) < -u(1 / 9))

Proof of Theorem cos2bnd

Step	Hyp	Ref	Expression
1		2cn 5980	. . . . . . 7 |- 2 e. CC
2		9re 5987	. . . . . . . 8 |- 9 e. RR
3	2	recn 5314	. . . . . . 7 |- 9 e. CC
4		9pos 5997	. . . . . . . . 9 |- 0 < 9
5	2, 4	gt0ne0i 5617	. . . . . . . 8 |- 9 =/= 0
6		divsubdirtOLD 5775	. . . . . . . 8 |- (((2 e. CC /\ 9 e. CC /\ 9 e. CC) /\ 9 =/= 0) -> ((2 - 9) / 9) = ((2 / 9) - (9 / 9)))
7	5, 6	mpan2 696	. . . . . . 7 |- ((2 e. CC /\ 9 e. CC /\ 9 e. CC) -> ((2 - 9) / 9) = ((2 / 9) - (9 / 9)))
8	1, 3, 3, 7	mp3an 916	. . . . . 6 |- ((2 - 9) / 9) = ((2 / 9) - (9 / 9))
9	3, 1	negsubdi2 5450	. . . . . . . 8 |- -u(9 - 2) = (2 - 9)
10		7re 5985	. . . . . . . . . . . . . 14 |- 7 e. RR
11	10	recn 5314	. . . . . . . . . . . . 13 |- 7 e. CC
12		ax1cn 5269	. . . . . . . . . . . . 13 |- 1 e. CC
13	11, 12, 12	addass 5324	. . . . . . . . . . . 12 |- ((7 + 1) + 1) = (7 + (1 + 1))
14		df-8 5976	. . . . . . . . . . . . 13 |- 8 = (7 + 1)
15	14	opreq1i 3971	. . . . . . . . . . . 12 |- (8 + 1) = ((7 + 1) + 1)
16		df-2 5970	. . . . . . . . . . . . 13 |- 2 = (1 + 1)
17	16	opreq2i 3972	. . . . . . . . . . . 12 |- (7 + 2) = (7 + (1 + 1))
18	13, 15, 17	3eqtr4r 1506	. . . . . . . . . . 11 |- (7 + 2) = (8 + 1)
19		df-9 5977	. . . . . . . . . . 11 |- 9 = (8 + 1)
20	18, 19	eqtr4 1498	. . . . . . . . . 10 |- (7 + 2) = 9
21	3, 1, 11	subadd2 5373	. . . . . . . . . 10 |- ((9 - 2) = 7 <-> (7 + 2) = 9)
22	20, 21	mpbir 190	. . . . . . . . 9 |- (9 - 2) = 7
23	22	negeqi 5360	. . . . . . . 8 |- -u(9 - 2) = -u7
24	9, 23	eqtr3 1497	. . . . . . 7 |- (2 - 9) = -u7
25	24	opreq1i 3971	. . . . . 6 |- ((2 - 9) / 9) = (-u7 / 9)
26	3, 5	divid 5770	. . . . . . 7 |- (9 / 9) = 1
27	26	opreq2i 3972	. . . . . 6 |- ((2 / 9) - (9 / 9)) = ((2 / 9) - 1)
28	8, 25, 27	3eqtr3r 1504	. . . . 5 |- ((2 / 9) - 1) = (-u7 / 9)
29		divnegt 5774	. . . . . 6 |- ((7 e. CC /\ 9 e. CC /\ 9 =/= 0) -> -u(7 / 9) = (-u7 / 9))
30	11, 3, 5, 29	mp3an 916	. . . . 5 |- -u(7 / 9) = (-u7 / 9)
31	28, 30	eqtr4 1498	. . . 4 |- ((2 / 9) - 1) = -u(7 / 9)
32	1, 12, 3, 5	divass 5746	. . . . . . 7 |- ((2 x. 1) / 9) = (2 x. (1 / 9))
33	1	mulid1 5332	. . . . . . . 8 |- (2 x. 1) = 2
34	33	opreq1i 3971	. . . . . . 7 |- ((2 x. 1) / 9) = (2 / 9)
35	32, 34	eqtr3 1497	. . . . . 6 |- (2 x. (1 / 9)) = (2 / 9)
36		3re 5981	. . . . . . . . . . 11 |- 3 e. RR
37	36	recn 5314	. . . . . . . . . 10 |- 3 e. CC
38		3nn 6000	. . . . . . . . . . 11 |- 3 e. NN
39	38	nnne0 5951	. . . . . . . . . 10 |- 3 =/= 0
40	12, 37, 39	sqdiv 6618	. . . . . . . . 9 |- ((1 / 3)^2) = ((1^2) / (3^2))
41		sq1 6637	. . . . . . . . . 10 |- (1^2) = 1
42		sq3 6639	. . . . . . . . . 10 |- (3^2) = 9
43	41, 42	opreq12i 3973	. . . . . . . . 9 |- ((1^2) / (3^2)) = (1 / 9)
44	40, 43	eqtr 1495	. . . . . . . 8 |- ((1 / 3)^2) = (1 / 9)
45		cos1bnd 7474	. . . . . . . . . 10 |- ((1 / 3) < (cos` 1) /\ (cos` 1) < (2 / 3))
46	45	pm3.26i 320	. . . . . . . . 9 |- (1 / 3) < (cos` 1)
47		1nn0 6114	. . . . . . . . . . . 12 |- 1 e. NN0
48	47	nn0ge0 6118	. . . . . . . . . . 11 |- 0 <_ 1
49	38	nngt0 5950	. . . . . . . . . . 11 |- 0 < 3
50		1re 5435	. . . . . . . . . . . 12 |- 1 e. RR
51	50, 36	divge0 5858	. . . . . . . . . . 11 |- ((0 <_ 1 /\ 0 < 3) -> 0 <_ (1 / 3))
52	48, 49, 51	mp2an 697	. . . . . . . . . 10 |- 0 <_ (1 / 3)
53		0re 5440	. . . . . . . . . . 11 |- 0 e. RR
54		recosclt 7439	. . . . . . . . . . . 12 |- (1 e. RR -> (cos` 1) e. RR)
55	50, 54	ax-mp 7	. . . . . . . . . . 11 |- (cos` 1) e. RR
56	36, 39	rereccl 5801	. . . . . . . . . . . . 13 |- (1 / 3) e. RR
57	53, 56, 55	lelttr 5586	. . . . . . . . . . . 12 |- ((0 <_ (1 / 3) /\ (1 / 3) < (cos` 1)) -> 0 < (cos` 1))
58	52, 46, 57	mp2an 697	. . . . . . . . . . 11 |- 0 < (cos` 1)
59	53, 55, 58	ltlei 5581	. . . . . . . . . 10 |- 0 <_ (cos` 1)
60	56, 55	lt2sq 6624	. . . . . . . . . 10 |- ((0 <_ (1 / 3) /\ 0 <_ (cos` 1)) -> ((1 / 3) < (cos` 1) <-> ((1 / 3)^2) < ((cos` 1)^2)))
61	52, 59, 60	mp2an 697	. . . . . . . . 9 |- ((1 / 3) < (cos` 1) <-> ((1 / 3)^2) < ((cos` 1)^2))
62	46, 61	mpbi 189	. . . . . . . 8 |- ((1 / 3)^2) < ((cos` 1)^2)
63	44, 62	eqbrtrr 2636	. . . . . . 7 |- (1 / 9) < ((cos` 1)^2)
64		2pos 5989	. . . . . . . 8 |- 0 < 2
65	2, 5	rereccl 5801	. . . . . . . . 9 |- (1 / 9) e. RR
66	55	resqcl 6623	. . . . . . . . 9 |- ((cos` 1)^2) e. RR
67		2re 5979	. . . . . . . . 9 |- 2 e. RR
68	65, 66, 67	ltmul2 5834	. . . . . . . 8 |- (0 < 2 -> ((1 / 9) < ((cos` 1)^2) <-> (2 x. (1 / 9)) < (2 x. ((cos` 1)^2))))
69	64, 68	ax-mp 7	. . . . . . 7 |- ((1 / 9) < ((cos` 1)^2) <-> (2 x. (1 / 9)) < (2 x. ((cos` 1)^2)))
70	63, 69	mpbi 189	. . . . . 6 |- (2 x. (1 / 9)) < (2 x. ((cos` 1)^2))
71	35, 70	eqbrtrr 2636	. . . . 5 |- (2 / 9) < (2 x. ((cos` 1)^2))
72	67, 2, 5	redivcl 5798	. . . . . 6 |- (2 / 9) e. RR
73	67, 66	remulcl 5335	. . . . . 6 |- (2 x. ((cos` 1)^2)) e. RR
74		ltsub1t 5662	. . . . . 6 |- (((2 / 9) e. RR /\ (2 x. ((cos` 1)^2)) e. RR /\ 1 e. RR) -> ((2 / 9) < (2 x. ((cos` 1)^2)) <-> ((2 / 9) - 1) < ((2 x. ((cos` 1)^2)) - 1)))
75	72, 73, 50, 74	mp3an 916	. . . . 5 |- ((2 / 9) < (2 x. ((cos` 1)^2)) <-> ((2 / 9) - 1) < ((2 x. ((cos` 1)^2)) - 1))
76	71, 75	mpbi 189	. . . 4 |- ((2 / 9) - 1) < ((2 x. ((cos` 1)^2)) - 1)
77	31, 76	eqbrtrr 2636	. . 3 |- -u(7 / 9) < ((2 x. ((cos` 1)^2)) - 1)
78	33	fveq2i 3727	. . . 4 |- (cos` (2 x. 1)) = (cos` 2)
79	12	cos2tOLD 7464	. . . 4 |- (cos` (2 x. 1)) = ((2 x. ((cos` 1)^2)) - 1)
80	78, 79	eqtr3 1497	. . 3 |- (cos` 2) = ((2 x. ((cos` 1)^2)) - 1)
81	77, 80	breqtrr 2640	. 2 |- -u(7 / 9) < (cos` 2)
82	45	pm3.27i 324	. . . . . . . . 9 |- (cos` 1) < (2 / 3)
83		2nn0 6115	. . . . . . . . . . . 12 |- 2 e. NN0
84	83	nn0ge0 6118	. . . . . . . . . . 11 |- 0 <_ 2
85	67, 36	divge0 5858	. . . . . . . . . . 11 |- ((0 <_ 2 /\ 0 < 3) -> 0 <_ (2 / 3))
86	84, 49, 85	mp2an 697	. . . . . . . . . 10 |- 0 <_ (2 / 3)
87	67, 36, 39	redivcl 5798	. . . . . . . . . . 11 |- (2 / 3) e. RR
88	55, 87	lt2sq 6624	. . . . . . . . . 10 |- ((0 <_ (cos` 1) /\ 0 <_ (2 / 3)) -> ((cos` 1) < (2 / 3) <-> ((cos` 1)^2) < ((2 / 3)^2)))
89	59, 86, 88	mp2an 697	. . . . . . . . 9 |- ((cos` 1) < (2 / 3) <-> ((cos` 1)^2) < ((2 / 3)^2))
90	82, 89	mpbi 189	. . . . . . . 8 |- ((cos` 1)^2) < ((2 / 3)^2)
91	1, 37, 39	sqdiv 6618	. . . . . . . . 9 |- ((2 / 3)^2) = ((2^2) / (3^2))
92		sq2 6638	. . . . . . . . . 10 |- (2^2) = 4
93	92, 42	opreq12i 3973	. . . . . . . . 9 |- ((2^2) / (3^2)) = (4 / 9)
94	91, 93	eqtr 1495	. . . . . . . 8 |- ((2 / 3)^2) = (4 / 9)
95	90, 94	breqtr 2638	. . . . . . 7 |- ((cos` 1)^2) < (4 / 9)
96		4re 5982	. . . . . . . . . 10 |- 4 e. RR
97	96, 2, 5	redivcl 5798	. . . . . . . . 9 |- (4 / 9) e. RR
98	66, 97, 67	ltmul2 5834	. . . . . . . 8 |- (0 < 2 -> (((cos` 1)^2) < (4 / 9) <-> (2 x. ((cos` 1)^2)) < (2 x. (4 / 9))))
99	64, 98	ax-mp 7	. . . . . . 7 |- (((cos` 1)^2) < (4 / 9) <-> (2 x. ((cos` 1)^2)) < (2 x. (4 / 9)))
100	95, 99	mpbi 189	. . . . . 6 |- (2 x. ((cos` 1)^2)) < (2 x. (4 / 9))
101	96	recn 5314	. . . . . . . 8 |- 4 e. CC
102	1, 101, 3, 5	divass 5746	. . . . . . 7 |- ((2 x. 4) / 9) = (2 x. (4 / 9))
103	1, 101	mulcom 5323	. . . . . . . . 9 |- (2 x. 4) = (4 x. 2)
104		4t2e8 6025	. . . . . . . . 9 |- (4 x. 2) = 8
105	103, 104	eqtr 1495	. . . . . . . 8 |- (2 x. 4) = 8
106	105	opreq1i 3971	. . . . . . 7 |- ((2 x. 4) / 9) = (8 / 9)
107	102, 106	eqtr3 1497	. . . . . 6 |- (2 x. (4 / 9)) = (8 / 9)
108	100, 107	breqtr 2638	. . . . 5 |- (2 x. ((cos` 1)^2)) < (8 / 9)
109		8re 5986	. . . . . . 7 |- 8 e. RR
110	109, 2, 5	redivcl