Step |
Hyp |
Ref |
Expression |
1 |
|
climcau.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
simp3 |
|- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> A. k e. Z ( F ` k ) e. CC ) |
3 |
1
|
climcau |
|- ( ( M e. ZZ /\ F e. dom ~~> ) -> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < y ) |
4 |
3
|
3adant3 |
|- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < y ) |
5 |
1
|
caubnd |
|- ( ( A. k e. Z ( F ` k ) e. CC /\ A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < y ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) < x ) |
6 |
2 4 5
|
syl2anc |
|- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) < x ) |
7 |
|
r19.26 |
|- ( A. k e. Z ( ( F ` k ) e. CC /\ ( abs ` ( F ` k ) ) < x ) <-> ( A. k e. Z ( F ` k ) e. CC /\ A. k e. Z ( abs ` ( F ` k ) ) < x ) ) |
8 |
|
simpr |
|- ( ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> ( F ` k ) e. CC ) |
9 |
8
|
abscld |
|- ( ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> ( abs ` ( F ` k ) ) e. RR ) |
10 |
|
simpllr |
|- ( ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> x e. RR ) |
11 |
|
ltle |
|- ( ( ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> ( ( abs ` ( F ` k ) ) < x -> ( abs ` ( F ` k ) ) <_ x ) ) |
12 |
9 10 11
|
syl2anc |
|- ( ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> ( ( abs ` ( F ` k ) ) < x -> ( abs ` ( F ` k ) ) <_ x ) ) |
13 |
12
|
expimpd |
|- ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( F ` k ) ) < x ) -> ( abs ` ( F ` k ) ) <_ x ) ) |
14 |
13
|
ralimdva |
|- ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) -> ( A. k e. Z ( ( F ` k ) e. CC /\ ( abs ` ( F ` k ) ) < x ) -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) |
15 |
7 14
|
syl5bir |
|- ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) -> ( ( A. k e. Z ( F ` k ) e. CC /\ A. k e. Z ( abs ` ( F ` k ) ) < x ) -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) |
16 |
15
|
exp4b |
|- ( ( M e. ZZ /\ F e. dom ~~> ) -> ( x e. RR -> ( A. k e. Z ( F ` k ) e. CC -> ( A. k e. Z ( abs ` ( F ` k ) ) < x -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) ) ) |
17 |
16
|
com23 |
|- ( ( M e. ZZ /\ F e. dom ~~> ) -> ( A. k e. Z ( F ` k ) e. CC -> ( x e. RR -> ( A. k e. Z ( abs ` ( F ` k ) ) < x -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) ) ) |
18 |
17
|
3impia |
|- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> ( x e. RR -> ( A. k e. Z ( abs ` ( F ` k ) ) < x -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) ) |
19 |
18
|
reximdvai |
|- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> ( E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) < x -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) |
20 |
6 19
|
mpd |
|- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x ) |