Metamath Proof Explorer

Theorem esumfsup

Description: Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 esumfsup.1 
 |-  F/_ k F
2 1z 
 |-  1 e. ZZ
3 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( +e , F ) Fn ( ZZ>= ` 1 ) )
4 2 3 ax-mp 
 |-  seq 1 ( +e , F ) Fn ( ZZ>= ` 1 )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 5 fneq2i 
 |-  ( seq 1 ( +e , F ) Fn NN <-> seq 1 ( +e , F ) Fn ( ZZ>= ` 1 ) )
7 4 6 mpbir 
 |-  seq 1 ( +e , F ) Fn NN
8 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
9 1 esumfzf 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) )
10 ovex 
 |-  ( 1 ... n ) e. _V
11 nfcv 
 |-  F/_ k NN
12 nfcv 
 |-  F/_ k ( 0 [,] +oo )
13 1 11 12 nff 
 |-  F/ k F : NN --> ( 0 [,] +oo )
14 nfv 
 |-  F/ k n e. NN
15 13 14 nfan 
 |-  F/ k ( F : NN --> ( 0 [,] +oo ) /\ n e. NN )
16 simpll 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> F : NN --> ( 0 [,] +oo ) )
17 1nn 
 |-  1 e. NN
18 fzssnn 
 |-  ( 1 e. NN -> ( 1 ... n ) C_ NN )
19 17 18 mp1i 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( 1 ... n ) C_ NN )
20 simpr 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. ( 1 ... n ) )
21 19 20 sseldd 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
22 16 21 ffvelrnd 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( F ` k ) e. ( 0 [,] +oo ) )
23 22 ex 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> ( k e. ( 1 ... n ) -> ( F ` k ) e. ( 0 [,] +oo ) ) )
24 15 23 ralrimi 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> A. k e. ( 1 ... n ) ( F ` k ) e. ( 0 [,] +oo ) )
25 nfcv 
 |-  F/_ k ( 1 ... n )
26 25 esumcl 
 |-  ( ( ( 1 ... n ) e. _V /\ A. k e. ( 1 ... n ) ( F ` k ) e. ( 0 [,] +oo ) ) -> sum* k e. ( 1 ... n ) ( F ` k ) e. ( 0 [,] +oo ) )
27 10 24 26 sylancr 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( F ` k ) e. ( 0 [,] +oo ) )
28 9 27 eqeltrrd 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> ( seq 1 ( +e , F ) ` n ) e. ( 0 [,] +oo ) )
29 8 28 sseldi 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> ( seq 1 ( +e , F ) ` n ) e. RR* )
30 29 ralrimiva 
 |-  ( F : NN --> ( 0 [,] +oo ) -> A. n e. NN ( seq 1 ( +e , F ) ` n ) e. RR* )
