Step |
Hyp |
Ref |
Expression |
1 |
|
fsumcvg3.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
fsumcvg3.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
fsumcvg3.3 |
|- ( ph -> A e. Fin ) |
4 |
|
fsumcvg3.4 |
|- ( ph -> A C_ Z ) |
5 |
|
fsumcvg3.5 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) ) |
6 |
|
fsumcvg3.6 |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
7 |
|
sseq1 |
|- ( A = (/) -> ( A C_ ( M ... n ) <-> (/) C_ ( M ... n ) ) ) |
8 |
7
|
rexbidv |
|- ( A = (/) -> ( E. n e. ( ZZ>= ` M ) A C_ ( M ... n ) <-> E. n e. ( ZZ>= ` M ) (/) C_ ( M ... n ) ) ) |
9 |
4
|
adantr |
|- ( ( ph /\ A =/= (/) ) -> A C_ Z ) |
10 |
9 1
|
sseqtrdi |
|- ( ( ph /\ A =/= (/) ) -> A C_ ( ZZ>= ` M ) ) |
11 |
|
ltso |
|- < Or RR |
12 |
3
|
adantr |
|- ( ( ph /\ A =/= (/) ) -> A e. Fin ) |
13 |
|
simpr |
|- ( ( ph /\ A =/= (/) ) -> A =/= (/) ) |
14 |
|
uzssz |
|- ( ZZ>= ` M ) C_ ZZ |
15 |
|
zssre |
|- ZZ C_ RR |
16 |
14 15
|
sstri |
|- ( ZZ>= ` M ) C_ RR |
17 |
1 16
|
eqsstri |
|- Z C_ RR |
18 |
9 17
|
sstrdi |
|- ( ( ph /\ A =/= (/) ) -> A C_ RR ) |
19 |
12 13 18
|
3jca |
|- ( ( ph /\ A =/= (/) ) -> ( A e. Fin /\ A =/= (/) /\ A C_ RR ) ) |
20 |
|
fisupcl |
|- ( ( < Or RR /\ ( A e. Fin /\ A =/= (/) /\ A C_ RR ) ) -> sup ( A , RR , < ) e. A ) |
21 |
11 19 20
|
sylancr |
|- ( ( ph /\ A =/= (/) ) -> sup ( A , RR , < ) e. A ) |
22 |
10 21
|
sseldd |
|- ( ( ph /\ A =/= (/) ) -> sup ( A , RR , < ) e. ( ZZ>= ` M ) ) |
23 |
|
fimaxre2 |
|- ( ( A C_ RR /\ A e. Fin ) -> E. k e. RR A. n e. A n <_ k ) |
24 |
18 12 23
|
syl2anc |
|- ( ( ph /\ A =/= (/) ) -> E. k e. RR A. n e. A n <_ k ) |
25 |
18 13 24
|
3jca |
|- ( ( ph /\ A =/= (/) ) -> ( A C_ RR /\ A =/= (/) /\ E. k e. RR A. n e. A n <_ k ) ) |
26 |
|
suprub |
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. k e. RR A. n e. A n <_ k ) /\ k e. A ) -> k <_ sup ( A , RR , < ) ) |
27 |
25 26
|
sylan |
|- ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> k <_ sup ( A , RR , < ) ) |
28 |
10
|
sselda |
|- ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> k e. ( ZZ>= ` M ) ) |
29 |
14 22
|
sselid |
|- ( ( ph /\ A =/= (/) ) -> sup ( A , RR , < ) e. ZZ ) |
30 |
29
|
adantr |
|- ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> sup ( A , RR , < ) e. ZZ ) |
31 |
|
elfz5 |
|- ( ( k e. ( ZZ>= ` M ) /\ sup ( A , RR , < ) e. ZZ ) -> ( k e. ( M ... sup ( A , RR , < ) ) <-> k <_ sup ( A , RR , < ) ) ) |
32 |
28 30 31
|
syl2anc |
|- ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> ( k e. ( M ... sup ( A , RR , < ) ) <-> k <_ sup ( A , RR , < ) ) ) |
33 |
27 32
|
mpbird |
|- ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> k e. ( M ... sup ( A , RR , < ) ) ) |
34 |
33
|
ex |
|- ( ( ph /\ A =/= (/) ) -> ( k e. A -> k e. ( M ... sup ( A , RR , < ) ) ) ) |
35 |
34
|
ssrdv |
|- ( ( ph /\ A =/= (/) ) -> A C_ ( M ... sup ( A , RR , < ) ) ) |
36 |
|
oveq2 |
|- ( n = sup ( A , RR , < ) -> ( M ... n ) = ( M ... sup ( A , RR , < ) ) ) |
37 |
36
|
sseq2d |
|- ( n = sup ( A , RR , < ) -> ( A C_ ( M ... n ) <-> A C_ ( M ... sup ( A , RR , < ) ) ) ) |
38 |
37
|
rspcev |
|- ( ( sup ( A , RR , < ) e. ( ZZ>= ` M ) /\ A C_ ( M ... sup ( A , RR , < ) ) ) -> E. n e. ( ZZ>= ` M ) A C_ ( M ... n ) ) |
39 |
22 35 38
|
syl2anc |
|- ( ( ph /\ A =/= (/) ) -> E. n e. ( ZZ>= ` M ) A C_ ( M ... n ) ) |
40 |
|
uzid |
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) |
41 |
2 40
|
syl |
|- ( ph -> M e. ( ZZ>= ` M ) ) |
42 |
|
0ss |
|- (/) C_ ( M ... M ) |
43 |
|
oveq2 |
|- ( n = M -> ( M ... n ) = ( M ... M ) ) |
44 |
43
|
sseq2d |
|- ( n = M -> ( (/) C_ ( M ... n ) <-> (/) C_ ( M ... M ) ) ) |
45 |
44
|
rspcev |
|- ( ( M e. ( ZZ>= ` M ) /\ (/) C_ ( M ... M ) ) -> E. n e. ( ZZ>= ` M ) (/) C_ ( M ... n ) ) |
46 |
41 42 45
|
sylancl |
|- ( ph -> E. n e. ( ZZ>= ` M ) (/) C_ ( M ... n ) ) |
47 |
8 39 46
|
pm2.61ne |
|- ( ph -> E. n e. ( ZZ>= ` M ) A C_ ( M ... n ) ) |
48 |
1
|
eleq2i |
|- ( k e. Z <-> k e. ( ZZ>= ` M ) ) |
49 |
48 5
|
sylan2br |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) ) |
50 |
49
|
adantlr |
|- ( ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) ) |
51 |
|
simprl |
|- ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) -> n e. ( ZZ>= ` M ) ) |
52 |
6
|
adantlr |
|- ( ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) /\ k e. A ) -> B e. CC ) |
53 |
|
simprr |
|- ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) -> A C_ ( M ... n ) ) |
54 |
50 51 52 53
|
fsumcvg2 |
|- ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` n ) ) |
55 |
|
climrel |
|- Rel ~~> |
56 |
55
|
releldmi |
|- ( seq M ( + , F ) ~~> ( seq M ( + , F ) ` n ) -> seq M ( + , F ) e. dom ~~> ) |
57 |
54 56
|
syl |
|- ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) -> seq M ( + , F ) e. dom ~~> ) |
58 |
47 57
|
rexlimddv |
|- ( ph -> seq M ( + , F ) e. dom ~~> ) |