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 ⊢ φ → F : ℕ ⟶ ℝ
ruc.2 ⊢ φ → D = x ∈ ℝ 2 , y ∈ ℝ ⟼ ⦋ 1 st ⁡ x + 2 nd ⁡ x 2 / m⦌ if m < y 1 st ⁡ x m m + 2 nd ⁡ x 2 2 nd ⁡ x
ruclem1.3 ⊢ φ → A ∈ ℝ
ruclem1.4 ⊢ φ → B ∈ ℝ
ruclem1.5 ⊢ φ → M ∈ ℝ
ruclem1.6 ⊢ X = 1 st ⁡ A B D M
ruclem1.7 ⊢ Y = 2 nd ⁡ A B D M
ruclem2.8 ⊢ φ → A < B
Assertion ruclem2 ⊢ φ → A ≤ X ∧ X < Y ∧ Y ≤ B

Proof

Step Hyp Ref Expression
1 ruc.1 ⊢ φ → F : ℕ ⟶ ℝ
2 ruc.2 ⊢ φ → D = x ∈ ℝ 2 , y ∈ ℝ ⟼ ⦋ 1 st ⁡ x + 2 nd ⁡ x 2 / m⦌ if m < y 1 st ⁡ x m m + 2 nd ⁡ x 2 2 nd ⁡ x
3 ruclem1.3 ⊢ φ → A ∈ ℝ
4 ruclem1.4 ⊢ φ → B ∈ ℝ
5 ruclem1.5 ⊢ φ → M ∈ ℝ
6 ruclem1.6 ⊢ X = 1 st ⁡ A B D M
7 ruclem1.7 ⊢ Y = 2 nd ⁡ A B D M
8 ruclem2.8 ⊢ φ → A < B
9 3 leidd ⊢ φ → A ≤ A
10 3 4 readdcld ⊢ φ → A + B ∈ ℝ
11 10 rehalfcld ⊢ φ → A + B 2 ∈ ℝ
12 11 4 readdcld ⊢ φ → A + B 2 + B ∈ ℝ
13 12 rehalfcld ⊢ φ → A + B 2 + B 2 ∈ ℝ
14 avglt1 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A < A + B 2
15 3 4 14 syl2anc ⊢ φ → A < B ↔ A < A + B 2
16 8 15 mpbid ⊢ φ → A < A + B 2
17 avglt2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A + B 2 < B
18 3 4 17 syl2anc ⊢ φ → A < B ↔ A + B 2 < B
19 8 18 mpbid ⊢ φ → A + B 2 < B
20 avglt1 ⊢ A + B 2 ∈ ℝ ∧ B ∈ ℝ → A + B 2 < B ↔ A + B 2 < A + B 2 + B 2
21 11 4 20 syl2anc ⊢ φ → A + B 2 < B ↔ A + B 2 < A + B 2 + B 2
22 19 21 mpbid ⊢ φ → A + B 2 < A + B 2 + B 2
23 3 11 13 16 22 lttrd ⊢ φ → A < A + B 2 + B 2
24 3 13 23 ltled ⊢ φ → A ≤ A + B 2 + B 2
25 breq2 ⊢ A = if A + B 2 < M A A + B 2 + B 2 → A ≤ A ↔ A ≤ if A + B 2 < M A A + B 2 + B 2
26 breq2 ⊢ A + B 2 + B 2 = if A + B 2 < M A A + B 2 + B 2 → A ≤ A + B 2 + B 2 ↔ A ≤ if A + B 2 < M A A + B 2 + B 2
27 25 26 ifboth ⊢ A ≤ A ∧ A ≤ A + B 2 + B 2 → A ≤ if A + B 2 < M A A + B 2 + B 2
28 9 24 27 syl2anc ⊢ φ → A ≤ if A + B 2 < M A A + B 2 + B 2
29 1 2 3 4 5 6 7 ruclem1 ⊢ φ → A B D M ∈ ℝ 2 ∧ X = if A + B 2 < M A A + B 2 + B 2 ∧ Y = if A + B 2 < M A + B 2 B
30 29 simp2d ⊢ φ → X = if A + B 2 < M A A + B 2 + B 2
31 28 30 breqtrrd ⊢ φ → A ≤ X
32 iftrue ⊢ A + B 2 < M → if A + B 2 < M A A + B 2 + B 2 = A
33 iftrue ⊢ A + B 2 < M → if A + B 2 < M A + B 2 B = A + B 2
34 32 33 breq12d ⊢ A + B 2 < M → if A + B 2 < M A A + B 2 + B 2 < if A + B 2 < M A + B 2 B ↔ A < A + B 2
35 16 34 syl5ibrcom ⊢ φ → A + B 2 < M → if A + B 2 < M A A + B 2 + B 2 < if A + B 2 < M A + B 2 B
36 avglt2 ⊢ A + B 2 ∈ ℝ ∧ B ∈ ℝ → A + B 2 < B ↔ A + B 2 + B 2 < B
37 11 4 36 syl2anc ⊢ φ → A + B 2 < B ↔ A + B 2 + B 2 < B
38 19 37 mpbid ⊢ φ → A + B 2 + B 2 < B
39 iffalse ⊢ ¬ A + B 2 < M → if A + B 2 < M A A + B 2 + B 2 = A + B 2 + B 2
40 iffalse ⊢ ¬ A + B 2 < M → if A + B 2 < M A + B 2 B = B
41 39 40 breq12d ⊢ ¬ A + B 2 < M → if A + B 2 < M A A + B 2 + B 2 < if A + B 2 < M A + B 2 B ↔ A + B 2 + B 2 < B
42 38 41 syl5ibrcom ⊢ φ → ¬ A + B 2 < M → if A + B 2 < M A A + B 2 + B 2 < if A + B 2 < M A + B 2 B
43 35 42 pm2.61d ⊢ φ → if A + B 2 < M A A + B 2 + B 2 < if A + B 2 < M A + B 2 B
44 29 simp3d ⊢ φ → Y = if A + B 2 < M A + B 2 B
45 43 30 44 3brtr4d ⊢ φ → X < Y
46 11 4 19 ltled ⊢ φ → A + B 2 ≤ B
47 4 leidd ⊢ φ → B ≤ B
48 breq1 ⊢ A + B 2 = if A + B 2 < M A + B 2 B → A + B 2 ≤ B ↔ if A + B 2 < M A + B 2 B ≤ B
49 breq1 ⊢ B = if A + B 2 < M A + B 2 B → B ≤ B ↔ if A + B 2 < M A + B 2 B ≤ B
50 48 49 ifboth ⊢ A + B 2 ≤ B ∧ B ≤ B → if A + B 2 < M A + B 2 B ≤ B
51 46 47 50 syl2anc ⊢ φ → if A + B 2 < M A + B 2 B ≤ B
52 44 51 eqbrtrd ⊢ φ → Y ≤ B
53 31 45 52 3jca ⊢ φ → A ≤ X ∧ X < Y ∧ Y ≤ B