31 fnfvrnss 
 |-  ( ( seq 1 ( +e , F ) Fn NN /\ A. n e. NN ( seq 1 ( +e , F ) ` n ) e. RR* ) -> ran seq 1 ( +e , F ) C_ RR* )
32 7 30 31 sylancr 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ran seq 1 ( +e , F ) C_ RR* )
33 nnex 
 |-  NN e. _V
34 ffvelrn 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ k e. NN ) -> ( F ` k ) e. ( 0 [,] +oo ) )
35 34 ex 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( k e. NN -> ( F ` k ) e. ( 0 [,] +oo ) ) )
36 13 35 ralrimi 
 |-  ( F : NN --> ( 0 [,] +oo ) -> A. k e. NN ( F ` k ) e. ( 0 [,] +oo ) )
37 11 esumcl 
 |-  ( ( NN e. _V /\ A. k e. NN ( F ` k ) e. ( 0 [,] +oo ) ) -> sum* k e. NN ( F ` k ) e. ( 0 [,] +oo ) )
38 33 36 37 sylancr 
 |-  ( F : NN --> ( 0 [,] +oo ) -> sum* k e. NN ( F ` k ) e. ( 0 [,] +oo ) )
39 8 38 sseldi 
 |-  ( F : NN --> ( 0 [,] +oo ) -> sum* k e. NN ( F ` k ) e. RR* )
40 fvelrnb 
 |-  ( seq 1 ( +e , F ) Fn NN -> ( x e. ran seq 1 ( +e , F ) <-> E. n e. NN ( seq 1 ( +e , F ) ` n ) = x ) )
41 7 40 mp1i 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( x e. ran seq 1 ( +e , F ) <-> E. n e. NN ( seq 1 ( +e , F ) ` n ) = x ) )
42 eqcom 
 |-  ( sum* k e. ( 1 ... n ) ( F ` k ) = x <-> x = sum* k e. ( 1 ... n ) ( F ` k ) )
43 9 eqeq1d 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> ( sum* k e. ( 1 ... n ) ( F ` k ) = x <-> ( seq 1 ( +e , F ) ` n ) = x ) )
44 42 43 bitr3id 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> ( x = sum* k e. ( 1 ... n ) ( F ` k ) <-> ( seq 1 ( +e , F ) ` n ) = x ) )
45 44 rexbidva 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( E. n e. NN x = sum* k e. ( 1 ... n ) ( F ` k ) <-> E. n e. NN ( seq 1 ( +e , F ) ` n ) = x ) )
46 41 45 bitr4d 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( x e. ran seq 1 ( +e , F ) <-> E. n e. NN x = sum* k e. ( 1 ... n ) ( F ` k ) ) )
47 46 biimpa 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ x e. ran seq 1 ( +e , F ) ) -> E. n e. NN x = sum* k e. ( 1 ... n ) ( F ` k ) )
48 33 a1i 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> NN e. _V )
49 34 adantlr 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) /\ k e. NN ) -> ( F ` k ) e. ( 0 [,] +oo ) )
50 17 18 mp1i 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> ( 1 ... n ) C_ NN )
51 15 48 49 50 esummono 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) )
52 51 ralrimiva 
 |-  ( F : NN --> ( 0 [,] +oo ) -> A. n e. NN sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) )
53 52 adantr 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ x e. ran seq 1 ( +e , F ) ) -> A. n e. NN sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) )
54 47 53 jca 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ x e. ran seq 1 ( +e , F ) ) -> ( E. n e. NN x = sum* k e. ( 1 ... n ) ( F ` k ) /\ A. n e. NN sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) ) )
55 r19.29r 
 |-  ( ( E. n e. NN x = sum* k e. ( 1 ... n ) ( F ` k ) /\ A. n e. NN sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) ) -> E. n e. NN ( x = sum* k e. ( 1 ... n ) ( F ` k ) /\ sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) ) )
56 breq1 
 |-  ( x = sum* k e. ( 1 ... n ) ( F ` k ) -> ( x <_ sum* k e. NN ( F ` k ) <-> sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) ) )
57 56 biimpar 
 |-  ( ( x = sum* k e. ( 1 ... n ) ( F ` k ) /\ sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) ) -> x <_ sum* k e. NN ( F ` k ) )
58 57 rexlimivw 
 |-  ( E. n e. NN ( x = sum* k e. ( 1 ... n ) ( F ` k ) /\ sum* k e. ( 1 ... n ) ( F ` k ) <_ sum* k e. NN ( F ` k ) ) -> x <_ sum* k e. NN ( F ` k ) )
59 54 55 58 3syl 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ x e. ran seq 1 ( +e , F ) ) -> x <_ sum* k e. NN ( F ` k ) )
60 59 ralrimiva 
 |-  ( F : NN --> ( 0 [,] +oo ) -> A. x e. ran seq 1 ( +e , F ) x <_ sum* k e. NN ( F ` k ) )
61 nfv 
 |-  F/ k x e. RR
