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