Metamath Proof Explorer

Theorem ruclem3

Description: Lemma for ruc . The constructed interval [ X , Y ] always excludes M . (Contributed by Mario Carneiro, 28-May-2014)

Ref Expression
Hypotheses ruc.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
ruc.2 ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
ruclem1.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ruclem1.4 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ruclem1.5 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
ruclem1.6 ⊢ 𝑋 = ( 1st ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) )
ruclem1.7 ⊢ 𝑌 = ( 2nd ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) )
ruclem2.8 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion ruclem3 ( 𝜑 → ( 𝑀 < 𝑋 ∨ 𝑌 < 𝑀 ) )

Proof

Step Hyp Ref Expression
1 ruc.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
2 ruc.2 ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
3 ruclem1.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 ruclem1.4 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5 ruclem1.5 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
6 ruclem1.6 ⊢ 𝑋 = ( 1st ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) )
7 ruclem1.7 ⊢ 𝑌 = ( 2nd ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) )
8 ruclem2.8 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
9 3 4 readdcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
10 9 rehalfcld ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ )
11 5 10 lenltd ⊢ ( 𝜑 → ( 𝑀 ≤ ( ( 𝐴 + 𝐵 ) / 2 ) ↔ ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) )
12 avglt2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ) )
13 3 4 12 syl2anc ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ) )
14 8 13 mpbid ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 )
15 avglt1 ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
16 10 4 15 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
17 14 16 mpbid ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
18 10 4 readdcld ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) ∈ ℝ )
19 18 rehalfcld ⊢ ( 𝜑 → ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ∈ ℝ )
20 lelttr ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ ∧ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ∈ ℝ ) → ( ( 𝑀 ≤ ( ( 𝐴 + 𝐵 ) / 2 ) ∧ ( ( 𝐴 + 𝐵 ) / 2 ) < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) → 𝑀 < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
21 5 10 19 20 syl3anc ⊢ ( 𝜑 → ( ( 𝑀 ≤ ( ( 𝐴 + 𝐵 ) / 2 ) ∧ ( ( 𝐴 + 𝐵 ) / 2 ) < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) → 𝑀 < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
22 17 21 mpan2d ⊢ ( 𝜑 → ( 𝑀 ≤ ( ( 𝐴 + 𝐵 ) / 2 ) → 𝑀 < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
23 11 22 sylbird ⊢ ( 𝜑 → ( ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → 𝑀 < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
24 23 imp ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) → 𝑀 < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
25 1 2 3 4 5 6 7 ruclem1 ⊢ ( 𝜑 → ( ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ∈ ( ℝ × ℝ ) ∧ 𝑋 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) ∧ 𝑌 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ) )
26 25 simp2d ⊢ ( 𝜑 → 𝑋 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
27 iffalse ⊢ ( ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) = ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
28 26 27 sylan9eq ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) → 𝑋 = ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
29 24 28 breqtrrd ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) → 𝑀 < 𝑋 )
30 29 ex ⊢ ( 𝜑 → ( ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → 𝑀 < 𝑋 ) )
31 30 con1d ⊢ ( 𝜑 → ( ¬ 𝑀 < 𝑋 → ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) )
32 25 simp3d ⊢ ( 𝜑 → 𝑌 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) )
33 iftrue ⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) = ( ( 𝐴 + 𝐵 ) / 2 ) )
34 32 33 sylan9eq ⊢ ( ( 𝜑 ∧ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) → 𝑌 = ( ( 𝐴 + 𝐵 ) / 2 ) )
35 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) → ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 )
36 34 35 eqbrtrd ⊢ ( ( 𝜑 ∧ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) → 𝑌 < 𝑀 )
37 36 ex ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → 𝑌 < 𝑀 ) )
38 31 37 syld ⊢ ( 𝜑 → ( ¬ 𝑀 < 𝑋 → 𝑌 < 𝑀 ) )
39 38 orrd ⊢ ( 𝜑 → ( 𝑀 < 𝑋 ∨ 𝑌 < 𝑀 ) )