62 13 61 nfan 
 |-  F/ k ( F : NN --> ( 0 [,] +oo ) /\ x e. RR )
63 nfcv 
 |-  F/_ k x
64 nfcv 
 |-  F/_ k <
65 11 nfesum1 
 |-  F/_ k sum* k e. NN ( F ` k )
66 63 64 65 nfbr 
 |-  F/ k x < sum* k e. NN ( F ` k )
67 62 66 nfan 
 |-  F/ k ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) )
68 33 a1i 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> NN e. _V )
69 simplll 
 |-  ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ k e. NN ) -> F : NN --> ( 0 [,] +oo ) )
70 69 34 sylancom 
 |-  ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ k e. NN ) -> ( F ` k ) e. ( 0 [,] +oo ) )
71 simplr 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> x e. RR )
72 71 rexrd 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> x e. RR* )
73 simpr 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> x < sum* k e. NN ( F ` k ) )
74 67 68 70 72 73 esumlub 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> E. a e. ( ~P NN i^i Fin ) x < sum* k e. a ( F ` k ) )
75 ssnnssfz 
 |-  ( a e. ( ~P NN i^i Fin ) -> E. n e. NN a C_ ( 1 ... n ) )
76 r19.42v 
 |-  ( E. n e. NN ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) <-> ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ E. n e. NN a C_ ( 1 ... n ) ) )
77 nfv 
 |-  F/ k a C_ ( 1 ... n )
78 67 77 nfan 
 |-  F/ k ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) )
79 10 a1i 
 |-  ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) -> ( 1 ... n ) e. _V )
80 simp-4l 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) /\ k e. ( 1 ... n ) ) -> F : NN --> ( 0 [,] +oo ) )
81 17 18 ax-mp 
 |-  ( 1 ... n ) C_ NN
82 simpr 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) /\ k e. ( 1 ... n ) ) -> k e. ( 1 ... n ) )
83 81 82 sseldi 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) /\ k e. ( 1 ... n ) ) -> k e. NN )
84 80 83 ffvelrnd 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) /\ k e. ( 1 ... n ) ) -> ( F ` k ) e. ( 0 [,] +oo ) )
85 simpr 
 |-  ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) -> a C_ ( 1 ... n ) )
86 78 79 84 85 esummono 
 |-  ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) -> sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) )
87 86 reximi 
 |-  ( E. n e. NN ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a C_ ( 1 ... n ) ) -> E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) )
88 76 87 sylbir 
 |-  ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ E. n e. NN a C_ ( 1 ... n ) ) -> E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) )
89 75 88 sylan2 
 |-  ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) -> E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) )
90 89 ralrimiva 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> A. a e. ( ~P NN i^i Fin ) E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) )
91 r19.29r 
 |-  ( ( E. a e. ( ~P NN i^i Fin ) x < sum* k e. a ( F ` k ) /\ A. a e. ( ~P NN i^i Fin ) E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) -> E. a e. ( ~P NN i^i Fin ) ( x < sum* k e. a ( F ` k ) /\ E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) )
92 r19.42v 
 |-  ( E. n e. NN ( x < sum* k e. a ( F ` k ) /\ sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) <-> ( x < sum* k e. a ( F ` k ) /\ E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) )
93 92 rexbii 
 |-  ( E. a e. ( ~P NN i^i Fin ) E. n e. NN ( x < sum* k e. a ( F ` k ) /\ sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) <-> E. a e. ( ~P NN i^i Fin ) ( x < sum* k e. a ( F ` k ) /\ E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) )
94 91 93 sylibr 
 |-  ( ( E. a e. ( ~P NN i^i Fin ) x < sum* k e. a ( F ` k ) /\ A. a e. ( ~P NN i^i Fin ) E. n e. NN sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) -> E. a e. ( ~P NN i^i Fin ) E. n e. NN ( x < sum* k e. a ( F ` k ) /\ sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) )
