Metamath Proof Explorer

Theorem ruclem2

Description: Lemma for ruc . Ordering property for the input to D . (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 ruclem2 ( 𝜑 → ( 𝐴 ≤ 𝑋 ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ 𝐵 ) )

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 leidd ⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
10 3 4 readdcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
11 10 rehalfcld ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ )
12 11 4 readdcld ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) ∈ ℝ )
13 12 rehalfcld ⊢ ( 𝜑 → ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ∈ ℝ )
14 avglt1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 < ( ( 𝐴 + 𝐵 ) / 2 ) ) )
15 3 4 14 syl2anc ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 𝐴 < ( ( 𝐴 + 𝐵 ) / 2 ) ) )
16 8 15 mpbid ⊢ ( 𝜑 → 𝐴 < ( ( 𝐴 + 𝐵 ) / 2 ) )
17 avglt2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ) )
18 3 4 17 syl2anc ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ) )
19 8 18 mpbid ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 )
20 avglt1 ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
21 11 4 20 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
22 19 21 mpbid ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
23 3 11 13 16 22 lttrd ⊢ ( 𝜑 → 𝐴 < ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
24 3 13 23 ltled ⊢ ( 𝜑 → 𝐴 ≤ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
25 breq2 ⊢ ( 𝐴 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) → ( 𝐴 ≤ 𝐴 ↔ 𝐴 ≤ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) ) )
26 breq2 ⊢ ( ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) → ( 𝐴 ≤ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ↔ 𝐴 ≤ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) ) )
27 25 26 ifboth ⊢ ( ( 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) → 𝐴 ≤ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
28 9 24 27 syl2anc ⊢ ( 𝜑 → 𝐴 ≤ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
29 1 2 3 4 5 6 7 ruclem1 ⊢ ( 𝜑 → ( ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ∈ ( ℝ × ℝ ) ∧ 𝑋 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) ∧ 𝑌 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ) )
30 29 simp2d ⊢ ( 𝜑 → 𝑋 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
31 28 30 breqtrrd ⊢ ( 𝜑 → 𝐴 ≤ 𝑋 )
32 iftrue ⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) = 𝐴 )
33 iftrue ⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) = ( ( 𝐴 + 𝐵 ) / 2 ) )
34 32 33 breq12d ⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → ( if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) < if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ↔ 𝐴 < ( ( 𝐴 + 𝐵 ) / 2 ) ) )
35 16 34 syl5ibrcom ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) < if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ) )
36 avglt2 ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ↔ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) < 𝐵 ) )
37 11 4 36 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ↔ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) < 𝐵 ) )
38 19 37 mpbid ⊢ ( 𝜑 → ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) < 𝐵 )
39 iffalse ⊢ ( ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) = ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
40 iffalse ⊢ ( ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) = 𝐵 )
41 39 40 breq12d ⊢ ( ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → ( if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) < if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ↔ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) < 𝐵 ) )
42 38 41 syl5ibrcom ⊢ ( 𝜑 → ( ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) < if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ) )
43 35 42 pm2.61d ⊢ ( 𝜑 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) < if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) )
44 29 simp3d ⊢ ( 𝜑 → 𝑌 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) )
45 43 30 44 3brtr4d ⊢ ( 𝜑 → 𝑋 < 𝑌 )
46 11 4 19 ltled ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ≤ 𝐵 )
47 4 leidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
48 breq1 ⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) ≤ 𝐵 ↔ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ≤ 𝐵 ) )
49 breq1 ⊢ ( 𝐵 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) → ( 𝐵 ≤ 𝐵 ↔ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ≤ 𝐵 ) )
50 48 49 ifboth ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ≤ 𝐵 )
51 46 47 50 syl2anc ⊢ ( 𝜑 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ≤ 𝐵 )
52 44 51 eqbrtrd ⊢ ( 𝜑 → 𝑌 ≤ 𝐵 )
53 31 45 52 3jca ⊢ ( 𝜑 → ( 𝐴 ≤ 𝑋 ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ 𝐵 ) )