Theorem ruclem4

Description: Lemma for ruc . Initial value of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypotheses	ruc.1	$$⊢\phi \to F:\mathbb{N}⟶ℝ$$
	ruc.2	$$⊢\phi \to D=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)$$
	ruc.4	$$⊢C=\left\{⟨0,⟨0,1⟩⟩\right\}\cup F$$
	ruc.5	$$⊢G=seq0\left(D,C\right)$$
Assertion	ruclem4	$$⊢\phi \to G\left(0\right)=⟨0,1⟩$$

Proof

Step	Hyp	Ref	Expression
1		ruc.1	$$⊢\phi \to F:\mathbb{N}⟶ℝ$$
2		ruc.2	$$⊢\phi \to D=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)$$
3		ruc.4	$$⊢C=\left\{⟨0,⟨0,1⟩⟩\right\}\cup F$$
4		ruc.5	$$⊢G=seq0\left(D,C\right)$$
5	4	fveq1i	$$⊢G\left(0\right)=seq0\left(D,C\right)\left(0\right)$$
6		0z	$$⊢0\in \mathbb{Z}$$
7		dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$
8	7	reseq2i	$$⊢{F\upharpoonright }_{\mathbb{N}}={F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}$$
9		ffn	$$⊢F:\mathbb{N}⟶ℝ\to FFn\mathbb{N}$$
10		fnresdm	$$⊢FFn\mathbb{N}\to {F\upharpoonright }_{\mathbb{N}}=F$$
11	1 9 10	3syl	$$⊢\phi \to {F\upharpoonright }_{\mathbb{N}}=F$$
12	8 11	syl5reqr	$$⊢\phi \to F={F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}$$
13	12	uneq2d	$$⊢\phi \to \left\{⟨0,⟨0,1⟩⟩\right\}\cup F=\left\{⟨0,⟨0,1⟩⟩\right\}\cup \left({F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)$$
14	3 13	syl5eq	$$⊢\phi \to C=\left\{⟨0,⟨0,1⟩⟩\right\}\cup \left({F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)$$
15	14	fveq1d	$$⊢\phi \to C\left(0\right)=\left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup \left({F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)\right)\left(0\right)$$
16		c0ex	$$⊢0\in \mathrm{V}$$
17	16	a1i	$$⊢\top \to 0\in \mathrm{V}$$
18		opex	$$⊢⟨0,1⟩\in \mathrm{V}$$
19	18	a1i	$$⊢\top \to ⟨0,1⟩\in \mathrm{V}$$
20		eqid	$$⊢\left\{⟨0,⟨0,1⟩⟩\right\}\cup \left({F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)=\left\{⟨0,⟨0,1⟩⟩\right\}\cup \left({F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)$$
21	17 19 20	fvsnun1	$$⊢\top \to \left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup \left({F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)\right)\left(0\right)=⟨0,1⟩$$
22	21	mptru	$$⊢\left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup \left({F\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)\right)\left(0\right)=⟨0,1⟩$$
23	15 22	syl6eq	$$⊢\phi \to C\left(0\right)=⟨0,1⟩$$
24	6 23	seq1i	$$⊢\phi \to seq0\left(D,C\right)\left(0\right)=⟨0,1⟩$$
25	5 24	syl5eq	$$⊢\phi \to G\left(0\right)=⟨0,1⟩$$