95 74 90 94 syl2anc 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> E. a e. ( ~P NN i^i Fin ) E. n e. NN ( x < sum* k e. a ( F ` k ) /\ sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) )
96 simp-4r 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> x e. RR )
97 96 rexrd 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> x e. RR* )
98 vex 
 |-  a e. _V
99 nfcv 
 |-  F/_ k a
100 99 nfel1 
 |-  F/ k a e. ( ~P NN i^i Fin )
101 67 100 nfan 
 |-  F/ k ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) )
102 101 14 nfan 
 |-  F/ k ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN )
103 simp-5l 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. a ) -> F : NN --> ( 0 [,] +oo ) )
104 simpllr 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. a ) -> a e. ( ~P NN i^i Fin ) )
105 inss1 
 |-  ( ~P NN i^i Fin ) C_ ~P NN
106 105 sseli 
 |-  ( a e. ( ~P NN i^i Fin ) -> a e. ~P NN )
107 elpwi 
 |-  ( a e. ~P NN -> a C_ NN )
108 104 106 107 3syl 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. a ) -> a C_ NN )
109 simpr 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. a ) -> k e. a )
110 108 109 sseldd 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. a ) -> k e. NN )
111 103 110 ffvelrnd 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. a ) -> ( F ` k ) e. ( 0 [,] +oo ) )
112 111 ex 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> ( k e. a -> ( F ` k ) e. ( 0 [,] +oo ) ) )
113 102 112 ralrimi 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> A. k e. a ( F ` k ) e. ( 0 [,] +oo ) )
114 99 esumcl 
 |-  ( ( a e. _V /\ A. k e. a ( F ` k ) e. ( 0 [,] +oo ) ) -> sum* k e. a ( F ` k ) e. ( 0 [,] +oo ) )
115 98 113 114 sylancr 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> sum* k e. a ( F ` k ) e. ( 0 [,] +oo ) )
116 8 115 sseldi 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> sum* k e. a ( F ` k ) e. RR* )
117 simp-5l 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> F : NN --> ( 0 [,] +oo ) )
118 simpr 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. ( 1 ... n ) )
119 81 118 sseldi 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
120 117 119 ffvelrnd 
 |-  ( ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( F ` k ) e. ( 0 [,] +oo ) )
121 120 ex 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> ( k e. ( 1 ... n ) -> ( F ` k ) e. ( 0 [,] +oo ) ) )
122 102 121 ralrimi 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> A. k e. ( 1 ... n ) ( F ` k ) e. ( 0 [,] +oo ) )
123 10 122 26 sylancr 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( F ` k ) e. ( 0 [,] +oo ) )
124 8 123 sseldi 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( F ` k ) e. RR* )
125 xrltletr 
 |-  ( ( x e. RR* /\ sum* k e. a ( F ` k ) e. RR* /\ sum* k e. ( 1 ... n ) ( F ` k ) e. RR* ) -> ( ( x < sum* k e. a ( F ` k ) /\ sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) -> x < sum* k e. ( 1 ... n ) ( F ` k ) ) )
126 97 116 124 125 syl3anc 
 |-  ( ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) /\ n e. NN ) -> ( ( x < sum* k e. a ( F ` k ) /\ sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) -> x < sum* k e. ( 1 ... n ) ( F ` k ) ) )
127 126 reximdva 
 |-  ( ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) /\ a e. ( ~P NN i^i Fin ) ) -> ( E. n e. NN ( x < sum* k e. a ( F ` k ) /\ sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) -> E. n e. NN x < sum* k e. ( 1 ... n ) ( F ` k ) ) )
128 127 rexlimdva 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> ( E. a e. ( ~P NN i^i Fin ) E. n e. NN ( x < sum* k e. a ( F ` k ) /\ sum* k e. a ( F ` k ) <_ sum* k e. ( 1 ... n ) ( F ` k ) ) -> E. n e. NN x < sum* k e. ( 1 ... n ) ( F ` k ) ) )
129 95 128 mpd 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> E. n e. NN x < sum* k e. ( 1 ... n ) ( F ` k ) )
130 fvelrnb 
 |-  ( seq 1 ( +e , F ) Fn NN -> ( y e. ran seq 1 ( +e , F ) <-> E. n e. NN ( seq 1 ( +e , F ) ` n ) = y ) )
131 7 130 mp1i 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( y e. ran seq 1 ( +e , F ) <-> E. n e. NN ( seq 1 ( +e , F ) ` n ) = y ) )
132 eqcom 
 |-  ( sum* k e. ( 1 ... n ) ( F ` k ) = y <-> y = sum* k e. ( 1 ... n ) ( F ` k ) )
