Step |
Hyp |
Ref |
Expression |
1 |
|
clim2ser.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
climserle.2 |
|- ( ph -> N e. Z ) |
3 |
|
climserle.3 |
|- ( ph -> seq M ( + , F ) ~~> A ) |
4 |
|
climserle.4 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR ) |
5 |
|
climserle.5 |
|- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) ) |
6 |
2 1
|
eleqtrdi |
|- ( ph -> N e. ( ZZ>= ` M ) ) |
7 |
|
eluzel2 |
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) |
8 |
6 7
|
syl |
|- ( ph -> M e. ZZ ) |
9 |
1 8 4
|
serfre |
|- ( ph -> seq M ( + , F ) : Z --> RR ) |
10 |
9
|
ffvelrnda |
|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. RR ) |
11 |
1
|
peano2uzs |
|- ( j e. Z -> ( j + 1 ) e. Z ) |
12 |
|
fveq2 |
|- ( k = ( j + 1 ) -> ( F ` k ) = ( F ` ( j + 1 ) ) ) |
13 |
12
|
breq2d |
|- ( k = ( j + 1 ) -> ( 0 <_ ( F ` k ) <-> 0 <_ ( F ` ( j + 1 ) ) ) ) |
14 |
13
|
imbi2d |
|- ( k = ( j + 1 ) -> ( ( ph -> 0 <_ ( F ` k ) ) <-> ( ph -> 0 <_ ( F ` ( j + 1 ) ) ) ) ) |
15 |
5
|
expcom |
|- ( k e. Z -> ( ph -> 0 <_ ( F ` k ) ) ) |
16 |
14 15
|
vtoclga |
|- ( ( j + 1 ) e. Z -> ( ph -> 0 <_ ( F ` ( j + 1 ) ) ) ) |
17 |
16
|
impcom |
|- ( ( ph /\ ( j + 1 ) e. Z ) -> 0 <_ ( F ` ( j + 1 ) ) ) |
18 |
11 17
|
sylan2 |
|- ( ( ph /\ j e. Z ) -> 0 <_ ( F ` ( j + 1 ) ) ) |
19 |
12
|
eleq1d |
|- ( k = ( j + 1 ) -> ( ( F ` k ) e. RR <-> ( F ` ( j + 1 ) ) e. RR ) ) |
20 |
19
|
imbi2d |
|- ( k = ( j + 1 ) -> ( ( ph -> ( F ` k ) e. RR ) <-> ( ph -> ( F ` ( j + 1 ) ) e. RR ) ) ) |
21 |
4
|
expcom |
|- ( k e. Z -> ( ph -> ( F ` k ) e. RR ) ) |
22 |
20 21
|
vtoclga |
|- ( ( j + 1 ) e. Z -> ( ph -> ( F ` ( j + 1 ) ) e. RR ) ) |
23 |
22
|
impcom |
|- ( ( ph /\ ( j + 1 ) e. Z ) -> ( F ` ( j + 1 ) ) e. RR ) |
24 |
11 23
|
sylan2 |
|- ( ( ph /\ j e. Z ) -> ( F ` ( j + 1 ) ) e. RR ) |
25 |
10 24
|
addge01d |
|- ( ( ph /\ j e. Z ) -> ( 0 <_ ( F ` ( j + 1 ) ) <-> ( seq M ( + , F ) ` j ) <_ ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) ) ) |
26 |
18 25
|
mpbid |
|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) <_ ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) ) |
27 |
|
simpr |
|- ( ( ph /\ j e. Z ) -> j e. Z ) |
28 |
27 1
|
eleqtrdi |
|- ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) ) |
29 |
|
seqp1 |
|- ( j e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( j + 1 ) ) = ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) ) |
30 |
28 29
|
syl |
|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` ( j + 1 ) ) = ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) ) |
31 |
26 30
|
breqtrrd |
|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) <_ ( seq M ( + , F ) ` ( j + 1 ) ) ) |
32 |
1 2 3 10 31
|
climub |
|- ( ph -> ( seq M ( + , F ) ` N ) <_ A ) |