Metamath Proof Explorer


Theorem cosordlem

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

Ref Expression
Hypotheses cosord.1 ( 𝜑𝐴 ∈ ( 0 [,] π ) )
cosord.2 ( 𝜑𝐵 ∈ ( 0 [,] π ) )
cosord.3 ( 𝜑𝐴 < 𝐵 )
Assertion cosordlem ( 𝜑 → ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) )

Proof

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