Metamath Proof Explorer

Theorem cosq34lt1

Description: Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024)

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

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 2re 
 |-  2 e. RR
3 2 1 remulcli 
 |-  ( 2 x. _pi ) e. RR
4 3 rexri 
 |-  ( 2 x. _pi ) e. RR*
5 elico2 
 |-  ( ( _pi e. RR /\ ( 2 x. _pi ) e. RR* ) -> ( A e. ( _pi [,) ( 2 x. _pi ) ) <-> ( A e. RR /\ _pi <_ A /\ A < ( 2 x. _pi ) ) ) )
6 1 4 5 mp2an 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) <-> ( A e. RR /\ _pi <_ A /\ A < ( 2 x. _pi ) ) )
7 6 simp1bi 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> A e. RR )
8 0red 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> 0 e. RR )
9 1 a1i 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> _pi e. RR )
10 pipos 
 |-  0 < _pi
11 10 a1i 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> 0 < _pi )
12 6 simp2bi 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> _pi <_ A )
13 8 9 7 11 12 ltletrd 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> 0 < A )
14 6 simp3bi 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> A < ( 2 x. _pi ) )
15 0xr 
 |-  0 e. RR*
16 elioo2 
 |-  ( ( 0 e. RR* /\ ( 2 x. _pi ) e. RR* ) -> ( A e. ( 0 (,) ( 2 x. _pi ) ) <-> ( A e. RR /\ 0 < A /\ A < ( 2 x. _pi ) ) ) )
17 15 4 16 mp2an 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) <-> ( A e. RR /\ 0 < A /\ A < ( 2 x. _pi ) ) )
18 7 13 14 17 syl3anbrc 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> A e. ( 0 (,) ( 2 x. _pi ) ) )
19 cos02pilt1 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( cos ` A ) < 1 )
20 18 19 syl 
 |-  ( A e. ( _pi [,) ( 2 x. _pi ) ) -> ( cos ` A ) < 1 )