Step |
Hyp |
Ref |
Expression |
1 |
|
caucvgb.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
eldm2g |
|- ( F e. dom ~~> -> ( F e. dom ~~> <-> E. m <. F , m >. e. ~~> ) ) |
3 |
2
|
ibi |
|- ( F e. dom ~~> -> E. m <. F , m >. e. ~~> ) |
4 |
|
df-br |
|- ( F ~~> m <-> <. F , m >. e. ~~> ) |
5 |
|
simpll |
|- ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> M e. ZZ ) |
6 |
|
1rp |
|- 1 e. RR+ |
7 |
6
|
a1i |
|- ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> 1 e. RR+ ) |
8 |
|
eqidd |
|- ( ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) ) |
9 |
|
simpr |
|- ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> F ~~> m ) |
10 |
1 5 7 8 9
|
climi |
|- ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - m ) ) < 1 ) ) |
11 |
|
simpl |
|- ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - m ) ) < 1 ) -> ( F ` k ) e. CC ) |
12 |
11
|
ralimi |
|- ( A. k e. ( ZZ>= ` n ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - m ) ) < 1 ) -> A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) |
13 |
12
|
reximi |
|- ( E. n e. Z A. k e. ( ZZ>= ` n ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - m ) ) < 1 ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) |
14 |
10 13
|
syl |
|- ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) |
15 |
14
|
ex |
|- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> m -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) |
16 |
4 15
|
syl5bir |
|- ( ( M e. ZZ /\ F e. V ) -> ( <. F , m >. e. ~~> -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) |
17 |
16
|
exlimdv |
|- ( ( M e. ZZ /\ F e. V ) -> ( E. m <. F , m >. e. ~~> -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) |
18 |
3 17
|
syl5 |
|- ( ( M e. ZZ /\ F e. V ) -> ( F e. dom ~~> -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) |
19 |
|
fveq2 |
|- ( j = n -> ( ZZ>= ` j ) = ( ZZ>= ` n ) ) |
20 |
19
|
raleqdv |
|- ( j = n -> ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC <-> A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) |
21 |
20
|
cbvrexvw |
|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC <-> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) |
22 |
21
|
a1i |
|- ( x = 1 -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC <-> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) |
23 |
|
simpl |
|- ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( F ` k ) e. CC ) |
24 |
23
|
ralimi |
|- ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) |
25 |
24
|
reximi |
|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) |
26 |
25
|
ralimi |
|- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) |
27 |
6
|
a1i |
|- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> 1 e. RR+ ) |
28 |
22 26 27
|
rspcdva |
|- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) |
29 |
28
|
a1i |
|- ( ( M e. ZZ /\ F e. V ) -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) |
30 |
|
eluzelz |
|- ( n e. ( ZZ>= ` M ) -> n e. ZZ ) |
31 |
30 1
|
eleq2s |
|- ( n e. Z -> n e. ZZ ) |
32 |
|
eqid |
|- ( ZZ>= ` n ) = ( ZZ>= ` n ) |
33 |
32
|
climcau |
|- ( ( n e. ZZ /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) |
34 |
31 33
|
sylan |
|- ( ( n e. Z /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) |
35 |
32
|
r19.29uz |
|- ( ( A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC /\ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
36 |
35
|
ex |
|- ( A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC -> ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
37 |
36
|
ralimdv |
|- ( A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC -> ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
38 |
34 37
|
mpan9 |
|- ( ( ( n e. Z /\ F e. dom ~~> ) /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
39 |
38
|
an32s |
|- ( ( ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
40 |
39
|
adantll |
|- ( ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
41 |
|
simplrr |
|- ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) |
42 |
|
fveq2 |
|- ( k = m -> ( F ` k ) = ( F ` m ) ) |
43 |
42
|
eleq1d |
|- ( k = m -> ( ( F ` k ) e. CC <-> ( F ` m ) e. CC ) ) |
44 |
43
|
rspccva |
|- ( ( A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) e. CC ) |
45 |
41 44
|
sylan |
|- ( ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) e. CC ) |
46 |
|
simpr |
|- ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) |
47 |
46
|
ralimi |
|- ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) |
48 |
42
|
fvoveq1d |
|- ( k = m -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) = ( abs ` ( ( F ` m ) - ( F ` j ) ) ) ) |
49 |
48
|
breq1d |
|- ( k = m -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x <-> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x ) ) |
50 |
49
|
cbvralvw |
|- ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x <-> A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x ) |
51 |
47 50
|
sylib |
|- ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x ) |
52 |
51
|
reximi |
|- ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x ) |
53 |
52
|
ralimi |
|- ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x ) |
54 |
53
|
adantl |
|- ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x ) |
55 |
|
fveq2 |
|- ( j = i -> ( ZZ>= ` j ) = ( ZZ>= ` i ) ) |
56 |
|
fveq2 |
|- ( j = i -> ( F ` j ) = ( F ` i ) ) |
57 |
56
|
oveq2d |
|- ( j = i -> ( ( F ` m ) - ( F ` j ) ) = ( ( F ` m ) - ( F ` i ) ) ) |
58 |
57
|
fveq2d |
|- ( j = i -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) = ( abs ` ( ( F ` m ) - ( F ` i ) ) ) ) |
59 |
58
|
breq1d |
|- ( j = i -> ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x ) ) |
60 |
55 59
|
raleqbidv |
|- ( j = i -> ( A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x ) ) |
61 |
60
|
cbvrexvw |
|- ( E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x ) |
62 |
|
breq2 |
|- ( x = y -> ( ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x <-> ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y ) ) |
63 |
62
|
rexralbidv |
|- ( x = y -> ( E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x <-> E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y ) ) |
64 |
61 63
|
syl5bb |
|- ( x = y -> ( E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y ) ) |
65 |
64
|
cbvralvw |
|- ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> A. y e. RR+ E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y ) |
66 |
54 65
|
sylib |
|- ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> A. y e. RR+ E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y ) |
67 |
|
simpll |
|- ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> F e. V ) |
68 |
32 45 66 67
|
caucvg |
|- ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> F e. dom ~~> ) |
69 |
68
|
adantlll |
|- ( ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> F e. dom ~~> ) |
70 |
40 69
|
impbida |
|- ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
71 |
1 32
|
cau4 |
|- ( n e. Z -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
72 |
71
|
ad2antrl |
|- ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
73 |
70 72
|
bitr4d |
|- ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
74 |
73
|
rexlimdvaa |
|- ( ( M e. ZZ /\ F e. V ) -> ( E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) ) |
75 |
18 29 74
|
pm5.21ndd |
|- ( ( M e. ZZ /\ F e. V ) -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |