Metamath Proof Explorer

Theorem cosbnd

Description: The cosine of a real number lies between -1 and 1. Equation 18 of Gleason p. 311. (Contributed by NM, 16-Jan-2006)

Ref Expression
Assertion cosbnd 
|- ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )

Proof

Step Hyp Ref Expression
1 resincl 
 |-  ( A e. RR -> ( sin ` A ) e. RR )
2 1 sqge0d 
 |-  ( A e. RR -> 0 <_ ( ( sin ` A ) ^ 2 ) )
3 recoscl 
 |-  ( A e. RR -> ( cos ` A ) e. RR )
4 3 resqcld 
 |-  ( A e. RR -> ( ( cos ` A ) ^ 2 ) e. RR )
5 1 resqcld 
 |-  ( A e. RR -> ( ( sin ` A ) ^ 2 ) e. RR )
6 4 5 addge02d 
 |-  ( A e. RR -> ( 0 <_ ( ( sin ` A ) ^ 2 ) <-> ( ( cos ` A ) ^ 2 ) <_ ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) ) )
7 2 6 mpbid 
 |-  ( A e. RR -> ( ( cos ` A ) ^ 2 ) <_ ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) )
8 recn 
 |-  ( A e. RR -> A e. CC )
9 sincossq 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
10 8 9 syl 
 |-  ( A e. RR -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
11 sq1 
 |-  ( 1 ^ 2 ) = 1
12 10 11 eqtr4di 
 |-  ( A e. RR -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = ( 1 ^ 2 ) )
13 7 12 breqtrd 
 |-  ( A e. RR -> ( ( cos ` A ) ^ 2 ) <_ ( 1 ^ 2 ) )
14 1re 
 |-  1 e. RR
15 0le1 
 |-  0 <_ 1
16 lenegsq 
 |-  ( ( ( cos ` A ) e. RR /\ 1 e. RR /\ 0 <_ 1 ) -> ( ( ( cos ` A ) <_ 1 /\ -u ( cos ` A ) <_ 1 ) <-> ( ( cos ` A ) ^ 2 ) <_ ( 1 ^ 2 ) ) )
17 14 15 16 mp3an23 
 |-  ( ( cos ` A ) e. RR -> ( ( ( cos ` A ) <_ 1 /\ -u ( cos ` A ) <_ 1 ) <-> ( ( cos ` A ) ^ 2 ) <_ ( 1 ^ 2 ) ) )
18 lenegcon1 
 |-  ( ( ( cos ` A ) e. RR /\ 1 e. RR ) -> ( -u ( cos ` A ) <_ 1 <-> -u 1 <_ ( cos ` A ) ) )
19 14 18 mpan2 
 |-  ( ( cos ` A ) e. RR -> ( -u ( cos ` A ) <_ 1 <-> -u 1 <_ ( cos ` A ) ) )
20 19 anbi2d 
 |-  ( ( cos ` A ) e. RR -> ( ( ( cos ` A ) <_ 1 /\ -u ( cos ` A ) <_ 1 ) <-> ( ( cos ` A ) <_ 1 /\ -u 1 <_ ( cos ` A ) ) ) )
21 17 20 bitr3d 
 |-  ( ( cos ` A ) e. RR -> ( ( ( cos ` A ) ^ 2 ) <_ ( 1 ^ 2 ) <-> ( ( cos ` A ) <_ 1 /\ -u 1 <_ ( cos ` A ) ) ) )
22 3 21 syl 
 |-  ( A e. RR -> ( ( ( cos ` A ) ^ 2 ) <_ ( 1 ^ 2 ) <-> ( ( cos ` A ) <_ 1 /\ -u 1 <_ ( cos ` A ) ) ) )
23 13 22 mpbid 
 |-  ( A e. RR -> ( ( cos ` A ) <_ 1 /\ -u 1 <_ ( cos ` A ) ) )
24 23 ancomd 
 |-  ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )