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 ) ) ) |