Metamath Proof Explorer


Theorem caubnd

Description: A Cauchy sequence of complex numbers is bounded. (Contributed by NM, 4-Apr-2005) (Revised by Mario Carneiro, 14-Feb-2014)

Ref Expression
Hypothesis cau3.1
|- Z = ( ZZ>= ` M )
Assertion caubnd
|- ( ( A. k e. Z ( F ` k ) e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y )

Proof

Step Hyp Ref Expression
1 cau3.1
 |-  Z = ( ZZ>= ` M )
2 abscl
 |-  ( ( F ` k ) e. CC -> ( abs ` ( F ` k ) ) e. RR )
3 2 ralimi
 |-  ( A. k e. Z ( F ` k ) e. CC -> A. k e. Z ( abs ` ( F ` k ) ) e. RR )
4 1 r19.29uz
 |-  ( ( A. k e. Z ( F ` k ) e. CC /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
5 4 ex
 |-  ( A. k e. Z ( F ` k ) e. CC -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
6 5 ralimdv
 |-  ( A. k e. Z ( F ` k ) e. CC -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
7 1 caubnd2
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. z e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z )
8 6 7 syl6
 |-  ( A. k e. Z ( F ` k ) e. CC -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> E. z e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z ) )
9 fzssuz
 |-  ( M ... j ) C_ ( ZZ>= ` M )
10 9 1 sseqtrri
 |-  ( M ... j ) C_ Z
11 ssralv
 |-  ( ( M ... j ) C_ Z -> ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR ) )
12 10 11 ax-mp
 |-  ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR )
13 fzfi
 |-  ( M ... j ) e. Fin
14 fimaxre3
 |-  ( ( ( M ... j ) e. Fin /\ A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR ) -> E. x e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) <_ x )
15 13 14 mpan
 |-  ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR -> E. x e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) <_ x )
16 peano2re
 |-  ( x e. RR -> ( x + 1 ) e. RR )
17 16 adantl
 |-  ( ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> ( x + 1 ) e. RR )
18 ltp1
 |-  ( x e. RR -> x < ( x + 1 ) )
19 18 adantl
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> x < ( x + 1 ) )
20 16 adantl
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> ( x + 1 ) e. RR )
21 lelttr
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ x e. RR /\ ( x + 1 ) e. RR ) -> ( ( ( abs ` ( F ` k ) ) <_ x /\ x < ( x + 1 ) ) -> ( abs ` ( F ` k ) ) < ( x + 1 ) ) )
22 20 21 mpd3an3
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> ( ( ( abs ` ( F ` k ) ) <_ x /\ x < ( x + 1 ) ) -> ( abs ` ( F ` k ) ) < ( x + 1 ) ) )
23 19 22 mpan2d
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> ( ( abs ` ( F ` k ) ) <_ x -> ( abs ` ( F ` k ) ) < ( x + 1 ) ) )
24 23 expcom
 |-  ( x e. RR -> ( ( abs ` ( F ` k ) ) e. RR -> ( ( abs ` ( F ` k ) ) <_ x -> ( abs ` ( F ` k ) ) < ( x + 1 ) ) ) )
25 24 ralimdv
 |-  ( x e. RR -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR -> A. k e. ( M ... j ) ( ( abs ` ( F ` k ) ) <_ x -> ( abs ` ( F ` k ) ) < ( x + 1 ) ) ) )
26 25 impcom
 |-  ( ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> A. k e. ( M ... j ) ( ( abs ` ( F ` k ) ) <_ x -> ( abs ` ( F ` k ) ) < ( x + 1 ) ) )
27 ralim
 |-  ( A. k e. ( M ... j ) ( ( abs ` ( F ` k ) ) <_ x -> ( abs ` ( F ` k ) ) < ( x + 1 ) ) -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) <_ x -> A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < ( x + 1 ) ) )
28 26 27 syl
 |-  ( ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) <_ x -> A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < ( x + 1 ) ) )
29 brralrspcev
 |-  ( ( ( x + 1 ) e. RR /\ A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < ( x + 1 ) ) -> E. w e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w )
30 17 28 29 syl6an
 |-  ( ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) <_ x -> E. w e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w ) )
31 30 rexlimdva
 |-  ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR -> ( E. x e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) <_ x -> E. w e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w ) )
32 15 31 mpd
 |-  ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) e. RR -> E. w e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w )
33 12 32 syl
 |-  ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> E. w e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w )
34 max1
 |-  ( ( w e. RR /\ z e. RR ) -> w <_ if ( w <_ z , z , w ) )
