ruclem1

Description: Lemma for ruc (the reals are uncountable). Substitutions for the function D . (Contributed by Mario Carneiro, 28-May-2014) (Revised by Fan Zheng, 6-Jun-2016)

	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)$
Assertion	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))$

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	2	oveqd	$⊢ φ \to ⟨A, B⟩ D M = ⟨A, B⟩ (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)⟩)) M$
9	3 4	opelxpd	$⊢ φ \to ⟨A, B⟩ \in ℝ^{2}$
10		simpr	$⊢ (x = ⟨A, B⟩ \land y = M) \to y = M$
11	10	breq2d	$⊢ (x = ⟨A, B⟩ \land y = M) \to (m < y \leftrightarrow m < M)$
12		simpl	$⊢ (x = ⟨A, B⟩ \land y = M) \to x = ⟨A, B⟩$
13	12	fveq2d	$⊢ (x = ⟨A, B⟩ \land y = M) \to 1^{st} (x) = 1^{st} (⟨A, B⟩)$
14	13	opeq1d	$⊢ (x = ⟨A, B⟩ \land y = M) \to ⟨1^{st} (x), m⟩ = ⟨1^{st} (⟨A, B⟩), m⟩$
15	12	fveq2d	$⊢ (x = ⟨A, B⟩ \land y = M) \to 2^{nd} (x) = 2^{nd} (⟨A, B⟩)$
16	15	oveq2d	$⊢ (x = ⟨A, B⟩ \land y = M) \to m + 2^{nd} (x) = m + 2^{nd} (⟨A, B⟩)$
17	16	oveq1d	$⊢ (x = ⟨A, B⟩ \land y = M) \to \frac{m + 2^{nd} (x)}{2} = \frac{m + 2^{nd} (⟨A, B⟩)}{2}$
18	17 15	opeq12d	$⊢ (x = ⟨A, B⟩ \land y = M) \to ⟨\frac{m + 2^{nd} (x)}{2}, 2^{nd} (x)⟩ = ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩$
19	11 14 18	ifbieq12d	$⊢ (x = ⟨A, B⟩ \land y = M) \to if (m < y, ⟨1^{st} (x), m⟩, ⟨\frac{m + 2^{nd} (x)}{2}, 2^{nd} (x)⟩) = if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
20	19	csbeq2dv	$⊢ (x = ⟨A, B⟩ \land y = M) \to ⦋ (\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)⟩) = ⦋ (\frac{1^{st} (x) + 2^{nd} (x)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
21	13 15	oveq12d	$⊢ (x = ⟨A, B⟩ \land y = M) \to 1^{st} (x) + 2^{nd} (x) = 1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)$
22	21	oveq1d	$⊢ (x = ⟨A, B⟩ \land y = M) \to \frac{1^{st} (x) + 2^{nd} (x)}{2} = \frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}$
23	22	csbeq1d	$⊢ (x = ⟨A, B⟩ \land y = M) \to ⦋ (\frac{1^{st} (x) + 2^{nd} (x)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) = ⦋ (\frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
24	20 23	eqtrd	$⊢ (x = ⟨A, B⟩ \land y = M) \to ⦋ (\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)⟩) = ⦋ (\frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
25		eqid	$⊢ (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)⟩)) = (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)⟩))$
26		opex	$⊢ ⟨1^{st} (⟨A, B⟩), m⟩ \in V$
27		opex	$⊢ ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩ \in V$
28	26 27	ifex	$⊢ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) \in V$
29	28	csbex	$⊢ ⦋ (\frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) \in V$
30	24 25 29	ovmpoa	$⊢ (⟨A, B⟩ \in ℝ^{2} \land M \in ℝ) \to ⟨A, B⟩ (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)⟩)) M = ⦋ (\frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
31	9 5 30	syl2anc	$⊢ φ \to ⟨A, B⟩ (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)⟩)) M = ⦋ (\frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
32	8 31	eqtrd	$⊢ φ \to ⟨A, B⟩ D M = ⦋ (\frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
33		op1stg	$⊢ (A \in ℝ \land B \in ℝ) \to 1^{st} (⟨A, B⟩) = A$
34	3 4 33	syl2anc	$⊢ φ \to 1^{st} (⟨A, B⟩) = A$
35		op2ndg	$⊢ (A \in ℝ \land B \in ℝ) \to 2^{nd} (⟨A, B⟩) = B$
36	3 4 35	syl2anc	$⊢ φ \to 2^{nd} (⟨A, B⟩) = B$
37	34 36	oveq12d	$⊢ φ \to 1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩) = A + B$
38	37	oveq1d	$⊢ φ \to \frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2} = \frac{A + B}{2}$
39	38	csbeq1d	$⊢ φ \to ⦋ (\frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) = ⦋ (\frac{A + B}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
40		ovex	$⊢ \frac{A + B}{2} \in V$
41		breq1	$⊢ m = \frac{A + B}{2} \to (m < M \leftrightarrow \frac{A + B}{2} < M)$
42		opeq2	$⊢ m = \frac{A + B}{2} \to ⟨1^{st} (⟨A, B⟩), m⟩ = ⟨1^{st} (⟨A, B⟩), \frac{A + B}{2}⟩$
43		oveq1	$⊢ m = \frac{A + B}{2} \to m + 2^{nd} (⟨A, B⟩) = (\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩)$
44	43	oveq1d	$⊢ m = \frac{A + B}{2} \to \frac{m + 2^{nd} (⟨A, B⟩)}{2} = \frac{(\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩)}{2}$
45	44	opeq1d	$⊢ m = \frac{A + B}{2} \to ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩ = ⟨\frac{(\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩$
46	41 42 45	ifbieq12d	$⊢ m = \frac{A + B}{2} \to if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) = if (\frac{A + B}{2} < M, ⟨1^{st} (⟨A, B⟩), \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
47	40 46	csbie	$⊢ ⦋ (\frac{A + B}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) = if (\frac{A + B}{2} < M, ⟨1^{st} (⟨A, B⟩), \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩)$
48	34	opeq1d	$⊢ φ \to ⟨1^{st} (⟨A, B⟩), \frac{A + B}{2}⟩ = ⟨A, \frac{A + B}{2}⟩$
49	36	oveq2d	$⊢ φ \to (\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩) = (\frac{A + B}{2}) + B$
50	49	oveq1d	$⊢ φ \to \frac{(\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩)}{2} = \frac{(\frac{A + B}{2}) + B}{2}$
51	50 36	opeq12d	$⊢ φ \to ⟨\frac{(\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩ = ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩$
52	48 51	ifeq12d	$⊢ φ \to if (\frac{A + B}{2} < M, ⟨1^{st} (⟨A, B⟩), \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) = if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)$
53	47 52	syl5eq	$⊢ φ \to ⦋ (\frac{A + B}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) = if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)$
54	39 53	eqtrd	$⊢ φ \to ⦋ (\frac{1^{st} (⟨A, B⟩) + 2^{nd} (⟨A, B⟩)}{2}) / m ⦌ if (m < M, ⟨1^{st} (⟨A, B⟩), m⟩, ⟨\frac{m + 2^{nd} (⟨A, B⟩)}{2}, 2^{nd} (⟨A, B⟩)⟩) = if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)$
55	32 54	eqtrd	$⊢ φ \to ⟨A, B⟩ D M = if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)$
56	3 4	readdcld	$⊢ φ \to A + B \in ℝ$
57	56	rehalfcld	$⊢ φ \to \frac{A + B}{2} \in ℝ$
58	3 57	opelxpd	$⊢ φ \to ⟨A, \frac{A + B}{2}⟩ \in ℝ^{2}$
59	57 4	readdcld	$⊢ φ \to (\frac{A + B}{2}) + B \in ℝ$
60	59	rehalfcld	$⊢ φ \to \frac{(\frac{A + B}{2}) + B}{2} \in ℝ$
61	60 4	opelxpd	$⊢ φ \to ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩ \in ℝ^{2}$
62	58 61	ifcld	$⊢ φ \to if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩) \in ℝ^{2}$
63	55 62	eqeltrd	$⊢ φ \to ⟨A, B⟩ D M \in ℝ^{2}$
64	55	fveq2d	$⊢ φ \to 1^{st} (⟨A, B⟩ D M) = 1^{st} (if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩))$
65		fvif	$⊢ 1^{st} (if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)) = if (\frac{A + B}{2} < M, 1^{st} (⟨A, \frac{A + B}{2}⟩), 1^{st} (⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩))$
66		op1stg	$⊢ (A \in ℝ \land \frac{A + B}{2} \in V) \to 1^{st} (⟨A, \frac{A + B}{2}⟩) = A$
67	3 40 66	sylancl	$⊢ φ \to 1^{st} (⟨A, \frac{A + B}{2}⟩) = A$
68		ovex	$⊢ \frac{(\frac{A + B}{2}) + B}{2} \in V$
69		op1stg	$⊢ (\frac{(\frac{A + B}{2}) + B}{2} \in V \land B \in ℝ) \to 1^{st} (⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩) = \frac{(\frac{A + B}{2}) + B}{2}$
70	68 4 69	sylancr	$⊢ φ \to 1^{st} (⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩) = \frac{(\frac{A + B}{2}) + B}{2}$
71	67 70	ifeq12d	$⊢ φ \to if (\frac{A + B}{2} < M, 1^{st} (⟨A, \frac{A + B}{2}⟩), 1^{st} (⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)) = if (\frac{A + B}{2} < M, A, \frac{(\frac{A + B}{2}) + B}{2})$
72	65 71	syl5eq	$⊢ φ \to 1^{st} (if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)) = if (\frac{A + B}{2} < M, A, \frac{(\frac{A + B}{2}) + B}{2})$
73	64 72	eqtrd	$⊢ φ \to 1^{st} (⟨A, B⟩ D M) = if (\frac{A + B}{2} < M, A, \frac{(\frac{A + B}{2}) + B}{2})$
74	6 73	syl5eq	$⊢ φ \to X = if (\frac{A + B}{2} < M, A, \frac{(\frac{A + B}{2}) + B}{2})$
75	55	fveq2d	$⊢ φ \to 2^{nd} (⟨A, B⟩ D M) = 2^{nd} (if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩))$
76		fvif	$⊢ 2^{nd} (if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)) = if (\frac{A + B}{2} < M, 2^{nd} (⟨A, \frac{A + B}{2}⟩), 2^{nd} (⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩))$
77		op2ndg	$⊢ (A \in ℝ \land \frac{A + B}{2} \in V) \to 2^{nd} (⟨A, \frac{A + B}{2}⟩) = \frac{A + B}{2}$
78	3 40 77	sylancl	$⊢ φ \to 2^{nd} (⟨A, \frac{A + B}{2}⟩) = \frac{A + B}{2}$
79		op2ndg	$⊢ (\frac{(\frac{A + B}{2}) + B}{2} \in V \land B \in ℝ) \to 2^{nd} (⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩) = B$
80	68 4 79	sylancr	$⊢ φ \to 2^{nd} (⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩) = B$
81	78 80	ifeq12d	$⊢ φ \to if (\frac{A + B}{2} < M, 2^{nd} (⟨A, \frac{A + B}{2}⟩), 2^{nd} (⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)) = if (\frac{A + B}{2} < M, \frac{A + B}{2}, B)$
82	76 81	syl5eq	$⊢ φ \to 2^{nd} (if (\frac{A + B}{2} < M, ⟨A, \frac{A + B}{2}⟩, ⟨\frac{(\frac{A + B}{2}) + B}{2}, B⟩)) = if (\frac{A + B}{2} < M, \frac{A + B}{2}, B)$
83	75 82	eqtrd	$⊢ φ \to 2^{nd} (⟨A, B⟩ D M) = if (\frac{A + B}{2} < M, \frac{A + B}{2}, B)$
84	7 83	syl5eq	$⊢ φ \to Y = if (\frac{A + B}{2} < M, \frac{A + B}{2}, B)$
85	63 74 84	3jca	$⊢ φ \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))$

Metamath Proof Explorer

Theorem ruclem1

Proof