# 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 ( 𝜑 → ( 𝐴𝑋𝑋 < 𝑌𝑌𝐵 ) )