Metamath Proof Explorer

Theorem cosordlem

Description: Lemma for cosord . (Contributed by Mario Carneiro, 10-May-2014)

Ref Expression
Hypotheses cosord.1 
|- ( ph -> A e. ( 0 [,] _pi ) )
cosord.2 
|- ( ph -> B e. ( 0 [,] _pi ) )
cosord.3 
|- ( ph -> A < B )
Assertion cosordlem 
|- ( ph -> ( cos ` B ) < ( cos ` A ) )

Proof

Step Hyp Ref Expression
1 cosord.1 
 |-  ( ph -> A e. ( 0 [,] _pi ) )
2 cosord.2 
 |-  ( ph -> B e. ( 0 [,] _pi ) )
3 cosord.3 
 |-  ( ph -> A < B )
4 0re 
 |-  0 e. RR
5 pire 
 |-  _pi e. RR
6 4 5 elicc2i 
 |-  ( B e. ( 0 [,] _pi ) <-> ( B e. RR /\ 0 <_ B /\ B <_ _pi ) )
7 2 6 sylib 
 |-  ( ph -> ( B e. RR /\ 0 <_ B /\ B <_ _pi ) )
8 7 simp1d 
 |-  ( ph -> B e. RR )
9 8 recnd 
 |-  ( ph -> B e. CC )
10 4 5 elicc2i 
 |-  ( A e. ( 0 [,] _pi ) <-> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) )
11 1 10 sylib 
 |-  ( ph -> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) )
12 11 simp1d 
 |-  ( ph -> A e. RR )
13 12 recnd 
 |-  ( ph -> A e. CC )
14 subcos 
 |-  ( ( B e. CC /\ A e. CC ) -> ( ( cos ` A ) - ( cos ` B ) ) = ( 2 x. ( ( sin ` ( ( B + A ) / 2 ) ) x. ( sin ` ( ( B - A ) / 2 ) ) ) ) )
15 9 13 14 syl2anc 
 |-  ( ph -> ( ( cos ` A ) - ( cos ` B ) ) = ( 2 x. ( ( sin ` ( ( B + A ) / 2 ) ) x. ( sin ` ( ( B - A ) / 2 ) ) ) ) )
16 2rp 
 |-  2 e. RR+
17 8 12 readdcld 
 |-  ( ph -> ( B + A ) e. RR )
18 17 rehalfcld 
 |-  ( ph -> ( ( B + A ) / 2 ) e. RR )
19 18 resincld 
 |-  ( ph -> ( sin ` ( ( B + A ) / 2 ) ) e. RR )
20 4 a1i 
 |-  ( ph -> 0 e. RR )
21 11 simp2d 
 |-  ( ph -> 0 <_ A )
22 20 12 8 21 3 lelttrd 
 |-  ( ph -> 0 < B )
23 8 12 22 21 addgtge0d 
 |-  ( ph -> 0 < ( B + A ) )
24 2re 
 |-  2 e. RR
25 2pos 
 |-  0 < 2
26 divgt0 
 |-  ( ( ( ( B + A ) e. RR /\ 0 < ( B + A ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( ( B + A ) / 2 ) )
27 24 25 26 mpanr12 
 |-  ( ( ( B + A ) e. RR /\ 0 < ( B + A ) ) -> 0 < ( ( B + A ) / 2 ) )
28 17 23 27 syl2anc 
 |-  ( ph -> 0 < ( ( B + A ) / 2 ) )
29 5 a1i 
 |-  ( ph -> _pi e. RR )
30 12 8 8 3 ltadd2dd 
 |-  ( ph -> ( B + A ) < ( B + B ) )
31 9 2timesd 
 |-  ( ph -> ( 2 x. B ) = ( B + B ) )
32 30 31 breqtrrd 
 |-  ( ph -> ( B + A ) < ( 2 x. B ) )
33 24 a1i 
 |-  ( ph -> 2 e. RR )
34 25 a1i 
 |-  ( ph -> 0 < 2 )
35 ltdivmul 
 |-  ( ( ( B + A ) e. RR /\ B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( B + A ) / 2 ) < B <-> ( B + A ) < ( 2 x. B ) ) )
36 17 8 33 34 35 syl112anc 
 |-  ( ph -> ( ( ( B + A ) / 2 ) < B <-> ( B + A ) < ( 2 x. B ) ) )
37 32 36 mpbird 
 |-  ( ph -> ( ( B + A ) / 2 ) < B )
38 7 simp3d 
 |-  ( ph -> B <_ _pi )
39 18 8 29 37 38 ltletrd 
 |-  ( ph -> ( ( B + A ) / 2 ) < _pi )
40 0xr 
 |-  0 e. RR*
41 5 rexri 
 |-  _pi e. RR*
42 elioo2 
 |-  ( ( 0 e. RR* /\ _pi e. RR* ) -> ( ( ( B + A ) / 2 ) e. ( 0 (,) _pi ) <-> ( ( ( B + A ) / 2 ) e. RR /\ 0 < ( ( B + A ) / 2 ) /\ ( ( B + A ) / 2 ) < _pi ) ) )
43 40 41 42 mp2an 
 |-  ( ( ( B + A ) / 2 ) e. ( 0 (,) _pi ) <-> ( ( ( B + A ) / 2 ) e. RR /\ 0 < ( ( B + A ) / 2 ) /\ ( ( B + A ) / 2 ) < _pi ) )
44 18 28 39 43 syl3anbrc 
 |-  ( ph -> ( ( B + A ) / 2 ) e. ( 0 (,) _pi ) )
45 sinq12gt0 
 |-  ( ( ( B + A ) / 2 ) e. ( 0 (,) _pi ) -> 0 < ( sin ` ( ( B + A ) / 2 ) ) )
