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+A2⁢sin⁡B−A2
15 9 13 14 syl2anc ⊢φ→cos⁡A−cos⁡B=2⁢sin⁡B+A2⁢sin⁡B−A2
16 2rp ⊢2∈ℝ+
17 8 12 readdcld ⊢φ→B+A∈ℝ
18 17 rehalfcld ⊢φ→B+A2∈ℝ
19 18 resincld ⊢φ→sin⁡B+A2∈ℝ
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+A2
27 24 25 26 mpanr12 ⊢B+A∈ℝ∧0<B+A→0<B+A2
28 17 23 27 syl2anc ⊢φ→0<B+A2
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+A2<B↔B+A<2⁢B
36 17 8 33 34 35 syl112anc ⊢φ→B+A2<B↔B+A<2⁢B
37 32 36 mpbird ⊢φ→B+A2<B
38 7 simp3d ⊢φ→B≤π
39 18 8 29 37 38 ltletrd ⊢φ→B+A2<π
40 0xr ⊢0∈ℝ*
41 5 rexri ⊢π∈ℝ*
42 elioo2 ⊢0∈ℝ*∧π∈ℝ*→B+A2∈0π↔B+A2∈ℝ∧0<B+A2∧B+A2<π
43 40 41 42 mp2an ⊢B+A2∈0π↔B+A2∈ℝ∧0<B+A2∧B+A2<π
44 18 28 39 43 syl3anbrc ⊢φ→B+A2∈0π
45 sinq12gt0 ⊢B+A2∈0π→0<sin⁡B+A2
46 44 45 syl ⊢φ→0<sin⁡B+A2
47 19 46 elrpd ⊢φ→sin⁡B+A2∈ℝ+
48 8 12 resubcld ⊢φ→B−A∈ℝ
49 48 rehalfcld ⊢φ→B−A2∈ℝ
50 49 resincld ⊢φ→sin⁡B−A2∈ℝ
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−A2
54 24 25 53 mpanr12 ⊢B−A∈ℝ∧0<B−A→0<B−A2
55 48 52 54 syl2anc ⊢φ→0<B−A2
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−A2≤π2
62 48 29 33 34 61 syl112anc ⊢φ→B−A≤π↔B−A2≤π2
63 60 62 mpbid ⊢φ→B−A2≤π2
64 pirp ⊢π∈ℝ+
65 rphalflt ⊢π∈ℝ+→π2<π
66 64 65 mp1i ⊢φ→π2<π
67 49 57 29 63 66 lelttrd ⊢φ→B−A2<π
68 elioo2 ⊢0∈ℝ*∧π∈ℝ*→B−A2∈0π↔B−A2∈ℝ∧0<B−A2∧B−A2<π
69 40 41 68 mp2an ⊢B−A2∈0π↔B−A2∈ℝ∧0<B−A2∧B−A2<π
70 49 55 67 69 syl3anbrc ⊢φ→B−A2∈0π
71 sinq12gt0 ⊢B−A2∈0π→0<sin⁡B−A2
72 70 71 syl ⊢φ→0<sin⁡B−A2
73 50 72 elrpd ⊢φ→sin⁡B−A2∈ℝ+
74 47 73 rpmulcld ⊢φ→sin⁡B+A2⁢sin⁡B−A2∈ℝ+
75 rpmulcl ⊢2∈ℝ+∧sin⁡B+A2⁢sin⁡B−A2∈ℝ+→2⁢sin⁡B+A2⁢sin⁡B−A2∈ℝ+
76 16 74 75 sylancr ⊢φ→2⁢sin⁡B+A2⁢sin⁡B−A2∈ℝ+
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