Metamath Proof Explorer

Theorem cosordlem

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

Ref Expression
Hypotheses cosord.1 ⊢ φ → A ∈ 0 π
cosord.2 ⊢ φ → B ∈ 0 π
cosord.3 ⊢ φ → A < B
Assertion cosordlem ⊢ φ → cos ⁡ B < cos ⁡ A

Proof

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