Step |
Hyp |
Ref |
Expression |
1 |
|
isumrpcl.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
isumrpcl.2 |
|- W = ( ZZ>= ` N ) |
3 |
|
isumrpcl.3 |
|- ( ph -> N e. Z ) |
4 |
|
isumrpcl.4 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A ) |
5 |
|
isumrpcl.5 |
|- ( ( ph /\ k e. Z ) -> A e. RR+ ) |
6 |
|
isumrpcl.6 |
|- ( ph -> seq M ( + , F ) e. dom ~~> ) |
7 |
3 1
|
eleqtrdi |
|- ( ph -> N e. ( ZZ>= ` M ) ) |
8 |
|
eluzelz |
|- ( N e. ( ZZ>= ` M ) -> N e. ZZ ) |
9 |
7 8
|
syl |
|- ( ph -> N e. ZZ ) |
10 |
|
uzss |
|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) ) |
11 |
7 10
|
syl |
|- ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) ) |
12 |
11 2 1
|
3sstr4g |
|- ( ph -> W C_ Z ) |
13 |
12
|
sselda |
|- ( ( ph /\ k e. W ) -> k e. Z ) |
14 |
13 4
|
syldan |
|- ( ( ph /\ k e. W ) -> ( F ` k ) = A ) |
15 |
5
|
rpred |
|- ( ( ph /\ k e. Z ) -> A e. RR ) |
16 |
13 15
|
syldan |
|- ( ( ph /\ k e. W ) -> A e. RR ) |
17 |
4 5
|
eqeltrd |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR+ ) |
18 |
17
|
rpcnd |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
19 |
1 3 18
|
iserex |
|- ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) ) |
20 |
6 19
|
mpbid |
|- ( ph -> seq N ( + , F ) e. dom ~~> ) |
21 |
2 9 14 16 20
|
isumrecl |
|- ( ph -> sum_ k e. W A e. RR ) |
22 |
|
fveq2 |
|- ( k = N -> ( F ` k ) = ( F ` N ) ) |
23 |
22
|
eleq1d |
|- ( k = N -> ( ( F ` k ) e. RR+ <-> ( F ` N ) e. RR+ ) ) |
24 |
17
|
ralrimiva |
|- ( ph -> A. k e. Z ( F ` k ) e. RR+ ) |
25 |
23 24 3
|
rspcdva |
|- ( ph -> ( F ` N ) e. RR+ ) |
26 |
|
seq1 |
|- ( N e. ZZ -> ( seq N ( + , F ) ` N ) = ( F ` N ) ) |
27 |
9 26
|
syl |
|- ( ph -> ( seq N ( + , F ) ` N ) = ( F ` N ) ) |
28 |
|
uzid |
|- ( N e. ZZ -> N e. ( ZZ>= ` N ) ) |
29 |
9 28
|
syl |
|- ( ph -> N e. ( ZZ>= ` N ) ) |
30 |
29 2
|
eleqtrrdi |
|- ( ph -> N e. W ) |
31 |
16
|
recnd |
|- ( ( ph /\ k e. W ) -> A e. CC ) |
32 |
2 9 14 31 20
|
isumclim2 |
|- ( ph -> seq N ( + , F ) ~~> sum_ k e. W A ) |
33 |
12
|
sseld |
|- ( ph -> ( m e. W -> m e. Z ) ) |
34 |
|
fveq2 |
|- ( k = m -> ( F ` k ) = ( F ` m ) ) |
35 |
34
|
eleq1d |
|- ( k = m -> ( ( F ` k ) e. RR+ <-> ( F ` m ) e. RR+ ) ) |
36 |
35
|
rspcv |
|- ( m e. Z -> ( A. k e. Z ( F ` k ) e. RR+ -> ( F ` m ) e. RR+ ) ) |
37 |
33 24 36
|
syl6ci |
|- ( ph -> ( m e. W -> ( F ` m ) e. RR+ ) ) |
38 |
37
|
imp |
|- ( ( ph /\ m e. W ) -> ( F ` m ) e. RR+ ) |
39 |
38
|
rpred |
|- ( ( ph /\ m e. W ) -> ( F ` m ) e. RR ) |
40 |
38
|
rpge0d |
|- ( ( ph /\ m e. W ) -> 0 <_ ( F ` m ) ) |
41 |
2 30 32 39 40
|
climserle |
|- ( ph -> ( seq N ( + , F ) ` N ) <_ sum_ k e. W A ) |
42 |
27 41
|
eqbrtrrd |
|- ( ph -> ( F ` N ) <_ sum_ k e. W A ) |
43 |
21 25 42
|
rpgecld |
|- ( ph -> sum_ k e. W A e. RR+ ) |