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 sselid
 |-  ( ( 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 sselid
 |-  ( 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 sselid
 |-  ( ( ( ( ( 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 sselid
 |-  ( ( ( ( ( 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 sselid
 |-  ( ( ( ( ( ( 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 sselid
 |-  ( ( ( ( ( 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* , < ) )