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 )