Metamath Proof Explorer

Theorem cos11

Description: Cosine is one-to-one 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 cos11 
|- ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A = B <-> ( cos ` A ) = ( cos ` B ) ) )

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( -. A < B /\ -. B < A ) <-> ( -. B < A /\ -. A < B ) )
2 cosord 
 |-  ( ( B e. ( 0 [,] _pi ) /\ A e. ( 0 [,] _pi ) ) -> ( B < A <-> ( cos ` A ) < ( cos ` B ) ) )
3 2 ancoms 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( B < A <-> ( cos ` A ) < ( cos ` B ) ) )
4 3 notbid 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( -. B < A <-> -. ( cos ` A ) < ( cos ` B ) ) )
5 cosord 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A < B <-> ( cos ` B ) < ( cos ` A ) ) )
6 5 notbid 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( -. A < B <-> -. ( cos ` B ) < ( cos ` A ) ) )
7 4 6 anbi12d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( ( -. B < A /\ -. A < B ) <-> ( -. ( cos ` A ) < ( cos ` B ) /\ -. ( cos ` B ) < ( cos ` A ) ) ) )
8 1 7 bitrid 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( ( -. A < B /\ -. B < A ) <-> ( -. ( cos ` A ) < ( cos ` B ) /\ -. ( cos ` B ) < ( cos ` A ) ) ) )
9 0re 
 |-  0 e. RR
10 pire 
 |-  _pi e. RR
11 9 10 elicc2i 
 |-  ( A e. ( 0 [,] _pi ) <-> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) )
12 11 simp1bi 
 |-  ( A e. ( 0 [,] _pi ) -> A e. RR )
13 9 10 elicc2i 
 |-  ( B e. ( 0 [,] _pi ) <-> ( B e. RR /\ 0 <_ B /\ B <_ _pi ) )
14 13 simp1bi 
 |-  ( B e. ( 0 [,] _pi ) -> B e. RR )
15 lttri3 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
16 12 14 15 syl2an 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
17 recoscl 
 |-  ( A e. RR -> ( cos ` A ) e. RR )
18 recoscl 
 |-  ( B e. RR -> ( cos ` B ) e. RR )
19 lttri3 
 |-  ( ( ( cos ` A ) e. RR /\ ( cos ` B ) e. RR ) -> ( ( cos ` A ) = ( cos ` B ) <-> ( -. ( cos ` A ) < ( cos ` B ) /\ -. ( cos ` B ) < ( cos ` A ) ) ) )
20 17 18 19 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( cos ` A ) = ( cos ` B ) <-> ( -. ( cos ` A ) < ( cos ` B ) /\ -. ( cos ` B ) < ( cos ` A ) ) ) )
21 12 14 20 syl2an 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( ( cos ` A ) = ( cos ` B ) <-> ( -. ( cos ` A ) < ( cos ` B ) /\ -. ( cos ` B ) < ( cos ` A ) ) ) )
22 8 16 21 3bitr4d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ B e. ( 0 [,] _pi ) ) -> ( A = B <-> ( cos ` A ) = ( cos ` B ) ) )