46 44 45 syl 
 |-  ( ph -> 0 < ( sin ` ( ( B + A ) / 2 ) ) )
47 19 46 elrpd 
 |-  ( ph -> ( sin ` ( ( B + A ) / 2 ) ) e. RR+ )
48 8 12 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
49 48 rehalfcld 
 |-  ( ph -> ( ( B - A ) / 2 ) e. RR )
50 49 resincld 
 |-  ( ph -> ( sin ` ( ( B - A ) / 2 ) ) e. RR )
51 12 8 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
52 3 51 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
53 divgt0 
 |-  ( ( ( ( B - A ) e. RR /\ 0 < ( B - A ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( ( B - A ) / 2 ) )
54 24 25 53 mpanr12 
 |-  ( ( ( B - A ) e. RR /\ 0 < ( B - A ) ) -> 0 < ( ( B - A ) / 2 ) )
55 48 52 54 syl2anc 
 |-  ( ph -> 0 < ( ( B - A ) / 2 ) )
56 rehalfcl 
 |-  ( _pi e. RR -> ( _pi / 2 ) e. RR )
57 5 56 mp1i 
 |-  ( ph -> ( _pi / 2 ) e. RR )
58 8 12 subge02d 
 |-  ( ph -> ( 0 <_ A <-> ( B - A ) <_ B ) )
59 21 58 mpbid 
 |-  ( ph -> ( B - A ) <_ B )
60 48 8 29 59 38 letrd 
 |-  ( ph -> ( B - A ) <_ _pi )
61 lediv1 
 |-  ( ( ( B - A ) e. RR /\ _pi e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( B - A ) <_ _pi <-> ( ( B - A ) / 2 ) <_ ( _pi / 2 ) ) )
62 48 29 33 34 61 syl112anc 
 |-  ( ph -> ( ( B - A ) <_ _pi <-> ( ( B - A ) / 2 ) <_ ( _pi / 2 ) ) )
63 60 62 mpbid 
 |-  ( ph -> ( ( B - A ) / 2 ) <_ ( _pi / 2 ) )
64 pirp 
 |-  _pi e. RR+
65 rphalflt 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) < _pi )
66 64 65 mp1i 
 |-  ( ph -> ( _pi / 2 ) < _pi )
67 49 57 29 63 66 lelttrd 
 |-  ( ph -> ( ( B - A ) / 2 ) < _pi )
68 elioo2 
 |-  ( ( 0 e. RR* /\ _pi e. RR* ) -> ( ( ( B - A ) / 2 ) e. ( 0 (,) _pi ) <-> ( ( ( B - A ) / 2 ) e. RR /\ 0 < ( ( B - A ) / 2 ) /\ ( ( B - A ) / 2 ) < _pi ) ) )
69 40 41 68 mp2an 
 |-  ( ( ( B - A ) / 2 ) e. ( 0 (,) _pi ) <-> ( ( ( B - A ) / 2 ) e. RR /\ 0 < ( ( B - A ) / 2 ) /\ ( ( B - A ) / 2 ) < _pi ) )
70 49 55 67 69 syl3anbrc 
 |-  ( ph -> ( ( B - A ) / 2 ) e. ( 0 (,) _pi ) )
71 sinq12gt0 
 |-  ( ( ( B - A ) / 2 ) e. ( 0 (,) _pi ) -> 0 < ( sin ` ( ( B - A ) / 2 ) ) )
72 70 71 syl 
 |-  ( ph -> 0 < ( sin ` ( ( B - A ) / 2 ) ) )
73 50 72 elrpd 
 |-  ( ph -> ( sin ` ( ( B - A ) / 2 ) ) e. RR+ )
74 47 73 rpmulcld 
 |-  ( ph -> ( ( sin ` ( ( B + A ) / 2 ) ) x. ( sin ` ( ( B - A ) / 2 ) ) ) e. RR+ )
75 rpmulcl 
 |-  ( ( 2 e. RR+ /\ ( ( sin ` ( ( B + A ) / 2 ) ) x. ( sin ` ( ( B - A ) / 2 ) ) ) e. RR+ ) -> ( 2 x. ( ( sin ` ( ( B + A ) / 2 ) ) x. ( sin ` ( ( B - A ) / 2 ) ) ) ) e. RR+ )
76 16 74 75 sylancr 
 |-  ( ph -> ( 2 x. ( ( sin ` ( ( B + A ) / 2 ) ) x. ( sin ` ( ( B - A ) / 2 ) ) ) ) e. RR+ )
77 15 76 eqeltrd 
 |-  ( ph -> ( ( cos ` A ) - ( cos ` B ) ) e. RR+ )
78 8 recoscld 
 |-  ( ph -> ( cos ` B ) e. RR )
79 12 recoscld 
 |-  ( ph -> ( cos ` A ) e. RR )
80 difrp 
 |-  ( ( ( cos ` B ) e. RR /\ ( cos ` A ) e. RR ) -> ( ( cos ` B ) < ( cos ` A ) <-> ( ( cos ` A ) - ( cos ` B ) ) e. RR+ ) )
81 78 79 80 syl2anc 
 |-  ( ph -> ( ( cos ` B ) < ( cos ` A ) <-> ( ( cos ` A ) - ( cos ` B ) ) e. RR+ ) )
82 77 81 mpbird 
 |-  ( ph -> ( cos ` B ) < ( cos ` A ) )