# 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 = ( ( abs o. - ) o. F )`
ovolfs.2
`|- S = seq 1 ( + , G )`
Assertion ovolsf
`|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )`

### Proof

Step Hyp Ref Expression
1 ovolfs.1
` |-  G = ( ( abs o. - ) o. F )`
2 ovolfs.2
` |-  S = seq 1 ( + , G )`
3 nnuz
` |-  NN = ( ZZ>= ` 1 )`
4 1zzd
` |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> 1 e. ZZ )`
5 1 ovolfsf
` |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G : NN --> ( 0 [,) +oo ) )`
6 5 ffvelrnda
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( G ` x ) e. ( 0 [,) +oo ) )`
` |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )`
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,) +oo ) )`
` |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , G ) : NN --> ( 0 [,) +oo ) )`
` |-  ( S : NN --> ( 0 [,) +oo ) <-> seq 1 ( + , G ) : NN --> ( 0 [,) +oo ) )`
` |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )`