# Metamath Proof Explorer

## 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}:ℕ⟶\le \cap {ℝ}^{2}\to {S}:ℕ⟶\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 ${⊢}ℕ={ℤ}_{\ge 1}$
4 1zzd ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to 1\in ℤ$
5 1 ovolfsf ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {G}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
6 5 ffvelrnda ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\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}:ℕ⟶\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}:ℕ⟶\le \cap {ℝ}^{2}\to seq1\left(+,{G}\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
10 2 feq1i ${⊢}{S}:ℕ⟶\left[0,\mathrm{+\infty }\right)↔seq1\left(+,{G}\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
11 9 10 sylibr ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$