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