Metamath Proof Explorer

Theorem cos2bnd

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

Ref Expression
Assertion cos2bnd ( - ( 7 / 9 ) < ( cos ‘ 2 ) ∧ ( cos ‘ 2 ) < - ( 1 / 9 ) )

Proof

Step Hyp Ref Expression
1 7cn ⊢ 7 ∈ ℂ
2 9cn ⊢ 9 ∈ ℂ
3 9re ⊢ 9 ∈ ℝ
4 9pos ⊢ 0 < 9
5 3 4 gt0ne0ii ⊢ 9 ≠ 0
6 divneg ⊢ ( ( 7 ∈ ℂ ∧ 9 ∈ ℂ ∧ 9 ≠ 0 ) → - ( 7 / 9 ) = ( - 7 / 9 ) )
7 1 2 5 6 mp3an ⊢ - ( 7 / 9 ) = ( - 7 / 9 )
8 2cn ⊢ 2 ∈ ℂ
9 2 5 pm3.2i ⊢ ( 9 ∈ ℂ ∧ 9 ≠ 0 )
10 divsubdir ⊢ ( ( 2 ∈ ℂ ∧ 9 ∈ ℂ ∧ ( 9 ∈ ℂ ∧ 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 ⊢ - ( 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 ⊢ - ( 9 − 2 ) = - 7
17 12 16 eqtr3i ⊢ ( 2 − 9 ) = - 7
18 17 oveq1i ⊢ ( ( 2 − 9 ) / 9 ) = ( - 7 / 9 )
19 11 18 eqtr3i ⊢ ( ( 2 / 9 ) − ( 9 / 9 ) ) = ( - 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 ) = - ( 7 / 9 )
23 ax-1cn ⊢ 1 ∈ ℂ
24 8 23 2 5 divassi ⊢ ( ( 2 · 1 ) / 9 ) = ( 2 · ( 1 / 9 ) )
25 2t1e2 ⊢ ( 2 · 1 ) = 2
26 25 oveq1i ⊢ ( ( 2 · 1 ) / 9 ) = ( 2 / 9 )
27 24 26 eqtr3i ⊢ ( 2 · ( 1 / 9 ) ) = ( 2 / 9 )
28 3cn ⊢ 3 ∈ ℂ
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 ∈ ℝ
40 3re ⊢ 3 ∈ ℝ
41 39 40 divge0i ⊢ ( ( 0 ≤ 1 ∧ 0 < 3 ) → 0 ≤ ( 1 / 3 ) )
42 37 38 41 mp2an ⊢ 0 ≤ ( 1 / 3 )
43 0re ⊢ 0 ∈ ℝ
44 recoscl ⊢ ( 1 ∈ ℝ → ( cos ‘ 1 ) ∈ ℝ )
45 39 44 ax-mp ⊢ ( cos ‘ 1 ) ∈ ℝ
46 40 29 rereccli ⊢ ( 1 / 3 ) ∈ ℝ
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 ) ∈ ℝ
56 45 resqcli ⊢ ( ( cos ‘ 1 ) ↑ 2 ) ∈ ℝ
57 2re ⊢ 2 ∈ ℝ
58 55 56 57 ltmul2i ⊢ ( 0 < 2 → ( ( 1 / 9 ) < ( ( cos ‘ 1 ) ↑ 2 ) ↔ ( 2 · ( 1 / 9 ) ) < ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) ) )
59 54 58 ax-mp ⊢ ( ( 1 / 9 ) < ( ( cos ‘ 1 ) ↑ 2 ) ↔ ( 2 · ( 1 / 9 ) ) < ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) )
60 53 59 mpbi ⊢ ( 2 · ( 1 / 9 ) ) < ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) )
61 27 60 eqbrtrri ⊢ ( 2 / 9 ) < ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) )
62 57 3 5 redivcli ⊢ ( 2 / 9 ) ∈ ℝ
63 57 56 remulcli ⊢ ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) ∈ ℝ
64 ltsub1 ⊢ ( ( ( 2 / 9 ) ∈ ℝ ∧ ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 2 / 9 ) < ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) ↔ ( ( 2 / 9 ) − 1 ) < ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 ) ) )
65 62 63 39 64 mp3an ⊢ ( ( 2 / 9 ) < ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) ↔ ( ( 2 / 9 ) − 1 ) < ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 ) )
66 61 65 mpbi ⊢ ( ( 2 / 9 ) − 1 ) < ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 )
67 22 66 eqbrtrri ⊢ - ( 7 / 9 ) < ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 )
68 25 fveq2i ⊢ ( cos ‘ ( 2 · 1 ) ) = ( cos ‘ 2 )
69 cos2t ⊢ ( 1 ∈ ℂ → ( cos ‘ ( 2 · 1 ) ) = ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 ) )
70 23 69 ax-mp ⊢ ( cos ‘ ( 2 · 1 ) ) = ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 )
71 68 70 eqtr3i ⊢ ( cos ‘ 2 ) = ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 )
72 67 71 breqtrri ⊢ - ( 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 ) ∈ ℝ
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 ∈ ℝ
87 86 3 5 redivcli ⊢ ( 4 / 9 ) ∈ ℝ
88 56 87 57 ltmul2i ⊢ ( 0 < 2 → ( ( ( cos ‘ 1 ) ↑ 2 ) < ( 4 / 9 ) ↔ ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) < ( 2 · ( 4 / 9 ) ) ) )
89 54 88 ax-mp ⊢ ( ( ( cos ‘ 1 ) ↑ 2 ) < ( 4 / 9 ) ↔ ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) < ( 2 · ( 4 / 9 ) ) )
90 85 89 mpbi ⊢ ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) < ( 2 · ( 4 / 9 ) )
91 4cn ⊢ 4 ∈ ℂ
92 8 91 2 5 divassi ⊢ ( ( 2 · 4 ) / 9 ) = ( 2 · ( 4 / 9 ) )
93 4t2e8 ⊢ ( 4 · 2 ) = 8
94 91 8 93 mulcomli ⊢ ( 2 · 4 ) = 8
95 94 oveq1i ⊢ ( ( 2 · 4 ) / 9 ) = ( 8 / 9 )
96 92 95 eqtr3i ⊢ ( 2 · ( 4 / 9 ) ) = ( 8 / 9 )
97 90 96 breqtri ⊢ ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) < ( 8 / 9 )
98 8re ⊢ 8 ∈ ℝ
99 98 3 5 redivcli ⊢ ( 8 / 9 ) ∈ ℝ
100 ltsub1 ⊢ ( ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) ∈ ℝ ∧ ( 8 / 9 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) < ( 8 / 9 ) ↔ ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 ) < ( ( 8 / 9 ) − 1 ) ) )
101 63 99 39 100 mp3an ⊢ ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) < ( 8 / 9 ) ↔ ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 ) < ( ( 8 / 9 ) − 1 ) )
102 97 101 mpbi ⊢ ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 ) < ( ( 8 / 9 ) − 1 )
103 20 oveq2i ⊢ ( ( 8 / 9 ) − ( 9 / 9 ) ) = ( ( 8 / 9 ) − 1 )
104 divneg ⊢ ( ( 1 ∈ ℂ ∧ 9 ∈ ℂ ∧ 9 ≠ 0 ) → - ( 1 / 9 ) = ( - 1 / 9 ) )
105 23 2 5 104 mp3an ⊢ - ( 1 / 9 ) = ( - 1 / 9 )
106 8cn ⊢ 8 ∈ ℂ
107 2 106 negsubdi2i ⊢ - ( 9 − 8 ) = ( 8 − 9 )
108 8p1e9 ⊢ ( 8 + 1 ) = 9
109 2 106 23 108 subaddrii ⊢ ( 9 − 8 ) = 1
110 109 negeqi ⊢ - ( 9 − 8 ) = - 1
111 107 110 eqtr3i ⊢ ( 8 − 9 ) = - 1
112 111 oveq1i ⊢ ( ( 8 − 9 ) / 9 ) = ( - 1 / 9 )
113 divsubdir ⊢ ( ( 8 ∈ ℂ ∧ 9 ∈ ℂ ∧ ( 9 ∈ ℂ ∧ 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 ) ) = - ( 1 / 9 )
116 103 115 eqtr3i ⊢ ( ( 8 / 9 ) − 1 ) = - ( 1 / 9 )
117 102 116 breqtri ⊢ ( ( 2 · ( ( cos ‘ 1 ) ↑ 2 ) ) − 1 ) < - ( 1 / 9 )
118 71 117 eqbrtri ⊢ ( cos ‘ 2 ) < - ( 1 / 9 )
119 72 118 pm3.2i ⊢ ( - ( 7 / 9 ) < ( cos ‘ 2 ) ∧ ( cos ‘ 2 ) < - ( 1 / 9 ) )