This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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