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 ) )