Metamath Proof Explorer

Theorem cos0pilt1

Description: Cosine is between minus one and one on the open interval between zero and _pi . (Contributed by Jim Kingdon, 7-May-2024)

Ref Expression
Assertion cos0pilt1 
|- ( A e. ( 0 (,) _pi ) -> ( cos ` A ) e. ( -u 1 (,) 1 ) )

Proof

Step Hyp Ref Expression
1 elioore 
 |-  ( A e. ( 0 (,) _pi ) -> A e. RR )
2 1 recoscld 
 |-  ( A e. ( 0 (,) _pi ) -> ( cos ` A ) e. RR )
3 cospi 
 |-  ( cos ` _pi ) = -u 1
4 ioossicc 
 |-  ( 0 (,) _pi ) C_ ( 0 [,] _pi )
5 4 sseli 
 |-  ( A e. ( 0 (,) _pi ) -> A e. ( 0 [,] _pi ) )
6 0xr 
 |-  0 e. RR*
7 pire 
 |-  _pi e. RR
8 7 rexri 
 |-  _pi e. RR*
9 0re 
 |-  0 e. RR
10 pipos 
 |-  0 < _pi
11 9 7 10 ltleii 
 |-  0 <_ _pi
12 ubicc2 
 |-  ( ( 0 e. RR* /\ _pi e. RR* /\ 0 <_ _pi ) -> _pi e. ( 0 [,] _pi ) )
13 6 8 11 12 mp3an 
 |-  _pi e. ( 0 [,] _pi )
14 13 a1i 
 |-  ( A e. ( 0 (,) _pi ) -> _pi e. ( 0 [,] _pi ) )
15 eliooord 
 |-  ( A e. ( 0 (,) _pi ) -> ( 0 < A /\ A < _pi ) )
16 15 simprd 
 |-  ( A e. ( 0 (,) _pi ) -> A < _pi )
17 5 14 16 cosordlem 
 |-  ( A e. ( 0 (,) _pi ) -> ( cos ` _pi ) < ( cos ` A ) )
18 3 17 eqbrtrrid 
 |-  ( A e. ( 0 (,) _pi ) -> -u 1 < ( cos ` A ) )
19 2re 
 |-  2 e. RR
20 19 7 remulcli 
 |-  ( 2 x. _pi ) e. RR
21 20 rexri 
 |-  ( 2 x. _pi ) e. RR*
22 1le2 
 |-  1 <_ 2
23 lemulge12 
 |-  ( ( ( _pi e. RR /\ 2 e. RR ) /\ ( 0 <_ _pi /\ 1 <_ 2 ) ) -> _pi <_ ( 2 x. _pi ) )
24 7 19 11 22 23 mp4an 
 |-  _pi <_ ( 2 x. _pi )
25 iooss2 
 |-  ( ( ( 2 x. _pi ) e. RR* /\ _pi <_ ( 2 x. _pi ) ) -> ( 0 (,) _pi ) C_ ( 0 (,) ( 2 x. _pi ) ) )
26 21 24 25 mp2an 
 |-  ( 0 (,) _pi ) C_ ( 0 (,) ( 2 x. _pi ) )
27 26 sseli 
 |-  ( A e. ( 0 (,) _pi ) -> A e. ( 0 (,) ( 2 x. _pi ) ) )
28 cos02pilt1 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( cos ` A ) < 1 )
29 27 28 syl 
 |-  ( A e. ( 0 (,) _pi ) -> ( cos ` A ) < 1 )
30 neg1rr 
 |-  -u 1 e. RR
31 30 rexri 
 |-  -u 1 e. RR*
32 1re 
 |-  1 e. RR
33 32 rexri 
 |-  1 e. RR*
34 elioo2 
 |-  ( ( -u 1 e. RR* /\ 1 e. RR* ) -> ( ( cos ` A ) e. ( -u 1 (,) 1 ) <-> ( ( cos ` A ) e. RR /\ -u 1 < ( cos ` A ) /\ ( cos ` A ) < 1 ) ) )
35 31 33 34 mp2an 
 |-  ( ( cos ` A ) e. ( -u 1 (,) 1 ) <-> ( ( cos ` A ) e. RR /\ -u 1 < ( cos ` A ) /\ ( cos ` A ) < 1 ) )
36 2 18 29 35 syl3anbrc 
 |-  ( A e. ( 0 (,) _pi ) -> ( cos ` A ) e. ( -u 1 (,) 1 ) )