Metamath Proof Explorer

Theorem cosord

Description: Cosine is decreasing over the closed interval from 0 to _pi . (Contributed by Paul Chapman, 16-Mar-2008) (Proof shortened by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion cosord 
|- ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A < B <-> ( cos ` B ) < ( cos ` A ) ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) /\ A < B ) -> A e. ( 0 [,] _pi ) )
2 simplr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) /\ A < B ) -> B e. ( 0 [,] _pi ) )
3 simpr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) /\ A < B ) -> A < B )
4 1 2 3 cosordlem 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) /\ A < B ) -> ( cos ` B ) < ( cos ` A ) )
5 4 ex 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A < B -> ( cos ` B ) < ( cos ` A ) ) )
6 fveq2 
 |-  ( A = B -> ( cos ` A ) = ( cos ` B ) )
7 6 eqcomd 
 |-  ( A = B -> ( cos ` B ) = ( cos ` A ) )
8 7 a1i 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A = B -> ( cos ` B ) = ( cos ` A ) ) )
9 simplr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) /\ B < A ) -> B e. ( 0 [,] _pi ) )
10 simpll 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) /\ B < A ) -> A e. ( 0 [,] _pi ) )
11 simpr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) /\ B < A ) -> B < A )
12 9 10 11 cosordlem 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) /\ B < A ) -> ( cos ` A ) < ( cos ` B ) )
13 12 ex 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( B < A -> ( cos ` A ) < ( cos ` B ) ) )
14 8 13 orim12d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( ( A = B \/ B < A ) -> ( ( cos ` B ) = ( cos ` A ) \/ ( cos ` A ) < ( cos ` B ) ) ) )
15 14 con3d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( -. ( ( cos ` B ) = ( cos ` A ) \/ ( cos ` A ) < ( cos ` B ) ) -> -. ( A = B \/ B < A ) ) )
16 0re 
 |-  0 e. RR
17 pire 
 |-  _pi e. RR
18 16 17 elicc2i 
 |-  ( A e. ( 0 [,] _pi ) <-> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) )
19 18 simp1bi 
 |-  ( A e. ( 0 [,] _pi ) -> A e. RR )
20 16 17 elicc2i 
 |-  ( B e. ( 0 [,] _pi ) <-> ( B e. RR /\ 0 <_ B /\ B <_ _pi ) )
21 20 simp1bi 
 |-  ( B e. ( 0 [,] _pi ) -> B e. RR )
22 recoscl 
 |-  ( B e. RR -> ( cos ` B ) e. RR )
23 recoscl 
 |-  ( A e. RR -> ( cos ` A ) e. RR )
24 axlttri 
 |-  ( ( ( cos ` B ) e. RR /\ ( cos ` A ) e. RR ) -> ( ( cos ` B ) < ( cos ` A ) <-> -. ( ( cos ` B ) = ( cos ` A ) \/ ( cos ` A ) < ( cos ` B ) ) ) )
25 22 23 24 syl2anr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( cos ` B ) < ( cos ` A ) <-> -. ( ( cos ` B ) = ( cos ` A ) \/ ( cos ` A ) < ( cos ` B ) ) ) )
26 19 21 25 syl2an 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( ( cos ` B ) < ( cos ` A ) <-> -. ( ( cos ` B ) = ( cos ` A ) \/ ( cos ` A ) < ( cos ` B ) ) ) )
27 axlttri 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
28 19 21 27 syl2an 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
29 15 26 28 3imtr4d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( ( cos ` B ) < ( cos ` A ) -> A < B ) )
30 5 29 impbid 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A < B <-> ( cos ` B ) < ( cos ` A ) ) )