35 34 3adant3
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> w <_ if ( w <_ z , z , w ) )
36 simp3
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> ( abs ` ( F ` k ) ) e. RR )
37 simp1
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> w e. RR )
38 ifcl
 |-  ( ( z e. RR /\ w e. RR ) -> if ( w <_ z , z , w ) e. RR )
39 38 ancoms
 |-  ( ( w e. RR /\ z e. RR ) -> if ( w <_ z , z , w ) e. RR )
40 39 3adant3
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> if ( w <_ z , z , w ) e. RR )
41 ltletr
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ w e. RR /\ if ( w <_ z , z , w ) e. RR ) -> ( ( ( abs ` ( F ` k ) ) < w /\ w <_ if ( w <_ z , z , w ) ) -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) )
42 36 37 40 41 syl3anc
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> ( ( ( abs ` ( F ` k ) ) < w /\ w <_ if ( w <_ z , z , w ) ) -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) )
43 35 42 mpan2d
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> ( ( abs ` ( F ` k ) ) < w -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) )
44 max2
 |-  ( ( w e. RR /\ z e. RR ) -> z <_ if ( w <_ z , z , w ) )
45 44 3adant3
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> z <_ if ( w <_ z , z , w ) )
46 simp2
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> z e. RR )
47 ltletr
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ z e. RR /\ if ( w <_ z , z , w ) e. RR ) -> ( ( ( abs ` ( F ` k ) ) < z /\ z <_ if ( w <_ z , z , w ) ) -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) )
48 36 46 40 47 syl3anc
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> ( ( ( abs ` ( F ` k ) ) < z /\ z <_ if ( w <_ z , z , w ) ) -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) )
49 45 48 mpan2d
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> ( ( abs ` ( F ` k ) ) < z -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) )
50 43 49 jaod
 |-  ( ( w e. RR /\ z e. RR /\ ( abs ` ( F ` k ) ) e. RR ) -> ( ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) )
51 50 3expia
 |-  ( ( w e. RR /\ z e. RR ) -> ( ( abs ` ( F ` k ) ) e. RR -> ( ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) ) )
52 51 ralimdv
 |-  ( ( w e. RR /\ z e. RR ) -> ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> A. k e. Z ( ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) ) )
53 ralim
 |-  ( A. k e. Z ( ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) -> ( A. k e. Z ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> A. k e. Z ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) )
54 52 53 syl6
 |-  ( ( w e. RR /\ z e. RR ) -> ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( A. k e. Z ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> A. k e. Z ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) ) )
55 brralrspcev
 |-  ( ( if ( w <_ z , z , w ) e. RR /\ A. k e. Z ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y )
56 55 ex
 |-  ( if ( w <_ z , z , w ) e. RR -> ( A. k e. Z ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) )
57 39 56 syl
 |-  ( ( w e. RR /\ z e. RR ) -> ( A. k e. Z ( abs ` ( F ` k ) ) < if ( w <_ z , z , w ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) )
58 54 57 syl6d
 |-  ( ( w e. RR /\ z e. RR ) -> ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( A. k e. Z ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) )
59 uzssz
 |-  ( ZZ>= ` M ) C_ ZZ
60 1 59 eqsstri
 |-  Z C_ ZZ
61 60 sseli
 |-  ( k e. Z -> k e. ZZ )
62 60 sseli
 |-  ( j e. Z -> j e. ZZ )
63 uztric
 |-  ( ( k e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` j ) ) )
64 61 62 63 syl2anr
 |-  ( ( j e. Z /\ k e. Z ) -> ( j e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` j ) ) )
65 simpr
 |-  ( ( j e. Z /\ k e. Z ) -> k e. Z )
66 65 1 eleqtrdi
 |-  ( ( j e. Z /\ k e. Z ) -> k e. ( ZZ>= ` M ) )
67 elfzuzb
 |-  ( k e. ( M ... j ) <-> ( k e. ( ZZ>= ` M ) /\ j e. ( ZZ>= ` k ) ) )
68 67 baib
 |-  ( k e. ( ZZ>= ` M ) -> ( k e. ( M ... j ) <-> j e. ( ZZ>= ` k ) ) )
69 66 68 syl
 |-  ( ( j e. Z /\ k e. Z ) -> ( k e. ( M ... j ) <-> j e. ( ZZ>= ` k ) ) )
70 69 orbi1d
 |-  ( ( j e. Z /\ k e. Z ) -> ( ( k e. ( M ... j ) \/ k e. ( ZZ>= ` j ) ) <-> ( j e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` j ) ) ) )
71 64 70 mpbird
 |-  ( ( j e. Z /\ k e. Z ) -> ( k e. ( M ... j ) \/ k e. ( ZZ>= ` j ) ) )
