Metamath Proof Explorer

Theorem cos1bnd

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

Ref Expression
Assertion cos1bnd ( ( 1 / 3 ) < ( cos ‘ 1 ) ∧ ( cos ‘ 1 ) < ( 2 / 3 ) )

Proof

Step Hyp Ref Expression
1 sq1 ⊢ ( 1 ↑ 2 ) = 1
2 1 oveq1i ⊢ ( ( 1 ↑ 2 ) / 3 ) = ( 1 / 3 )
3 2 oveq2i ⊢ ( 2 · ( ( 1 ↑ 2 ) / 3 ) ) = ( 2 · ( 1 / 3 ) )
4 2cn ⊢ 2 ∈ ℂ
5 3cn ⊢ 3 ∈ ℂ
6 3ne0 ⊢ 3 ≠ 0
7 4 5 6 divreci ⊢ ( 2 / 3 ) = ( 2 · ( 1 / 3 ) )
8 3 7 eqtr4i ⊢ ( 2 · ( ( 1 ↑ 2 ) / 3 ) ) = ( 2 / 3 )
9 8 oveq2i ⊢ ( 1 − ( 2 · ( ( 1 ↑ 2 ) / 3 ) ) ) = ( 1 − ( 2 / 3 ) )
10 ax-1cn ⊢ 1 ∈ ℂ
11 4 5 6 divcli ⊢ ( 2 / 3 ) ∈ ℂ
12 5 6 reccli ⊢ ( 1 / 3 ) ∈ ℂ
13 df-3 ⊢ 3 = ( 2 + 1 )
14 13 oveq1i ⊢ ( 3 / 3 ) = ( ( 2 + 1 ) / 3 )
15 5 6 dividi ⊢ ( 3 / 3 ) = 1
16 4 10 5 6 divdiri ⊢ ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
17 14 15 16 3eqtr3ri ⊢ ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1
18 10 11 12 17 subaddrii ⊢ ( 1 − ( 2 / 3 ) ) = ( 1 / 3 )
19 9 18 eqtri ⊢ ( 1 − ( 2 · ( ( 1 ↑ 2 ) / 3 ) ) ) = ( 1 / 3 )
20 1re ⊢ 1 ∈ ℝ
21 0lt1 ⊢ 0 < 1
22 1le1 ⊢ 1 ≤ 1
23 0xr ⊢ 0 ∈ ℝ*
24 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 1 ∈ ( 0 (,] 1 ) ↔ ( 1 ∈ ℝ ∧ 0 < 1 ∧ 1 ≤ 1 ) ) )
25 23 20 24 mp2an ⊢ ( 1 ∈ ( 0 (,] 1 ) ↔ ( 1 ∈ ℝ ∧ 0 < 1 ∧ 1 ≤ 1 ) )
26 cos01bnd ⊢ ( 1 ∈ ( 0 (,] 1 ) → ( ( 1 − ( 2 · ( ( 1 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 1 ) ∧ ( cos ‘ 1 ) < ( 1 − ( ( 1 ↑ 2 ) / 3 ) ) ) )
27 25 26 sylbir ⊢ ( ( 1 ∈ ℝ ∧ 0 < 1 ∧ 1 ≤ 1 ) → ( ( 1 − ( 2 · ( ( 1 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 1 ) ∧ ( cos ‘ 1 ) < ( 1 − ( ( 1 ↑ 2 ) / 3 ) ) ) )
28 20 21 22 27 mp3an ⊢ ( ( 1 − ( 2 · ( ( 1 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 1 ) ∧ ( cos ‘ 1 ) < ( 1 − ( ( 1 ↑ 2 ) / 3 ) ) )
29 28 simpli ⊢ ( 1 − ( 2 · ( ( 1 ↑ 2 ) / 3 ) ) ) < ( cos ‘ 1 )
30 19 29 eqbrtrri ⊢ ( 1 / 3 ) < ( cos ‘ 1 )
31 28 simpri ⊢ ( cos ‘ 1 ) < ( 1 − ( ( 1 ↑ 2 ) / 3 ) )
32 2 oveq2i ⊢ ( 1 − ( ( 1 ↑ 2 ) / 3 ) ) = ( 1 − ( 1 / 3 ) )
33 10 12 11 subadd2i ⊢ ( ( 1 − ( 1 / 3 ) ) = ( 2 / 3 ) ↔ ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1 )
34 17 33 mpbir ⊢ ( 1 − ( 1 / 3 ) ) = ( 2 / 3 )
35 32 34 eqtri ⊢ ( 1 − ( ( 1 ↑ 2 ) / 3 ) ) = ( 2 / 3 )
36 31 35 breqtri ⊢ ( cos ‘ 1 ) < ( 2 / 3 )
37 30 36 pm3.2i ⊢ ( ( 1 / 3 ) < ( cos ‘ 1 ) ∧ ( cos ‘ 1 ) < ( 2 / 3 ) )