Theorem ruclem11

Description: Lemma for ruc . Closure lemmas for supremum. (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	ruclem11	$$⊢\phi \to \left(\mathrm{ran}\left(1^{st}\circ G\right)\subseteq ℝ\wedge \mathrm{ran}\left(1^{st}\circ G\right)\ne \varnothing \wedge \forall z\in \mathrm{ran}\left(1^{st}\circ G\right)z\le 1\right)$$

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	1 2 3 4	ruclem6	$$⊢\phi \to G:{\mathbb{N}}_0⟶{ℝ}^2$$
6		1stcof	$$⊢G:{\mathbb{N}}_0⟶{ℝ}^2\to \left(1^{st}\circ G\right):{\mathbb{N}}_0⟶ℝ$$
7	5 6	syl	$$⊢\phi \to \left(1^{st}\circ G\right):{\mathbb{N}}_0⟶ℝ$$
8	7	frnd	$$⊢\phi \to \mathrm{ran}\left(1^{st}\circ G\right)\subseteq ℝ$$
9	7	fdmd	$$⊢\phi \to \mathrm{dom}\left(1^{st}\circ G\right)={\mathbb{N}}_0$$
10		0nn0	$$⊢0\in {\mathbb{N}}_0$$
11		ne0i	$$⊢0\in {\mathbb{N}}_0\to {\mathbb{N}}_0\ne \varnothing$$
12	10 11	mp1i	$$⊢\phi \to {\mathbb{N}}_0\ne \varnothing$$
13	9 12	eqnetrd	$$⊢\phi \to \mathrm{dom}\left(1^{st}\circ G\right)\ne \varnothing$$
14		dm0rn0	$$⊢\mathrm{dom}\left(1^{st}\circ G\right)=\varnothing \leftrightarrow \mathrm{ran}\left(1^{st}\circ G\right)=\varnothing$$
15	14	necon3bii	$$⊢\mathrm{dom}\left(1^{st}\circ G\right)\ne \varnothing \leftrightarrow \mathrm{ran}\left(1^{st}\circ G\right)\ne \varnothing$$
16	13 15	sylib	$$⊢\phi \to \mathrm{ran}\left(1^{st}\circ G\right)\ne \varnothing$$
17		fvco3	$$⊢\left(G:{\mathbb{N}}_0⟶{ℝ}^2\wedge n\in {\mathbb{N}}_0\right)\to \left(1^{st}\circ G\right)\left(n\right)=1^{st}\left(G\left(n\right)\right)$$
18	5 17	sylan	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(1^{st}\circ G\right)\left(n\right)=1^{st}\left(G\left(n\right)\right)$$
19	1	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to F:\mathbb{N}⟶ℝ$$
20	2	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\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)$$
21		simpr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to n\in {\mathbb{N}}_0$$
22	10	a1i	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to 0\in {\mathbb{N}}_0$$
23	19 20 3 4 21 22	ruclem10	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to 1^{st}\left(G\left(n\right)\right)<2^{nd}\left(G\left(0\right)\right)$$
24	1 2 3 4	ruclem4	$$⊢\phi \to G\left(0\right)=⟨0,1⟩$$
25	24	fveq2d	$$⊢\phi \to 2^{nd}\left(G\left(0\right)\right)=2^{nd}\left(⟨0,1⟩\right)$$
26		c0ex	$$⊢0\in \mathrm{V}$$
27		1ex	$$⊢1\in \mathrm{V}$$
28	26 27	op2nd	$$⊢2^{nd}\left(⟨0,1⟩\right)=1$$
29	25 28	eqtrdi	$$⊢\phi \to 2^{nd}\left(G\left(0\right)\right)=1$$
30	29	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to 2^{nd}\left(G\left(0\right)\right)=1$$
31	23 30	breqtrd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to 1^{st}\left(G\left(n\right)\right)<1$$
32	5	ffvelcdmda	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to G\left(n\right)\in {ℝ}^2$$
33		xp1st	$$⊢G\left(n\right)\in {ℝ}^2\to 1^{st}\left(G\left(n\right)\right)\in ℝ$$
34	32 33	syl	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to 1^{st}\left(G\left(n\right)\right)\in ℝ$$
35		1re	$$⊢1\in ℝ$$
36		ltle	$$⊢\left(1^{st}\left(G\left(n\right)\right)\in ℝ\wedge 1\in ℝ\right)\to \left(1^{st}\left(G\left(n\right)\right)<1\to 1^{st}\left(G\left(n\right)\right)\le 1\right)$$
37	34 35 36	sylancl	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(1^{st}\left(G\left(n\right)\right)<1\to 1^{st}\left(G\left(n\right)\right)\le 1\right)$$
38	31 37	mpd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to 1^{st}\left(G\left(n\right)\right)\le 1$$
39	18 38	eqbrtrd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(1^{st}\circ G\right)\left(n\right)\le 1$$
40	39	ralrimiva	$$⊢\phi \to \forall n\in {\mathbb{N}}_0\left(1^{st}\circ G\right)\left(n\right)\le 1$$
41	7	ffnd	$$⊢\phi \to \left(1^{st}\circ G\right)Fn{\mathbb{N}}_0$$
42		breq1	$$⊢z=\left(1^{st}\circ G\right)\left(n\right)\to \left(z\le 1\leftrightarrow \left(1^{st}\circ G\right)\left(n\right)\le 1\right)$$
43	42	ralrn	$$⊢\left(1^{st}\circ G\right)Fn{\mathbb{N}}_0\to \left(\forall z\in \mathrm{ran}\left(1^{st}\circ G\right)z\le 1\leftrightarrow \forall n\in {\mathbb{N}}_0\left(1^{st}\circ G\right)\left(n\right)\le 1\right)$$
44	41 43	syl	$$⊢\phi \to \left(\forall z\in \mathrm{ran}\left(1^{st}\circ G\right)z\le 1\leftrightarrow \forall n\in {\mathbb{N}}_0\left(1^{st}\circ G\right)\left(n\right)\le 1\right)$$
45	40 44	mpbird	$$⊢\phi \to \forall z\in \mathrm{ran}\left(1^{st}\circ G\right)z\le 1$$
46	8 16 45	3jca	$$⊢\phi \to \left(\mathrm{ran}\left(1^{st}\circ G\right)\subseteq ℝ\wedge \mathrm{ran}\left(1^{st}\circ G\right)\ne \varnothing \wedge \forall z\in \mathrm{ran}\left(1^{st}\circ G\right)z\le 1\right)$$