72 71 ex
 |-  ( j e. Z -> ( k e. Z -> ( k e. ( M ... j ) \/ k e. ( ZZ>= ` j ) ) ) )
73 pm3.48
 |-  ( ( ( k e. ( M ... j ) -> ( abs ` ( F ` k ) ) < w ) /\ ( k e. ( ZZ>= ` j ) -> ( abs ` ( F ` k ) ) < z ) ) -> ( ( k e. ( M ... j ) \/ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) ) )
74 72 73 syl9
 |-  ( j e. Z -> ( ( ( k e. ( M ... j ) -> ( abs ` ( F ` k ) ) < w ) /\ ( k e. ( ZZ>= ` j ) -> ( abs ` ( F ` k ) ) < z ) ) -> ( k e. Z -> ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) ) ) )
75 74 alimdv
 |-  ( j e. Z -> ( A. k ( ( k e. ( M ... j ) -> ( abs ` ( F ` k ) ) < w ) /\ ( k e. ( ZZ>= ` j ) -> ( abs ` ( F ` k ) ) < z ) ) -> A. k ( k e. Z -> ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) ) ) )
76 df-ral
 |-  ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w <-> A. k ( k e. ( M ... j ) -> ( abs ` ( F ` k ) ) < w ) )
77 df-ral
 |-  ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z <-> A. k ( k e. ( ZZ>= ` j ) -> ( abs ` ( F ` k ) ) < z ) )
78 76 77 anbi12i
 |-  ( ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z ) <-> ( A. k ( k e. ( M ... j ) -> ( abs ` ( F ` k ) ) < w ) /\ A. k ( k e. ( ZZ>= ` j ) -> ( abs ` ( F ` k ) ) < z ) ) )
79 19.26
 |-  ( A. k ( ( k e. ( M ... j ) -> ( abs ` ( F ` k ) ) < w ) /\ ( k e. ( ZZ>= ` j ) -> ( abs ` ( F ` k ) ) < z ) ) <-> ( A. k ( k e. ( M ... j ) -> ( abs ` ( F ` k ) ) < w ) /\ A. k ( k e. ( ZZ>= ` j ) -> ( abs ` ( F ` k ) ) < z ) ) )
80 78 79 bitr4i
 |-  ( ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z ) <-> A. k ( ( k e. ( M ... j ) -> ( abs ` ( F ` k ) ) < w ) /\ ( k e. ( ZZ>= ` j ) -> ( abs ` ( F ` k ) ) < z ) ) )
81 df-ral
 |-  ( A. k e. Z ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) <-> A. k ( k e. Z -> ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) ) )
82 75 80 81 3imtr4g
 |-  ( j e. Z -> ( ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z ) -> A. k e. Z ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) ) )
83 82 3impib
 |-  ( ( j e. Z /\ A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z ) -> A. k e. Z ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) )
84 83 imim1i
 |-  ( ( A. k e. Z ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) -> ( ( j e. Z /\ A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) )
85 84 3expd
 |-  ( ( A. k e. Z ( ( abs ` ( F ` k ) ) < w \/ ( abs ` ( F ` k ) ) < z ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) -> ( j e. Z -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) ) )
86 58 85 syl6
 |-  ( ( w e. RR /\ z e. RR ) -> ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( j e. Z -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) ) ) )
87 86 com23
 |-  ( ( w e. RR /\ z e. RR ) -> ( j e. Z -> ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) ) ) )
88 87 expimpd
 |-  ( w e. RR -> ( ( z e. RR /\ j e. Z ) -> ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) ) ) )
89 88 com3r
 |-  ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( w e. RR -> ( ( z e. RR /\ j e. Z ) -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) ) ) )
90 89 com34
 |-  ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( w e. RR -> ( A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w -> ( ( z e. RR /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) ) ) )
91 90 rexlimdv
 |-  ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( E. w e. RR A. k e. ( M ... j ) ( abs ` ( F ` k ) ) < w -> ( ( z e. RR /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) ) )
92 33 91 mpd
 |-  ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( ( z e. RR /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) ) )
93 92 rexlimdvv
 |-  ( A. k e. Z ( abs ` ( F ` k ) ) e. RR -> ( E. z e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < z -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) )
94 3 8 93 sylsyld
 |-  ( A. k e. Z ( F ` k ) e. CC -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y ) )
95 94 imp
 |-  ( ( A. k e. Z ( F ` k ) e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y )