Step |
Hyp |
Ref |
Expression |
1 |
|
neghalfpire |
|- -u ( _pi / 2 ) e. RR |
2 |
|
halfpire |
|- ( _pi / 2 ) e. RR |
3 |
|
iccssre |
|- ( ( -u ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR ) -> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ RR ) |
4 |
1 2 3
|
mp2an |
|- ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ RR |
5 |
4
|
sseli |
|- ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> A e. RR ) |
6 |
4
|
sseli |
|- ( B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> B e. RR ) |
7 |
|
ltsub2 |
|- ( ( A e. RR /\ B e. RR /\ ( _pi / 2 ) e. RR ) -> ( A < B <-> ( ( _pi / 2 ) - B ) < ( ( _pi / 2 ) - A ) ) ) |
8 |
2 7
|
mp3an3 |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( ( _pi / 2 ) - B ) < ( ( _pi / 2 ) - A ) ) ) |
9 |
5 6 8
|
syl2an |
|- ( ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( A < B <-> ( ( _pi / 2 ) - B ) < ( ( _pi / 2 ) - A ) ) ) |
10 |
|
oveq2 |
|- ( x = B -> ( ( _pi / 2 ) - x ) = ( ( _pi / 2 ) - B ) ) |
11 |
10
|
eleq1d |
|- ( x = B -> ( ( ( _pi / 2 ) - x ) e. ( 0 [,] _pi ) <-> ( ( _pi / 2 ) - B ) e. ( 0 [,] _pi ) ) ) |
12 |
4
|
sseli |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> x e. RR ) |
13 |
|
resubcl |
|- ( ( ( _pi / 2 ) e. RR /\ x e. RR ) -> ( ( _pi / 2 ) - x ) e. RR ) |
14 |
2 12 13
|
sylancr |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - x ) e. RR ) |
15 |
1 2
|
elicc2i |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( x e. RR /\ -u ( _pi / 2 ) <_ x /\ x <_ ( _pi / 2 ) ) ) |
16 |
15
|
simp3bi |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> x <_ ( _pi / 2 ) ) |
17 |
|
subge0 |
|- ( ( ( _pi / 2 ) e. RR /\ x e. RR ) -> ( 0 <_ ( ( _pi / 2 ) - x ) <-> x <_ ( _pi / 2 ) ) ) |
18 |
2 12 17
|
sylancr |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( 0 <_ ( ( _pi / 2 ) - x ) <-> x <_ ( _pi / 2 ) ) ) |
19 |
16 18
|
mpbird |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> 0 <_ ( ( _pi / 2 ) - x ) ) |
20 |
15
|
simp2bi |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> -u ( _pi / 2 ) <_ x ) |
21 |
|
lesub2 |
|- ( ( -u ( _pi / 2 ) e. RR /\ x e. RR /\ ( _pi / 2 ) e. RR ) -> ( -u ( _pi / 2 ) <_ x <-> ( ( _pi / 2 ) - x ) <_ ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) ) |
22 |
1 2 21
|
mp3an13 |
|- ( x e. RR -> ( -u ( _pi / 2 ) <_ x <-> ( ( _pi / 2 ) - x ) <_ ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) ) |
23 |
12 22
|
syl |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( -u ( _pi / 2 ) <_ x <-> ( ( _pi / 2 ) - x ) <_ ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) ) |
24 |
20 23
|
mpbid |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - x ) <_ ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) |
25 |
2
|
recni |
|- ( _pi / 2 ) e. CC |
26 |
25 25
|
subnegi |
|- ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = ( ( _pi / 2 ) + ( _pi / 2 ) ) |
27 |
|
pidiv2halves |
|- ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi |
28 |
26 27
|
eqtri |
|- ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = _pi |
29 |
24 28
|
breqtrdi |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - x ) <_ _pi ) |
30 |
|
0re |
|- 0 e. RR |
31 |
|
pire |
|- _pi e. RR |
32 |
30 31
|
elicc2i |
|- ( ( ( _pi / 2 ) - x ) e. ( 0 [,] _pi ) <-> ( ( ( _pi / 2 ) - x ) e. RR /\ 0 <_ ( ( _pi / 2 ) - x ) /\ ( ( _pi / 2 ) - x ) <_ _pi ) ) |
33 |
14 19 29 32
|
syl3anbrc |
|- ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - x ) e. ( 0 [,] _pi ) ) |
34 |
11 33
|
vtoclga |
|- ( B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - B ) e. ( 0 [,] _pi ) ) |
35 |
|
oveq2 |
|- ( x = A -> ( ( _pi / 2 ) - x ) = ( ( _pi / 2 ) - A ) ) |
36 |
35
|
eleq1d |
|- ( x = A -> ( ( ( _pi / 2 ) - x ) e. ( 0 [,] _pi ) <-> ( ( _pi / 2 ) - A ) e. ( 0 [,] _pi ) ) ) |
37 |
36 33
|
vtoclga |
|- ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - A ) e. ( 0 [,] _pi ) ) |
38 |
|
cosord |
|- ( ( ( ( _pi / 2 ) - B ) e. ( 0 [,] _pi ) /\ ( ( _pi / 2 ) - A ) e. ( 0 [,] _pi ) ) -> ( ( ( _pi / 2 ) - B ) < ( ( _pi / 2 ) - A ) <-> ( cos ` ( ( _pi / 2 ) - A ) ) < ( cos ` ( ( _pi / 2 ) - B ) ) ) ) |
39 |
34 37 38
|
syl2anr |
|- ( ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( ( ( _pi / 2 ) - B ) < ( ( _pi / 2 ) - A ) <-> ( cos ` ( ( _pi / 2 ) - A ) ) < ( cos ` ( ( _pi / 2 ) - B ) ) ) ) |
40 |
5
|
recnd |
|- ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> A e. CC ) |
41 |
|
coshalfpim |
|- ( A e. CC -> ( cos ` ( ( _pi / 2 ) - A ) ) = ( sin ` A ) ) |
42 |
40 41
|
syl |
|- ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( cos ` ( ( _pi / 2 ) - A ) ) = ( sin ` A ) ) |
43 |
6
|
recnd |
|- ( B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> B e. CC ) |
44 |
|
coshalfpim |
|- ( B e. CC -> ( cos ` ( ( _pi / 2 ) - B ) ) = ( sin ` B ) ) |
45 |
43 44
|
syl |
|- ( B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( cos ` ( ( _pi / 2 ) - B ) ) = ( sin ` B ) ) |
46 |
42 45
|
breqan12d |
|- ( ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( ( cos ` ( ( _pi / 2 ) - A ) ) < ( cos ` ( ( _pi / 2 ) - B ) ) <-> ( sin ` A ) < ( sin ` B ) ) ) |
47 |
9 39 46
|
3bitrd |
|- ( ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( A < B <-> ( sin ` A ) < ( sin ` B ) ) ) |