133 9 eqeq1d 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> ( sum* k e. ( 1 ... n ) ( F ` k ) = y <-> ( seq 1 ( +e , F ) ` n ) = y ) )
134 132 133 bitr3id 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ n e. NN ) -> ( y = sum* k e. ( 1 ... n ) ( F ` k ) <-> ( seq 1 ( +e , F ) ` n ) = y ) )
135 134 rexbidva 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( E. n e. NN y = sum* k e. ( 1 ... n ) ( F ` k ) <-> E. n e. NN ( seq 1 ( +e , F ) ` n ) = y ) )
136 131 135 bitr4d 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( y e. ran seq 1 ( +e , F ) <-> E. n e. NN y = sum* k e. ( 1 ... n ) ( F ` k ) ) )
137 simpr 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ y = sum* k e. ( 1 ... n ) ( F ` k ) ) -> y = sum* k e. ( 1 ... n ) ( F ` k ) )
138 137 breq2d 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ y = sum* k e. ( 1 ... n ) ( F ` k ) ) -> ( x < y <-> x < sum* k e. ( 1 ... n ) ( F ` k ) ) )
139 27 136 138 rexxfr2d 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( E. y e. ran seq 1 ( +e , F ) x < y <-> E. n e. NN x < sum* k e. ( 1 ... n ) ( F ` k ) ) )
140 139 ad2antrr 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> ( E. y e. ran seq 1 ( +e , F ) x < y <-> E. n e. NN x < sum* k e. ( 1 ... n ) ( F ` k ) ) )
141 129 140 mpbird 
 |-  ( ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) /\ x < sum* k e. NN ( F ` k ) ) -> E. y e. ran seq 1 ( +e , F ) x < y )
142 141 ex 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ x e. RR ) -> ( x < sum* k e. NN ( F ` k ) -> E. y e. ran seq 1 ( +e , F ) x < y ) )
143 142 ralrimiva 
 |-  ( F : NN --> ( 0 [,] +oo ) -> A. x e. RR ( x < sum* k e. NN ( F ` k ) -> E. y e. ran seq 1 ( +e , F ) x < y ) )
144 supxr2 
 |-  ( ( ( ran seq 1 ( +e , F ) C_ RR* /\ sum* k e. NN ( F ` k ) e. RR* ) /\ ( A. x e. ran seq 1 ( +e , F ) x <_ sum* k e. NN ( F ` k ) /\ A. x e. RR ( x < sum* k e. NN ( F ` k ) -> E. y e. ran seq 1 ( +e , F ) x < y ) ) ) -> sup ( ran seq 1 ( +e , F ) , RR* , < ) = sum* k e. NN ( F ` k ) )
145 32 39 60 143 144 syl22anc 
 |-  ( F : NN --> ( 0 [,] +oo ) -> sup ( ran seq 1 ( +e , F ) , RR* , < ) = sum* k e. NN ( F ` k ) )
146 145 eqcomd 
 |-  ( F : NN --> ( 0 [,] +oo ) -> sum* k e. NN ( F ` k ) = sup ( ran seq 1 ( +e , F ) , RR* , < ) )