Metamath Proof Explorer

Theorem cos02pilt1

Description: Cosine is less than one between zero and 2 x. _pi . (Contributed by Jim Kingdon, 23-Mar-2024)

Ref Expression
Assertion cos02pilt1 
|- ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( cos ` A ) < 1 )

Proof

Step Hyp Ref Expression
1 elioore 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> A e. RR )
2 1 recoscld 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( cos ` A ) e. RR )
3 1red 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 1 e. RR )
4 cosbnd 
 |-  ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )
5 4 simprd 
 |-  ( A e. RR -> ( cos ` A ) <_ 1 )
6 1 5 syl 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( cos ` A ) <_ 1 )
7 0zd 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 e. ZZ )
8 2re 
 |-  2 e. RR
9 pire 
 |-  _pi e. RR
10 8 9 remulcli 
 |-  ( 2 x. _pi ) e. RR
11 10 a1i 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( 2 x. _pi ) e. RR )
12 0xr 
 |-  0 e. RR*
13 10 rexri 
 |-  ( 2 x. _pi ) e. RR*
14 elioo2 
 |-  ( ( 0 e. RR* /\ ( 2 x. _pi ) e. RR* ) -> ( A e. ( 0 (,) ( 2 x. _pi ) ) <-> ( A e. RR /\ 0 < A /\ A < ( 2 x. _pi ) ) ) )
15 12 13 14 mp2an 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) <-> ( A e. RR /\ 0 < A /\ A < ( 2 x. _pi ) ) )
16 15 simp2bi 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 < A )
17 2rp 
 |-  2 e. RR+
18 pirp 
 |-  _pi e. RR+
19 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
20 17 18 19 mp2an 
 |-  ( 2 x. _pi ) e. RR+
21 rpgt0 
 |-  ( ( 2 x. _pi ) e. RR+ -> 0 < ( 2 x. _pi ) )
22 20 21 mp1i 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 < ( 2 x. _pi ) )
23 1 11 16 22 divgt0d 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 0 < ( A / ( 2 x. _pi ) ) )
24 20 a1i 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( 2 x. _pi ) e. RR+ )
25 15 simp3bi 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> A < ( 2 x. _pi ) )
26 1 11 24 25 ltdiv1dd 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( A / ( 2 x. _pi ) ) < ( ( 2 x. _pi ) / ( 2 x. _pi ) ) )
27 11 recnd 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( 2 x. _pi ) e. CC )
28 22 gt0ne0d 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( 2 x. _pi ) =/= 0 )
29 27 28 dividd 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( ( 2 x. _pi ) / ( 2 x. _pi ) ) = 1 )
30 26 29 breqtrd 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( A / ( 2 x. _pi ) ) < 1 )
31 0p1e1 
 |-  ( 0 + 1 ) = 1
32 30 31 breqtrrdi 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( A / ( 2 x. _pi ) ) < ( 0 + 1 ) )
33 btwnnz 
 |-  ( ( 0 e. ZZ /\ 0 < ( A / ( 2 x. _pi ) ) /\ ( A / ( 2 x. _pi ) ) < ( 0 + 1 ) ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
34 7 23 32 33 syl3anc 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
35 1 recnd 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> A e. CC )
36 coseq1 
 |-  ( A e. CC -> ( ( cos ` A ) = 1 <-> ( A / ( 2 x. _pi ) ) e. ZZ ) )
37 35 36 syl 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( ( cos ` A ) = 1 <-> ( A / ( 2 x. _pi ) ) e. ZZ ) )
38 34 37 mtbird 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> -. ( cos ` A ) = 1 )
39 38 neqned 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( cos ` A ) =/= 1 )
40 39 necomd 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> 1 =/= ( cos ` A ) )
41 2 3 6 40 leneltd 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( cos ` A ) < 1 )