Metamath Proof Explorer

Theorem cos2bnd

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

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

Proof

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