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