Step |
Hyp |
Ref |
Expression |
1 |
|
climcau.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
df-br |
|- ( F ~~> y <-> <. F , y >. e. ~~> ) |
3 |
|
simpll |
|- ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> M e. ZZ ) |
4 |
|
rphalfcl |
|- ( x e. RR+ -> ( x / 2 ) e. RR+ ) |
5 |
4
|
adantl |
|- ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> ( x / 2 ) e. RR+ ) |
6 |
|
eqidd |
|- ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) ) |
7 |
|
simplr |
|- ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> F ~~> y ) |
8 |
1 3 5 6 7
|
climi |
|- ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) |
9 |
|
eluzelz |
|- ( j e. ( ZZ>= ` M ) -> j e. ZZ ) |
10 |
|
uzid |
|- ( j e. ZZ -> j e. ( ZZ>= ` j ) ) |
11 |
9 10
|
syl |
|- ( j e. ( ZZ>= ` M ) -> j e. ( ZZ>= ` j ) ) |
12 |
11 1
|
eleq2s |
|- ( j e. Z -> j e. ( ZZ>= ` j ) ) |
13 |
12
|
adantl |
|- ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> j e. ( ZZ>= ` j ) ) |
14 |
|
fveq2 |
|- ( k = j -> ( F ` k ) = ( F ` j ) ) |
15 |
14
|
eleq1d |
|- ( k = j -> ( ( F ` k ) e. CC <-> ( F ` j ) e. CC ) ) |
16 |
14
|
fvoveq1d |
|- ( k = j -> ( abs ` ( ( F ` k ) - y ) ) = ( abs ` ( ( F ` j ) - y ) ) ) |
17 |
16
|
breq1d |
|- ( k = j -> ( ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) <-> ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) |
18 |
15 17
|
anbi12d |
|- ( k = j -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) <-> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) ) |
19 |
18
|
rspcv |
|- ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) ) |
20 |
13 19
|
syl |
|- ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) ) |
21 |
|
rpre |
|- ( x e. RR+ -> x e. RR ) |
22 |
21
|
ad2antlr |
|- ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> x e. RR ) |
23 |
|
simpllr |
|- ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> F ~~> y ) |
24 |
|
climcl |
|- ( F ~~> y -> y e. CC ) |
25 |
23 24
|
syl |
|- ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> y e. CC ) |
26 |
|
simprl |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( F ` k ) e. CC ) |
27 |
|
simplrl |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( F ` j ) e. CC ) |
28 |
|
simpllr |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> y e. CC ) |
29 |
|
simplll |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> x e. RR ) |
30 |
|
simprr |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) |
31 |
28 27
|
abssubd |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( y - ( F ` j ) ) ) = ( abs ` ( ( F ` j ) - y ) ) ) |
32 |
|
simplrr |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) |
33 |
31 32
|
eqbrtrd |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( y - ( F ` j ) ) ) < ( x / 2 ) ) |
34 |
26 27 28 29 30 33
|
abs3lemd |
|- ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) |
35 |
34
|
ex |
|- ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
36 |
35
|
ralimdv |
|- ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
37 |
36
|
ex |
|- ( ( x e. RR /\ y e. CC ) -> ( ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
38 |
37
|
com23 |
|- ( ( x e. RR /\ y e. CC ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
39 |
22 25 38
|
syl2anc |
|- ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) |
40 |
20 39
|
mpdd |
|- ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
41 |
40
|
reximdva |
|- ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
42 |
8 41
|
mpd |
|- ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) |
43 |
42
|
ralrimiva |
|- ( ( M e. ZZ /\ F ~~> y ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) |
44 |
43
|
ex |
|- ( M e. ZZ -> ( F ~~> y -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
45 |
2 44
|
syl5bir |
|- ( M e. ZZ -> ( <. F , y >. e. ~~> -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
46 |
45
|
exlimdv |
|- ( M e. ZZ -> ( E. y <. F , y >. e. ~~> -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) |
47 |
|
eldm2g |
|- ( F e. dom ~~> -> ( F e. dom ~~> <-> E. y <. F , y >. e. ~~> ) ) |
48 |
47
|
ibi |
|- ( F e. dom ~~> -> E. y <. F , y >. e. ~~> ) |
49 |
46 48
|
impel |
|- ( ( M e. ZZ /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) |