ruclem6

Description: Lemma for ruc . Domain and codomain of the interval sequence. (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)⟩))$
	ruc.4	$⊢ C = \{⟨0, ⟨0, 1⟩⟩\} \cup F$
	ruc.5	$⊢ G = seq 0 (D, C)$
Assertion	ruclem6	$⊢ φ \to G : ℕ_{0} ⟶ ℝ^{2}$

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		ruc.4	$⊢ C = \{⟨0, ⟨0, 1⟩⟩\} \cup F$
4		ruc.5	$⊢ G = seq 0 (D, C)$
5	4	fveq1i	$⊢ G (0) = seq 0 (D, C) (0)$
6		0z	$⊢ 0 \in ℤ$
7		seq1	$⊢ 0 \in ℤ \to seq 0 (D, C) (0) = C (0)$
8	6 7	ax-mp	$⊢ seq 0 (D, C) (0) = C (0)$
9	5 8	eqtri	$⊢ G (0) = C (0)$
10	1 2 3 4	ruclem4	$⊢ φ \to G (0) = ⟨0, 1⟩$
11	9 10	eqtr3id	$⊢ φ \to C (0) = ⟨0, 1⟩$
12		0re	$⊢ 0 \in ℝ$
13		1re	$⊢ 1 \in ℝ$
14		opelxpi	$⊢ (0 \in ℝ \land 1 \in ℝ) \to ⟨0, 1⟩ \in ℝ^{2}$
15	12 13 14	mp2an	$⊢ ⟨0, 1⟩ \in ℝ^{2}$
16	11 15	eqeltrdi	$⊢ φ \to C (0) \in ℝ^{2}$
17		1st2nd2	$⊢ z \in ℝ^{2} \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
18	17	ad2antrl	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
19	18	oveq1d	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to z D w = ⟨1^{st} (z), 2^{nd} (z)⟩ D w$
20	1	adantr	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to F : ℕ ⟶ ℝ$
21	2	adantr	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \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)⟩))$
22		xp1st	$⊢ z \in ℝ^{2} \to 1^{st} (z) \in ℝ$
23	22	ad2antrl	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to 1^{st} (z) \in ℝ$
24		xp2nd	$⊢ z \in ℝ^{2} \to 2^{nd} (z) \in ℝ$
25	24	ad2antrl	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to 2^{nd} (z) \in ℝ$
26		simprr	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to w \in ℝ$
27		eqid	$⊢ 1^{st} (⟨1^{st} (z), 2^{nd} (z)⟩ D w) = 1^{st} (⟨1^{st} (z), 2^{nd} (z)⟩ D w)$
28		eqid	$⊢ 2^{nd} (⟨1^{st} (z), 2^{nd} (z)⟩ D w) = 2^{nd} (⟨1^{st} (z), 2^{nd} (z)⟩ D w)$
29	20 21 23 25 26 27 28	ruclem1	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to (⟨1^{st} (z), 2^{nd} (z)⟩ D w \in ℝ^{2} \land 1^{st} (⟨1^{st} (z), 2^{nd} (z)⟩ D w) = if (\frac{1^{st} (z) + 2^{nd} (z)}{2} < w, 1^{st} (z), \frac{(\frac{1^{st} (z) + 2^{nd} (z)}{2}) + 2^{nd} (z)}{2}) \land 2^{nd} (⟨1^{st} (z), 2^{nd} (z)⟩ D w) = if (\frac{1^{st} (z) + 2^{nd} (z)}{2} < w, \frac{1^{st} (z) + 2^{nd} (z)}{2}, 2^{nd} (z)))$
30	29	simp1d	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to ⟨1^{st} (z), 2^{nd} (z)⟩ D w \in ℝ^{2}$
31	19 30	eqeltrd	$⊢ (φ \land (z \in ℝ^{2} \land w \in ℝ)) \to z D w \in ℝ^{2}$
32		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
33		0zd	$⊢ φ \to 0 \in ℤ$
34		0p1e1	$⊢ 0 + 1 = 1$
35	34	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
36		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
37	35 36	eqtr4i	$⊢ ℤ_{\geq (0 + 1)} = ℕ$
38	37	eleq2i	$⊢ z \in ℤ_{\geq (0 + 1)} \leftrightarrow z \in ℕ$
39	3	equncomi	$⊢ C = F \cup \{⟨0, ⟨0, 1⟩⟩\}$
40	39	fveq1i	$⊢ C (z) = (F \cup \{⟨0, ⟨0, 1⟩⟩\}) (z)$
41		nnne0	$⊢ z \in ℕ \to z \neq 0$
42	41	necomd	$⊢ z \in ℕ \to 0 \neq z$
43		fvunsn	$⊢ 0 \neq z \to (F \cup \{⟨0, ⟨0, 1⟩⟩\}) (z) = F (z)$
44	42 43	syl	$⊢ z \in ℕ \to (F \cup \{⟨0, ⟨0, 1⟩⟩\}) (z) = F (z)$
45	40 44	eqtrid	$⊢ z \in ℕ \to C (z) = F (z)$
46	45	adantl	$⊢ (φ \land z \in ℕ) \to C (z) = F (z)$
47	1	ffvelcdmda	$⊢ (φ \land z \in ℕ) \to F (z) \in ℝ$
48	46 47	eqeltrd	$⊢ (φ \land z \in ℕ) \to C (z) \in ℝ$
49	38 48	sylan2b	$⊢ (φ \land z \in ℤ_{\geq (0 + 1)}) \to C (z) \in ℝ$
50	16 31 32 33 49	seqf2	$⊢ φ \to seq 0 (D, C) : ℕ_{0} ⟶ ℝ^{2}$
51	4	feq1i	$⊢ G : ℕ_{0} ⟶ ℝ^{2} \leftrightarrow seq 0 (D, C) : ℕ_{0} ⟶ ℝ^{2}$
52	50 51	sylibr	$⊢ φ \to G : ℕ_{0} ⟶ ℝ^{2}$

Metamath Proof Explorer

Theorem ruclem6

Proof