Metamath Proof Explorer

Theorem esumsup

Description: Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020)

Ref Expression
Hypotheses esumsup.1 
|- ( ph -> B e. ( 0 [,] +oo ) )
esumsup.2 
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
Assertion esumsup 
|- ( ph -> sum* k e. NN A = sup ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 esumsup.1 
 |-  ( ph -> B e. ( 0 [,] +oo ) )
2 esumsup.2 
 |-  ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
3 2 fmpttd 
 |-  ( ph -> ( k e. NN |-> A ) : NN --> ( 0 [,] +oo ) )
4 nfmpt1 
 |-  F/_ k ( k e. NN |-> A )
5 4 esumfsup 
 |-  ( ( k e. NN |-> A ) : NN --> ( 0 [,] +oo ) -> sum* k e. NN ( ( k e. NN |-> A ) ` k ) = sup ( ran seq 1 ( +e , ( k e. NN |-> A ) ) , RR* , < ) )
6 3 5 syl 
 |-  ( ph -> sum* k e. NN ( ( k e. NN |-> A ) ` k ) = sup ( ran seq 1 ( +e , ( k e. NN |-> A ) ) , RR* , < ) )
7 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
8 eqid 
 |-  ( k e. NN |-> A ) = ( k e. NN |-> A )
9 8 fvmpt2 
 |-  ( ( k e. NN /\ A e. ( 0 [,] +oo ) ) -> ( ( k e. NN |-> A ) ` k ) = A )
10 7 2 9 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( k e. NN |-> A ) ` k ) = A )
11 10 esumeq2dv 
 |-  ( ph -> sum* k e. NN ( ( k e. NN |-> A ) ` k ) = sum* k e. NN A )
12 1z 
 |-  1 e. ZZ
13 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( +e , ( k e. NN |-> A ) ) Fn ( ZZ>= ` 1 ) )
14 12 13 ax-mp 
 |-  seq 1 ( +e , ( k e. NN |-> A ) ) Fn ( ZZ>= ` 1 )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 15 fneq2i 
 |-  ( seq 1 ( +e , ( k e. NN |-> A ) ) Fn NN <-> seq 1 ( +e , ( k e. NN |-> A ) ) Fn ( ZZ>= ` 1 ) )
17 14 16 mpbir 
 |-  seq 1 ( +e , ( k e. NN |-> A ) ) Fn NN
18 nfcv 
 |-  F/_ n seq 1 ( +e , ( k e. NN |-> A ) )
19 18 dffn5f 
 |-  ( seq 1 ( +e , ( k e. NN |-> A ) ) Fn NN <-> seq 1 ( +e , ( k e. NN |-> A ) ) = ( n e. NN |-> ( seq 1 ( +e , ( k e. NN |-> A ) ) ` n ) ) )
20 17 19 mpbi 
 |-  seq 1 ( +e , ( k e. NN |-> A ) ) = ( n e. NN |-> ( seq 1 ( +e , ( k e. NN |-> A ) ) ` n ) )
21 20 a1i 
 |-  ( ph -> seq 1 ( +e , ( k e. NN |-> A ) ) = ( n e. NN |-> ( seq 1 ( +e , ( k e. NN |-> A ) ) ` n ) ) )
22 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
23 22 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN )
24 23 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
25 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
26 25 24 2 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. ( 0 [,] +oo ) )
27 24 26 9 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( k e. NN |-> A ) ` k ) = A )
28 27 esumeq2dv 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( ( k e. NN |-> A ) ` k ) = sum* k e. ( 1 ... n ) A )
29 4 esumfzf 
 |-  ( ( ( k e. NN |-> A ) : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( ( k e. NN |-> A ) ` k ) = ( seq 1 ( +e , ( k e. NN |-> A ) ) ` n ) )
30 3 29 sylan 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( ( k e. NN |-> A ) ` k ) = ( seq 1 ( +e , ( k e. NN |-> A ) ) ` n ) )
31 28 30 eqtr3d 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) A = ( seq 1 ( +e , ( k e. NN |-> A ) ) ` n ) )
32 31 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> sum* k e. ( 1 ... n ) A ) = ( n e. NN |-> ( seq 1 ( +e , ( k e. NN |-> A ) ) ` n ) ) )
33 21 32 eqtr4d 
 |-  ( ph -> seq 1 ( +e , ( k e. NN |-> A ) ) = ( n e. NN |-> sum* k e. ( 1 ... n ) A ) )
34 33 rneqd 
 |-  ( ph -> ran seq 1 ( +e , ( k e. NN |-> A ) ) = ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) )
35 34 supeq1d 
 |-  ( ph -> sup ( ran seq 1 ( +e , ( k e. NN |-> A ) ) , RR* , < ) = sup ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) , RR* , < ) )
36 6 11 35 3eqtr3d 
 |-  ( ph -> sum* k e. NN A = sup ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) , RR* , < ) )