Proof of Theorem ruclem3
| Step | Hyp | Ref
| Expression |
| 1 | | ruclem1.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 2 | | ruclem1.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 3 | | ruclem1.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 4 | 2, 3 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) |
| 5 | 4 | rehalfcld 12513 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
| 6 | 1, 5 | lenltd 11407 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ≤ ((𝐴 + 𝐵) / 2) ↔ ¬ ((𝐴 + 𝐵) / 2) < 𝑀)) |
| 7 | | ruclem2.8 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) |
| 8 | | avglt2 12505 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) |
| 9 | 2, 3, 8 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) |
| 10 | 7, 9 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) < 𝐵) |
| 11 | | avglt1 12504 |
. . . . . . . . . . 11
⊢ ((((𝐴 + 𝐵) / 2) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + 𝐵) / 2) < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
| 12 | 5, 3, 11 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴 + 𝐵) / 2) < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
| 13 | 10, 12 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) |
| 14 | 5, 3 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴 + 𝐵) / 2) + 𝐵) ∈ ℝ) |
| 15 | 14 | rehalfcld 12513 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴 + 𝐵) / 2) + 𝐵) / 2) ∈ ℝ) |
| 16 | | lelttr 11351 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ ((𝐴 + 𝐵) / 2) ∈ ℝ ∧ ((((𝐴 + 𝐵) / 2) + 𝐵) / 2) ∈ ℝ) → ((𝑀 ≤ ((𝐴 + 𝐵) / 2) ∧ ((𝐴 + 𝐵) / 2) < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) → 𝑀 < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
| 17 | 1, 5, 15, 16 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 ≤ ((𝐴 + 𝐵) / 2) ∧ ((𝐴 + 𝐵) / 2) < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) → 𝑀 < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
| 18 | 13, 17 | mpan2d 694 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ≤ ((𝐴 + 𝐵) / 2) → 𝑀 < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
| 19 | 6, 18 | sylbird 260 |
. . . . . . 7
⊢ (𝜑 → (¬ ((𝐴 + 𝐵) / 2) < 𝑀 → 𝑀 < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
| 20 | 19 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑀) → 𝑀 < ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) |
| 21 | | ruc.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
| 22 | | ruc.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
| 23 | | ruclem1.6 |
. . . . . . . . 9
⊢ 𝑋 = (1st
‘(〈𝐴, 𝐵〉𝐷𝑀)) |
| 24 | | ruclem1.7 |
. . . . . . . . 9
⊢ 𝑌 = (2nd
‘(〈𝐴, 𝐵〉𝐷𝑀)) |
| 25 | 21, 22, 2, 3, 1, 23,
24 | ruclem1 16267 |
. . . . . . . 8
⊢ (𝜑 → ((〈𝐴, 𝐵〉𝐷𝑀) ∈ (ℝ × ℝ) ∧
𝑋 = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) ∧ 𝑌 = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵))) |
| 26 | 25 | simp2d 1144 |
. . . . . . 7
⊢ (𝜑 → 𝑋 = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2))) |
| 27 | | iffalse 4534 |
. . . . . . 7
⊢ (¬
((𝐴 + 𝐵) / 2) < 𝑀 → if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) = ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) |
| 28 | 26, 27 | sylan9eq 2797 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑀) → 𝑋 = ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) |
| 29 | 20, 28 | breqtrrd 5171 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑀) → 𝑀 < 𝑋) |
| 30 | 29 | ex 412 |
. . . 4
⊢ (𝜑 → (¬ ((𝐴 + 𝐵) / 2) < 𝑀 → 𝑀 < 𝑋)) |
| 31 | 30 | con1d 145 |
. . 3
⊢ (𝜑 → (¬ 𝑀 < 𝑋 → ((𝐴 + 𝐵) / 2) < 𝑀)) |
| 32 | 25 | simp3d 1145 |
. . . . . 6
⊢ (𝜑 → 𝑌 = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵)) |
| 33 | | iftrue 4531 |
. . . . . 6
⊢ (((𝐴 + 𝐵) / 2) < 𝑀 → if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵) = ((𝐴 + 𝐵) / 2)) |
| 34 | 32, 33 | sylan9eq 2797 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) < 𝑀) → 𝑌 = ((𝐴 + 𝐵) / 2)) |
| 35 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) < 𝑀) → ((𝐴 + 𝐵) / 2) < 𝑀) |
| 36 | 34, 35 | eqbrtrd 5165 |
. . . 4
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) < 𝑀) → 𝑌 < 𝑀) |
| 37 | 36 | ex 412 |
. . 3
⊢ (𝜑 → (((𝐴 + 𝐵) / 2) < 𝑀 → 𝑌 < 𝑀)) |
| 38 | 31, 37 | syld 47 |
. 2
⊢ (𝜑 → (¬ 𝑀 < 𝑋 → 𝑌 < 𝑀)) |
| 39 | 38 | orrd 864 |
1
⊢ (𝜑 → (𝑀 < 𝑋 ∨ 𝑌 < 𝑀)) |