Metamath Proof Explorer


Theorem sinord

Description: Sine is increasing over the closed interval from -u (pi / 2 ) to ( pi / 2 ) . (Contributed by Mario Carneiro, 29-Jul-2014)

Ref Expression
Assertion sinord
|- ( ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ B e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( A < B <-> ( sin ` A ) < ( sin ` B ) ) )

Proof

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