Theorem ovolsf

Description: Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

	Ref	Expression
Hypotheses	ovolfs.1	$$⊢G=\left(\mathrm{abs}\circ -\right)\circ F$$
	ovolfs.2	$$⊢S=seq1\left(+,G\right)$$
Assertion	ovolsf	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to S:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovolfs.1	$$⊢G=\left(\mathrm{abs}\circ -\right)\circ F$$
2		ovolfs.2	$$⊢S=seq1\left(+,G\right)$$
3		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
4		1zzd	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to 1\in \mathbb{Z}$$
5	1	ovolfsf	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to G:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$
6	5	ffvelcdmda	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge x\in \mathbb{N}\right)\to G\left(x\right)\in \left[0,\mathrm{+\infty }\right)$$
7		ge0addcl	$$⊢\left(x\in \left[0,\mathrm{+\infty }\right)\wedge y\in \left[0,\mathrm{+\infty }\right)\right)\to x+y\in \left[0,\mathrm{+\infty }\right)$$
8	7	adantl	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge \left(x\in \left[0,\mathrm{+\infty }\right)\wedge y\in \left[0,\mathrm{+\infty }\right)\right)\right)\to x+y\in \left[0,\mathrm{+\infty }\right)$$
9	3 4 6 8	seqf	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to seq1\left(+,G\right):\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$
10	2	feq1i	$$⊢S:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)\leftrightarrow seq1\left(+,G\right):\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$
11	9 10	sylibr	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to S:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$