This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 x. ( ( 1 ^ 2 ) / 3 ) ) = ( 2 x. ( 1 / 3 ) )
4 2cn 
 |-  2 e. CC
5 3cn 
 |-  3 e. CC
6 3ne0 
 |-  3 =/= 0
7 4 5 6 divreci 
 |-  ( 2 / 3 ) = ( 2 x. ( 1 / 3 ) )
8 3 7 eqtr4i 
 |-  ( 2 x. ( ( 1 ^ 2 ) / 3 ) ) = ( 2 / 3 )
9 8 oveq2i 
 |-  ( 1 - ( 2 x. ( ( 1 ^ 2 ) / 3 ) ) ) = ( 1 - ( 2 / 3 ) )
10 ax-1cn 
 |-  1 e. CC
11 4 5 6 divcli 
 |-  ( 2 / 3 ) e. CC
12 5 6 reccli 
 |-  ( 1 / 3 ) e. CC
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 x. ( ( 1 ^ 2 ) / 3 ) ) ) = ( 1 / 3 )
20 1re 
 |-  1 e. RR
21 0lt1 
 |-  0 < 1
22 1le1 
 |-  1 <_ 1
23 0xr 
 |-  0 e. RR*
24 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( 1 e. ( 0 (,] 1 ) <-> ( 1 e. RR /\ 0 < 1 /\ 1 <_ 1 ) ) )
25 23 20 24 mp2an 
 |-  ( 1 e. ( 0 (,] 1 ) <-> ( 1 e. RR /\ 0 < 1 /\ 1 <_ 1 ) )
26 cos01bnd 
 |-  ( 1 e. ( 0 (,] 1 ) -> ( ( 1 - ( 2 x. ( ( 1 ^ 2 ) / 3 ) ) ) < ( cos ` 1 ) /\ ( cos ` 1 ) < ( 1 - ( ( 1 ^ 2 ) / 3 ) ) ) )
27 25 26 sylbir 
 |-  ( ( 1 e. RR /\ 0 < 1 /\ 1 <_ 1 ) -> ( ( 1 - ( 2 x. ( ( 1 ^ 2 ) / 3 ) ) ) < ( cos ` 1 ) /\ ( cos ` 1 ) < ( 1 - ( ( 1 ^ 2 ) / 3 ) ) ) )
28 20 21 22 27 mp3an 
 |-  ( ( 1 - ( 2 x. ( ( 1 ^ 2 ) / 3 ) ) ) < ( cos ` 1 ) /\ ( cos ` 1 ) < ( 1 - ( ( 1 ^ 2 ) / 3 ) ) )
29 28 simpli 
 |-  ( 1 - ( 2 x. ( ( 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 ) )