ruclem2

Description: Lemma for ruc . Ordering property for the input to D . (Contributed by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypotheses	ruc.1	$⊢ φ \to F : ℕ ⟶ ℝ$
	ruc.2	$⊢ φ \to D = (x \in ℝ^{2}, y \in ℝ ⟼ ⦋ (\frac{1^{st} (x) + 2^{nd} (x)}{2}) / m ⦌ if (m < y, ⟨1^{st} (x), m⟩, ⟨\frac{m + 2^{nd} (x)}{2}, 2^{nd} (x)⟩))$
	ruclem1.3	$⊢ φ \to A \in ℝ$
	ruclem1.4	$⊢ φ \to B \in ℝ$
	ruclem1.5	$⊢ φ \to M \in ℝ$
	ruclem1.6	$⊢ X = 1^{st} (⟨A, B⟩ D M)$
	ruclem1.7	$⊢ Y = 2^{nd} (⟨A, B⟩ D M)$
	ruclem2.8	$⊢ φ \to A < B$
Assertion	ruclem2	$⊢ φ \to (A \leq X \land X < Y \land Y \leq B)$

Proof

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

Metamath Proof Explorer

Theorem ruclem2

Proof