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	$⊢ φ \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	ruclem3	$⊢ φ \to (M < X \lor Y < M)$

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 4	readdcld	$⊢ φ \to A + B \in ℝ$
10	9	rehalfcld	$⊢ φ \to \frac{A + B}{2} \in ℝ$
11	5 10	lenltd	$⊢ φ \to (M \leq \frac{A + B}{2} \leftrightarrow \neg \frac{A + B}{2} < M)$
12		avglt2	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow \frac{A + B}{2} < B)$
13	3 4 12	syl2anc	$⊢ φ \to (A < B \leftrightarrow \frac{A + B}{2} < B)$
14	8 13	mpbid	$⊢ φ \to \frac{A + B}{2} < B$
15		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})$
16	10 4 15	syl2anc	$⊢ φ \to (\frac{A + B}{2} < B \leftrightarrow \frac{A + B}{2} < \frac{(\frac{A + B}{2}) + B}{2})$
17	14 16	mpbid	$⊢ φ \to \frac{A + B}{2} < \frac{(\frac{A + B}{2}) + B}{2}$
18	10 4	readdcld	$⊢ φ \to (\frac{A + B}{2}) + B \in ℝ$
19	18	rehalfcld	$⊢ φ \to \frac{(\frac{A + B}{2}) + B}{2} \in ℝ$
20		lelttr	$⊢ (M \in ℝ \land \frac{A + B}{2} \in ℝ \land \frac{(\frac{A + B}{2}) + B}{2} \in ℝ) \to ((M \leq \frac{A + B}{2} \land \frac{A + B}{2} < \frac{(\frac{A + B}{2}) + B}{2}) \to M < \frac{(\frac{A + B}{2}) + B}{2})$
21	5 10 19 20	syl3anc	$⊢ φ \to ((M \leq \frac{A + B}{2} \land \frac{A + B}{2} < \frac{(\frac{A + B}{2}) + B}{2}) \to M < \frac{(\frac{A + B}{2}) + B}{2})$
22	17 21	mpan2d	$⊢ φ \to (M \leq \frac{A + B}{2} \to M < \frac{(\frac{A + B}{2}) + B}{2})$
23	11 22	sylbird	$⊢ φ \to (\neg \frac{A + B}{2} < M \to M < \frac{(\frac{A + B}{2}) + B}{2})$
24	23	imp	$⊢ (φ \land \neg \frac{A + B}{2} < M) \to M < \frac{(\frac{A + B}{2}) + B}{2}$
25	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))$
26	25	simp2d	$⊢ φ \to X = if (\frac{A + B}{2} < M, A, \frac{(\frac{A + B}{2}) + B}{2})$
27		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}$
28	26 27	sylan9eq	$⊢ (φ \land \neg \frac{A + B}{2} < M) \to X = \frac{(\frac{A + B}{2}) + B}{2}$
29	24 28	breqtrrd	$⊢ (φ \land \neg \frac{A + B}{2} < M) \to M < X$
30	29	ex	$⊢ φ \to (\neg \frac{A + B}{2} < M \to M < X)$
31	30	con1d	$⊢ φ \to (\neg M < X \to \frac{A + B}{2} < M)$
32	25	simp3d	$⊢ φ \to Y = if (\frac{A + B}{2} < M, \frac{A + B}{2}, B)$
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	sylan9eq	$⊢ (φ \land \frac{A + B}{2} < M) \to Y = \frac{A + B}{2}$
35		simpr	$⊢ (φ \land \frac{A + B}{2} < M) \to \frac{A + B}{2} < M$
36	34 35	eqbrtrd	$⊢ (φ \land \frac{A + B}{2} < M) \to Y < M$
37	36	ex	$⊢ φ \to (\frac{A + B}{2} < M \to Y < M)$
38	31 37	syld	$⊢ φ \to (\neg M < X \to Y < M)$
39	38	orrd	$⊢ φ \to (M < X \lor Y < M)$

Metamath Proof Explorer

Theorem ruclem3

Proof