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 pige0 
 |-  0 <_ _pi
10 ubicc2 
 |-  ( ( 0 e. RR* /\ _pi e. RR* /\ 0 <_ _pi ) -> _pi e. ( 0 [,] _pi ) )
11 6 8 9 10 mp3an 
 |-  _pi e. ( 0 [,] _pi )
12 11 a1i 
 |-  ( A e. ( 0 (,) _pi ) -> _pi e. ( 0 [,] _pi ) )
13 eliooord 
 |-  ( A e. ( 0 (,) _pi ) -> ( 0 < A /\ A < _pi ) )
14 13 simprd 
 |-  ( A e. ( 0 (,) _pi ) -> A < _pi )
15 5 12 14 cosordlem 
 |-  ( A e. ( 0 (,) _pi ) -> ( cos ` _pi ) < ( cos ` A ) )
16 3 15 eqbrtrrid 
 |-  ( A e. ( 0 (,) _pi ) -> -u 1 < ( cos ` A ) )
17 2pire 
 |-  ( 2 x. _pi ) e. RR
18 17 rexri 
 |-  ( 2 x. _pi ) e. RR*
19 2re 
 |-  2 e. RR
20 1le2 
 |-  1 <_ 2
21 lemulge12 
 |-  ( ( ( _pi e. RR /\ 2 e. RR ) /\ ( 0 <_ _pi /\ 1 <_ 2 ) ) -> _pi <_ ( 2 x. _pi ) )
22 7 19 9 20 21 mp4an 
 |-  _pi <_ ( 2 x. _pi )
23 iooss2 
 |-  ( ( ( 2 x. _pi ) e. RR* /\ _pi <_ ( 2 x. _pi ) ) -> ( 0 (,) _pi ) C_ ( 0 (,) ( 2 x. _pi ) ) )
24 18 22 23 mp2an 
 |-  ( 0 (,) _pi ) C_ ( 0 (,) ( 2 x. _pi ) )
25 24 sseli 
 |-  ( A e. ( 0 (,) _pi ) -> A e. ( 0 (,) ( 2 x. _pi ) ) )
26 cos02pilt1 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( cos ` A ) < 1 )
27 25 26 syl 
 |-  ( A e. ( 0 (,) _pi ) -> ( cos ` A ) < 1 )
28 neg1rr 
 |-  -u 1 e. RR
29 28 rexri 
 |-  -u 1 e. RR*
30 1xr 
 |-  1 e. RR*
31 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 ) ) )
32 29 30 31 mp2an 
 |-  ( ( cos ` A ) e. ( -u 1 (,) 1 ) <-> ( ( cos ` A ) e. RR /\ -u 1 < ( cos ` A ) /\ ( cos ` A ) < 1 ) )
33 2 16 27 32 syl3anbrc 
 |-  ( A e. ( 0 (,) _pi ) -> ( cos ` A ) e. ( -u 1 (,) 1 ) )