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 ) )
7 ge0addcl
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
8 7 adantl
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
9 3 4 6 8 seqf
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , G ) : NN --> ( 0 [,) +oo ) )
10 2 feq1i
 |-  ( S : NN --> ( 0 [,) +oo ) <-> seq 1 ( + , G ) : NN --> ( 0 [,) +oo ) )
11 9 10 sylibr
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )