Proof of Theorem ruclem1
Step | Hyp | Ref
| Expression |
1 | | ruc.2 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
2 | 1 | oveqd 6667 |
. . . . 5
⊢ (𝜑 → (〈𝐴, 𝐵〉𝐷𝑀) = (〈𝐴, 𝐵〉(𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))𝑀)) |
3 | | ruclem1.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | | ruclem1.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
5 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
〈𝐴, 𝐵〉 ∈ (ℝ ×
ℝ)) |
6 | 3, 4, 5 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (ℝ ×
ℝ)) |
7 | | ruclem1.5 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
8 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → 𝑦 = 𝑀) |
9 | 8 | breq2d 4665 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → (𝑚 < 𝑦 ↔ 𝑚 < 𝑀)) |
10 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → 𝑥 = 〈𝐴, 𝐵〉) |
11 | 10 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → (1st ‘𝑥) = (1st
‘〈𝐴, 𝐵〉)) |
12 | 11 | opeq1d 4408 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → 〈(1st ‘𝑥), 𝑚〉 = 〈(1st
‘〈𝐴, 𝐵〉), 𝑚〉) |
13 | 10 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → (2nd ‘𝑥) = (2nd
‘〈𝐴, 𝐵〉)) |
14 | 13 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → (𝑚 + (2nd ‘𝑥)) = (𝑚 + (2nd ‘〈𝐴, 𝐵〉))) |
15 | 14 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → ((𝑚 + (2nd ‘𝑥)) / 2) = ((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2)) |
16 | 15, 13 | opeq12d 4410 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉 = 〈((𝑚 + (2nd
‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) |
17 | 9, 12, 16 | ifbieq12d 4113 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉) = if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
18 | 17 | csbeq2dv 3992 |
. . . . . . . 8
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → ⦋(((1st
‘𝑥) + (2nd
‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉) =
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
19 | 11, 13 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → ((1st ‘𝑥) + (2nd ‘𝑥)) = ((1st
‘〈𝐴, 𝐵〉) + (2nd
‘〈𝐴, 𝐵〉))) |
20 | 19 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → (((1st ‘𝑥) + (2nd ‘𝑥)) / 2) = (((1st
‘〈𝐴, 𝐵〉) + (2nd
‘〈𝐴, 𝐵〉)) / 2)) |
21 | 20 | csbeq1d 3540 |
. . . . . . . 8
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → ⦋(((1st
‘𝑥) + (2nd
‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) =
⦋(((1st ‘〈𝐴, 𝐵〉) + (2nd ‘〈𝐴, 𝐵〉)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
22 | 18, 21 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝑥 = 〈𝐴, 𝐵〉 ∧ 𝑦 = 𝑀) → ⦋(((1st
‘𝑥) + (2nd
‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉) =
⦋(((1st ‘〈𝐴, 𝐵〉) + (2nd ‘〈𝐴, 𝐵〉)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
23 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ (ℝ ×
ℝ), 𝑦 ∈ ℝ
↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉)) = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉)) |
24 | | opex 4932 |
. . . . . . . . 9
⊢
〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉 ∈ V |
25 | | opex 4932 |
. . . . . . . . 9
⊢
〈((𝑚 +
(2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉 ∈
V |
26 | 24, 25 | ifex 4156 |
. . . . . . . 8
⊢ if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) ∈
V |
27 | 26 | csbex 4793 |
. . . . . . 7
⊢
⦋(((1st ‘〈𝐴, 𝐵〉) + (2nd ‘〈𝐴, 𝐵〉)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) ∈
V |
28 | 22, 23, 27 | ovmpt2a 6791 |
. . . . . 6
⊢
((〈𝐴, 𝐵〉 ∈ (ℝ ×
ℝ) ∧ 𝑀 ∈
ℝ) → (〈𝐴,
𝐵〉(𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))𝑀) = ⦋(((1st
‘〈𝐴, 𝐵〉) + (2nd
‘〈𝐴, 𝐵〉)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
29 | 6, 7, 28 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (〈𝐴, 𝐵〉(𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))𝑀) = ⦋(((1st
‘〈𝐴, 𝐵〉) + (2nd
‘〈𝐴, 𝐵〉)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
30 | 2, 29 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → (〈𝐴, 𝐵〉𝐷𝑀) = ⦋(((1st
‘〈𝐴, 𝐵〉) + (2nd
‘〈𝐴, 𝐵〉)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
31 | | op1stg 7180 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(1st ‘〈𝐴, 𝐵〉) = 𝐴) |
32 | 3, 4, 31 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝐴, 𝐵〉) = 𝐴) |
33 | | op2ndg 7181 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
34 | 3, 4, 33 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘〈𝐴, 𝐵〉) = 𝐵) |
35 | 32, 34 | oveq12d 6668 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘〈𝐴, 𝐵〉) + (2nd
‘〈𝐴, 𝐵〉)) = (𝐴 + 𝐵)) |
36 | 35 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → (((1st
‘〈𝐴, 𝐵〉) + (2nd
‘〈𝐴, 𝐵〉)) / 2) = ((𝐴 + 𝐵) / 2)) |
37 | 36 | csbeq1d 3540 |
. . . . 5
⊢ (𝜑 →
⦋(((1st ‘〈𝐴, 𝐵〉) + (2nd ‘〈𝐴, 𝐵〉)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) =
⦋((𝐴 + 𝐵) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
38 | | ovex 6678 |
. . . . . . 7
⊢ ((𝐴 + 𝐵) / 2) ∈ V |
39 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑚 = ((𝐴 + 𝐵) / 2) → (𝑚 < 𝑀 ↔ ((𝐴 + 𝐵) / 2) < 𝑀)) |
40 | | opeq2 4403 |
. . . . . . . 8
⊢ (𝑚 = ((𝐴 + 𝐵) / 2) → 〈(1st
‘〈𝐴, 𝐵〉), 𝑚〉 = 〈(1st
‘〈𝐴, 𝐵〉), ((𝐴 + 𝐵) / 2)〉) |
41 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑚 = ((𝐴 + 𝐵) / 2) → (𝑚 + (2nd ‘〈𝐴, 𝐵〉)) = (((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉))) |
42 | 41 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = ((𝐴 + 𝐵) / 2) → ((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2) = ((((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉)) / 2)) |
43 | 42 | opeq1d 4408 |
. . . . . . . 8
⊢ (𝑚 = ((𝐴 + 𝐵) / 2) → 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉 = 〈((((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) |
44 | 39, 40, 43 | ifbieq12d 4113 |
. . . . . . 7
⊢ (𝑚 = ((𝐴 + 𝐵) / 2) → if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) = if(((𝐴 + 𝐵) / 2) < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉)) |
45 | 38, 44 | csbie 3559 |
. . . . . 6
⊢
⦋((𝐴 +
𝐵) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) = if(((𝐴 + 𝐵) / 2) < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) |
46 | 32 | opeq1d 4408 |
. . . . . . 7
⊢ (𝜑 → 〈(1st
‘〈𝐴, 𝐵〉), ((𝐴 + 𝐵) / 2)〉 = 〈𝐴, ((𝐴 + 𝐵) / 2)〉) |
47 | 34 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉)) = (((𝐴 + 𝐵) / 2) + 𝐵)) |
48 | 47 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉)) / 2) = ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) |
49 | 48, 34 | opeq12d 4410 |
. . . . . . 7
⊢ (𝜑 → 〈((((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉 = 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉) |
50 | 46, 49 | ifeq12d 4106 |
. . . . . 6
⊢ (𝜑 → if(((𝐴 + 𝐵) / 2) < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) = if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) |
51 | 45, 50 | syl5eq 2668 |
. . . . 5
⊢ (𝜑 → ⦋((𝐴 + 𝐵) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) = if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) |
52 | 37, 51 | eqtrd 2656 |
. . . 4
⊢ (𝜑 →
⦋(((1st ‘〈𝐴, 𝐵〉) + (2nd ‘〈𝐴, 𝐵〉)) / 2) / 𝑚⦌if(𝑚 < 𝑀, 〈(1st ‘〈𝐴, 𝐵〉), 𝑚〉, 〈((𝑚 + (2nd ‘〈𝐴, 𝐵〉)) / 2), (2nd
‘〈𝐴, 𝐵〉)〉) = if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) |
53 | 30, 52 | eqtrd 2656 |
. . 3
⊢ (𝜑 → (〈𝐴, 𝐵〉𝐷𝑀) = if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) |
54 | 3, 4 | readdcld 10069 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) |
55 | 54 | rehalfcld 11279 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
56 | | opelxpi 5148 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ ((𝐴 + 𝐵) / 2) ∈ ℝ) → 〈𝐴, ((𝐴 + 𝐵) / 2)〉 ∈ (ℝ ×
ℝ)) |
57 | 3, 55, 56 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 〈𝐴, ((𝐴 + 𝐵) / 2)〉 ∈ (ℝ ×
ℝ)) |
58 | 55, 4 | readdcld 10069 |
. . . . . 6
⊢ (𝜑 → (((𝐴 + 𝐵) / 2) + 𝐵) ∈ ℝ) |
59 | 58 | rehalfcld 11279 |
. . . . 5
⊢ (𝜑 → ((((𝐴 + 𝐵) / 2) + 𝐵) / 2) ∈ ℝ) |
60 | | opelxpi 5148 |
. . . . 5
⊢
((((((𝐴 + 𝐵) / 2) + 𝐵) / 2) ∈ ℝ ∧ 𝐵 ∈ ℝ) →
〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉 ∈ (ℝ ×
ℝ)) |
61 | 59, 4, 60 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉 ∈ (ℝ ×
ℝ)) |
62 | 57, 61 | ifcld 4131 |
. . 3
⊢ (𝜑 → if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉) ∈ (ℝ ×
ℝ)) |
63 | 53, 62 | eqeltrd 2701 |
. 2
⊢ (𝜑 → (〈𝐴, 𝐵〉𝐷𝑀) ∈ (ℝ ×
ℝ)) |
64 | | ruclem1.6 |
. . 3
⊢ 𝑋 = (1st
‘(〈𝐴, 𝐵〉𝐷𝑀)) |
65 | 53 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (1st
‘(〈𝐴, 𝐵〉𝐷𝑀)) = (1st ‘if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉))) |
66 | | fvif 6204 |
. . . . 5
⊢
(1st ‘if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) = if(((𝐴 + 𝐵) / 2) < 𝑀, (1st ‘〈𝐴, ((𝐴 + 𝐵) / 2)〉), (1st
‘〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) |
67 | | op1stg 7180 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ ((𝐴 + 𝐵) / 2) ∈ V) → (1st
‘〈𝐴, ((𝐴 + 𝐵) / 2)〉) = 𝐴) |
68 | 3, 38, 67 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝐴, ((𝐴 + 𝐵) / 2)〉) = 𝐴) |
69 | | ovex 6678 |
. . . . . . 7
⊢ ((((𝐴 + 𝐵) / 2) + 𝐵) / 2) ∈ V |
70 | | op1stg 7180 |
. . . . . . 7
⊢
((((((𝐴 + 𝐵) / 2) + 𝐵) / 2) ∈ V ∧ 𝐵 ∈ ℝ) → (1st
‘〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉) = ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) |
71 | 69, 4, 70 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉) = ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) |
72 | 68, 71 | ifeq12d 4106 |
. . . . 5
⊢ (𝜑 → if(((𝐴 + 𝐵) / 2) < 𝑀, (1st ‘〈𝐴, ((𝐴 + 𝐵) / 2)〉), (1st
‘〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
73 | 66, 72 | syl5eq 2668 |
. . . 4
⊢ (𝜑 → (1st
‘if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
74 | 65, 73 | eqtrd 2656 |
. . 3
⊢ (𝜑 → (1st
‘(〈𝐴, 𝐵〉𝐷𝑀)) = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
75 | 64, 74 | syl5eq 2668 |
. 2
⊢ (𝜑 → 𝑋 = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
76 | | ruclem1.7 |
. . 3
⊢ 𝑌 = (2nd
‘(〈𝐴, 𝐵〉𝐷𝑀)) |
77 | 53 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (2nd
‘(〈𝐴, 𝐵〉𝐷𝑀)) = (2nd ‘if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉))) |
78 | | fvif 6204 |
. . . . 5
⊢
(2nd ‘if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) = if(((𝐴 + 𝐵) / 2) < 𝑀, (2nd ‘〈𝐴, ((𝐴 + 𝐵) / 2)〉), (2nd
‘〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) |
79 | | op2ndg 7181 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ ((𝐴 + 𝐵) / 2) ∈ V) → (2nd
‘〈𝐴, ((𝐴 + 𝐵) / 2)〉) = ((𝐴 + 𝐵) / 2)) |
80 | 3, 38, 79 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈𝐴, ((𝐴 + 𝐵) / 2)〉) = ((𝐴 + 𝐵) / 2)) |
81 | | op2ndg 7181 |
. . . . . . 7
⊢
((((((𝐴 + 𝐵) / 2) + 𝐵) / 2) ∈ V ∧ 𝐵 ∈ ℝ) → (2nd
‘〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉) = 𝐵) |
82 | 69, 4, 81 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉) = 𝐵) |
83 | 80, 82 | ifeq12d 4106 |
. . . . 5
⊢ (𝜑 → if(((𝐴 + 𝐵) / 2) < 𝑀, (2nd ‘〈𝐴, ((𝐴 + 𝐵) / 2)〉), (2nd
‘〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵)) |
84 | 78, 83 | syl5eq 2668 |
. . . 4
⊢ (𝜑 → (2nd
‘if(((𝐴 + 𝐵) / 2) < 𝑀, 〈𝐴, ((𝐴 + 𝐵) / 2)〉, 〈((((𝐴 + 𝐵) / 2) + 𝐵) / 2), 𝐵〉)) = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵)) |
85 | 77, 84 | eqtrd 2656 |
. . 3
⊢ (𝜑 → (2nd
‘(〈𝐴, 𝐵〉𝐷𝑀)) = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵)) |
86 | 76, 85 | syl5eq 2668 |
. 2
⊢ (𝜑 → 𝑌 = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵)) |
87 | 63, 75, 86 | 3jca 1242 |
1
⊢ (𝜑 → ((〈𝐴, 𝐵〉𝐷𝑀) ∈ (ℝ × ℝ) ∧
𝑋 = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) ∧ 𝑌 = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵))) |