Proof of Theorem cosordlem
Step | Hyp | Ref
| Expression |
1 | | cosord.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (0[,]π)) |
2 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
3 | | pire 24014 |
. . . . . . . 8
⊢ π
∈ ℝ |
4 | 2, 3 | elicc2i 12110 |
. . . . . . 7
⊢ (𝐵 ∈ (0[,]π) ↔ (𝐵 ∈ ℝ ∧ 0 ≤
𝐵 ∧ 𝐵 ≤ π)) |
5 | 1, 4 | sylib 207 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ π)) |
6 | 5 | simp1d 1066 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | 6 | recnd 9947 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℂ) |
8 | | cosord.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (0[,]π)) |
9 | 2, 3 | elicc2i 12110 |
. . . . . . 7
⊢ (𝐴 ∈ (0[,]π) ↔ (𝐴 ∈ ℝ ∧ 0 ≤
𝐴 ∧ 𝐴 ≤ π)) |
10 | 8, 9 | sylib 207 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ π)) |
11 | 10 | simp1d 1066 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
12 | 11 | recnd 9947 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
13 | | subcos 14744 |
. . . 4
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) →
((cos‘𝐴) −
(cos‘𝐵)) = (2
· ((sin‘((𝐵 +
𝐴) / 2)) ·
(sin‘((𝐵 −
𝐴) /
2))))) |
14 | 7, 12, 13 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((cos‘𝐴) − (cos‘𝐵)) = (2 ·
((sin‘((𝐵 + 𝐴) / 2)) ·
(sin‘((𝐵 −
𝐴) /
2))))) |
15 | | 2re 10967 |
. . . . 5
⊢ 2 ∈
ℝ |
16 | | 2pos 10989 |
. . . . 5
⊢ 0 <
2 |
17 | 15, 16 | elrpii 11711 |
. . . 4
⊢ 2 ∈
ℝ+ |
18 | 6, 11 | readdcld 9948 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℝ) |
19 | 18 | rehalfcld 11156 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 + 𝐴) / 2) ∈ ℝ) |
20 | 19 | resincld 14712 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝐵 + 𝐴) / 2)) ∈ ℝ) |
21 | 2 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) |
22 | 10 | simp2d 1067 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝐴) |
23 | | cosord.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) |
24 | 21, 11, 6, 22, 23 | lelttrd 10074 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝐵) |
25 | | addgtge0 10395 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ (0 <
𝐵 ∧ 0 ≤ 𝐴)) → 0 < (𝐵 + 𝐴)) |
26 | 6, 11, 24, 22, 25 | syl22anc 1319 |
. . . . . . . . 9
⊢ (𝜑 → 0 < (𝐵 + 𝐴)) |
27 | | divgt0 10770 |
. . . . . . . . . 10
⊢ ((((𝐵 + 𝐴) ∈ ℝ ∧ 0 < (𝐵 + 𝐴)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 < ((𝐵 + 𝐴) / 2)) |
28 | 15, 16, 27 | mpanr12 717 |
. . . . . . . . 9
⊢ (((𝐵 + 𝐴) ∈ ℝ ∧ 0 < (𝐵 + 𝐴)) → 0 < ((𝐵 + 𝐴) / 2)) |
29 | 18, 26, 28 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 0 < ((𝐵 + 𝐴) / 2)) |
30 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → π ∈
ℝ) |
31 | 11, 6, 6, 23 | ltadd2dd 10075 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 + 𝐴) < (𝐵 + 𝐵)) |
32 | 7 | 2timesd 11152 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝐵) = (𝐵 + 𝐵)) |
33 | 31, 32 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 + 𝐴) < (2 · 𝐵)) |
34 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
35 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 2) |
36 | | ltdivmul 10777 |
. . . . . . . . . . 11
⊢ (((𝐵 + 𝐴) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((𝐵 + 𝐴) / 2) < 𝐵 ↔ (𝐵 + 𝐴) < (2 · 𝐵))) |
37 | 18, 6, 34, 35, 36 | syl112anc 1322 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐵 + 𝐴) / 2) < 𝐵 ↔ (𝐵 + 𝐴) < (2 · 𝐵))) |
38 | 33, 37 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 + 𝐴) / 2) < 𝐵) |
39 | 5 | simp3d 1068 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ≤ π) |
40 | 19, 6, 30, 38, 39 | ltletrd 10076 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 + 𝐴) / 2) < π) |
41 | | 0xr 9965 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
42 | 3 | rexri 9976 |
. . . . . . . . 9
⊢ π
∈ ℝ* |
43 | | elioo2 12087 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ*) →
(((𝐵 + 𝐴) / 2) ∈ (0(,)π) ↔ (((𝐵 + 𝐴) / 2) ∈ ℝ ∧ 0 < ((𝐵 + 𝐴) / 2) ∧ ((𝐵 + 𝐴) / 2) < π))) |
44 | 41, 42, 43 | mp2an 704 |
. . . . . . . 8
⊢ (((𝐵 + 𝐴) / 2) ∈ (0(,)π) ↔ (((𝐵 + 𝐴) / 2) ∈ ℝ ∧ 0 < ((𝐵 + 𝐴) / 2) ∧ ((𝐵 + 𝐴) / 2) < π)) |
45 | 19, 29, 40, 44 | syl3anbrc 1239 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 + 𝐴) / 2) ∈ (0(,)π)) |
46 | | sinq12gt0 24063 |
. . . . . . 7
⊢ (((𝐵 + 𝐴) / 2) ∈ (0(,)π) → 0 <
(sin‘((𝐵 + 𝐴) / 2))) |
47 | 45, 46 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 < (sin‘((𝐵 + 𝐴) / 2))) |
48 | 20, 47 | elrpd 11745 |
. . . . 5
⊢ (𝜑 → (sin‘((𝐵 + 𝐴) / 2)) ∈
ℝ+) |
49 | 6, 11 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
50 | 49 | rehalfcld 11156 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 − 𝐴) / 2) ∈ ℝ) |
51 | 50 | resincld 14712 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝐵 − 𝐴) / 2)) ∈ ℝ) |
52 | 11, 6 | posdifd 10493 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
53 | 23, 52 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
54 | | divgt0 10770 |
. . . . . . . . . 10
⊢ ((((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 < ((𝐵 −
𝐴) / 2)) |
55 | 15, 16, 54 | mpanr12 717 |
. . . . . . . . 9
⊢ (((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴)) → 0 < ((𝐵 − 𝐴) / 2)) |
56 | 49, 53, 55 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 0 < ((𝐵 − 𝐴) / 2)) |
57 | | rehalfcl 11135 |
. . . . . . . . . 10
⊢ (π
∈ ℝ → (π / 2) ∈ ℝ) |
58 | 3, 57 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (π / 2) ∈
ℝ) |
59 | 6, 11 | subge02d 10498 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ 𝐴 ↔ (𝐵 − 𝐴) ≤ 𝐵)) |
60 | 22, 59 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 − 𝐴) ≤ 𝐵) |
61 | 49, 6, 30, 60, 39 | letrd 10073 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ≤ π) |
62 | | lediv1 10767 |
. . . . . . . . . . 11
⊢ (((𝐵 − 𝐴) ∈ ℝ ∧ π ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝐵 − 𝐴) ≤ π ↔ ((𝐵 − 𝐴) / 2) ≤ (π / 2))) |
63 | 49, 30, 34, 35, 62 | syl112anc 1322 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 − 𝐴) ≤ π ↔ ((𝐵 − 𝐴) / 2) ≤ (π / 2))) |
64 | 61, 63 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 − 𝐴) / 2) ≤ (π / 2)) |
65 | | pirp 24017 |
. . . . . . . . . 10
⊢ π
∈ ℝ+ |
66 | | rphalflt 11736 |
. . . . . . . . . 10
⊢ (π
∈ ℝ+ → (π / 2) < π) |
67 | 65, 66 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (π / 2) <
π) |
68 | 50, 58, 30, 64, 67 | lelttrd 10074 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − 𝐴) / 2) < π) |
69 | | elioo2 12087 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ*) →
(((𝐵 − 𝐴) / 2) ∈ (0(,)π) ↔
(((𝐵 − 𝐴) / 2) ∈ ℝ ∧ 0
< ((𝐵 − 𝐴) / 2) ∧ ((𝐵 − 𝐴) / 2) < π))) |
70 | 41, 42, 69 | mp2an 704 |
. . . . . . . 8
⊢ (((𝐵 − 𝐴) / 2) ∈ (0(,)π) ↔ (((𝐵 − 𝐴) / 2) ∈ ℝ ∧ 0 < ((𝐵 − 𝐴) / 2) ∧ ((𝐵 − 𝐴) / 2) < π)) |
71 | 50, 56, 68, 70 | syl3anbrc 1239 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 − 𝐴) / 2) ∈ (0(,)π)) |
72 | | sinq12gt0 24063 |
. . . . . . 7
⊢ (((𝐵 − 𝐴) / 2) ∈ (0(,)π) → 0 <
(sin‘((𝐵 −
𝐴) / 2))) |
73 | 71, 72 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 < (sin‘((𝐵 − 𝐴) / 2))) |
74 | 51, 73 | elrpd 11745 |
. . . . 5
⊢ (𝜑 → (sin‘((𝐵 − 𝐴) / 2)) ∈
ℝ+) |
75 | 48, 74 | rpmulcld 11764 |
. . . 4
⊢ (𝜑 → ((sin‘((𝐵 + 𝐴) / 2)) · (sin‘((𝐵 − 𝐴) / 2))) ∈
ℝ+) |
76 | | rpmulcl 11731 |
. . . 4
⊢ ((2
∈ ℝ+ ∧ ((sin‘((𝐵 + 𝐴) / 2)) · (sin‘((𝐵 − 𝐴) / 2))) ∈ ℝ+) →
(2 · ((sin‘((𝐵
+ 𝐴) / 2)) ·
(sin‘((𝐵 −
𝐴) / 2)))) ∈
ℝ+) |
77 | 17, 75, 76 | sylancr 694 |
. . 3
⊢ (𝜑 → (2 ·
((sin‘((𝐵 + 𝐴) / 2)) ·
(sin‘((𝐵 −
𝐴) / 2)))) ∈
ℝ+) |
78 | 14, 77 | eqeltrd 2688 |
. 2
⊢ (𝜑 → ((cos‘𝐴) − (cos‘𝐵)) ∈
ℝ+) |
79 | 6 | recoscld 14713 |
. . 3
⊢ (𝜑 → (cos‘𝐵) ∈
ℝ) |
80 | 11 | recoscld 14713 |
. . 3
⊢ (𝜑 → (cos‘𝐴) ∈
ℝ) |
81 | | difrp 11744 |
. . 3
⊢
(((cos‘𝐵)
∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → ((cos‘𝐵) < (cos‘𝐴) ↔ ((cos‘𝐴) − (cos‘𝐵)) ∈
ℝ+)) |
82 | 79, 80, 81 | syl2anc 691 |
. 2
⊢ (𝜑 → ((cos‘𝐵) < (cos‘𝐴) ↔ ((cos‘𝐴) − (cos‘𝐵)) ∈
ℝ+)) |
83 | 78, 82 | mpbird 246 |
1
⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴)) |