This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caubnd2

Description: A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014)

Ref Expression
Hypothesis cau3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion caubnd2 ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 )

Proof

Step Hyp Ref Expression
1 cau3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 1rp ⊢ 1 ∈ ℝ+
3 breq2 ⊢ ( 𝑥 = 1 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) )
4 3 anbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) )
5 4 rexralbidv ⊢ ( 𝑥 = 1 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) )
6 5 rspcv ⊢ ( 1 ∈ ℝ+ → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) )
7 2 6 ax-mp ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) )
8 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
9 8 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
10 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
11 9 10 syl ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
12 simpl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
13 12 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
14 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
15 14 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) )
16 15 rspcva ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
17 11 13 16 syl2an ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
18 abscl ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
19 17 18 syl ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
20 1re ⊢ 1 ∈ ℝ
21 readdcl ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ∈ ℝ )
22 19 20 21 sylancl ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ∈ ℝ )
23 simpr ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
24 simplr ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
25 abs2dif ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
26 23 24 25 syl2anc ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
27 abscl ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
28 23 27 syl ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
29 24 18 syl ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
30 28 29 resubcld ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
31 23 24 subcld ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ )
32 abscl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
33 31 32 syl ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
34 lelttr ⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) )
35 20 34 mp3an3 ⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) → ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) )
36 30 33 35 syl2anc ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) )
37 26 36 mpand ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) )
38 ltsubadd2 ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) < 1 ↔ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ) )
39 20 38 mp3an3 ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) < 1 ↔ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ) )
40 28 29 39 syl2anc ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ) < 1 ↔ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ) )
41 37 40 sylibd ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ) )
42 41 expimpd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ) )
43 42 ralimdv ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ) )
44 43 impancom ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ) )
45 17 44 mpd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) )
46 brralrspcev ⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ∈ ℝ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) + 1 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 )
47 22 45 46 syl2anc ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 )
48 47 ex ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 ) )
49 48 reximia ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ∃ 𝑗 ∈ 𝑍 ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 )
50 rexcom ⊢ ( ∃ 𝑗 ∈ 𝑍 ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 )
51 49 50 sylib ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 1 ) → ∃ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 )
52 7 51 syl ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 )