Metamath Proof Explorer

Theorem esumfsupre

Description: Formulating an extended sum over integers using the recursive sequence builder. This version is limited to real-valued functions. (Contributed by Thierry Arnoux, 19-Oct-2017)

Ref Expression
Hypothesis esumfsup.1 
|- F/_ k F
Assertion esumfsupre 
|- ( F : NN --> ( 0 [,) +oo ) -> sum* k e. NN ( F ` k ) = sup ( ran seq 1 ( + , F ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 esumfsup.1 
 |-  F/_ k F
2 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
3 fss 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : NN --> ( 0 [,] +oo ) )
4 2 3 mpan2 
 |-  ( F : NN --> ( 0 [,) +oo ) -> F : NN --> ( 0 [,] +oo ) )
5 1 esumfsup 
 |-  ( F : NN --> ( 0 [,] +oo ) -> sum* k e. NN ( F ` k ) = sup ( ran seq 1 ( +e , F ) , RR* , < ) )
6 4 5 syl 
 |-  ( F : NN --> ( 0 [,) +oo ) -> sum* k e. NN ( F ` k ) = sup ( ran seq 1 ( +e , F ) , RR* , < ) )
7 1zzd 
 |-  ( F : NN --> ( 0 [,) +oo ) -> 1 e. ZZ )
8 elnnuz 
 |-  ( x e. NN <-> x e. ( ZZ>= ` 1 ) )
9 ffvelrn 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ x e. NN ) -> ( F ` x ) e. ( 0 [,) +oo ) )
10 8 9 sylan2br 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ x e. ( ZZ>= ` 1 ) ) -> ( F ` x ) e. ( 0 [,) +oo ) )
11 ge0addcl 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
12 11 adantl 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
13 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
14 simprl 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> x e. ( 0 [,) +oo ) )
15 13 14 sselid 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> x e. RR )
16 simprr 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> y e. ( 0 [,) +oo ) )
17 13 16 sselid 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> y e. RR )
18 rexadd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x +e y ) = ( x + y ) )
19 18 eqcomd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) = ( x +e y ) )
20 15 17 19 syl2anc 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) = ( x +e y ) )
21 7 10 12 20 seqfeq3 
 |-  ( F : NN --> ( 0 [,) +oo ) -> seq 1 ( + , F ) = seq 1 ( +e , F ) )
22 21 rneqd 
 |-  ( F : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , F ) = ran seq 1 ( +e , F ) )
23 22 supeq1d 
 |-  ( F : NN --> ( 0 [,) +oo ) -> sup ( ran seq 1 ( + , F ) , RR* , < ) = sup ( ran seq 1 ( +e , F ) , RR* , < ) )
24 6 23 eqtr4d 
 |-  ( F : NN --> ( 0 [,) +oo ) -> sum* k e. NN ( F ` k ) = sup ( ran seq 1 ( + , F ) , RR* , < ) )