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