Step |
Hyp |
Ref |
Expression |
1 |
|
caucvgb.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
eldm2g |
⊢ ( 𝐹 ∈ dom ⇝ → ( 𝐹 ∈ dom ⇝ ↔ ∃ 𝑚 〈 𝐹 , 𝑚 〉 ∈ ⇝ ) ) |
3 |
2
|
ibi |
⊢ ( 𝐹 ∈ dom ⇝ → ∃ 𝑚 〈 𝐹 , 𝑚 〉 ∈ ⇝ ) |
4 |
|
df-br |
⊢ ( 𝐹 ⇝ 𝑚 ↔ 〈 𝐹 , 𝑚 〉 ∈ ⇝ ) |
5 |
|
simpll |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝐹 ⇝ 𝑚 ) → 𝑀 ∈ ℤ ) |
6 |
|
1rp |
⊢ 1 ∈ ℝ+ |
7 |
6
|
a1i |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝐹 ⇝ 𝑚 ) → 1 ∈ ℝ+ ) |
8 |
|
eqidd |
⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝐹 ⇝ 𝑚 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
9 |
|
simpr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝐹 ⇝ 𝑚 ) → 𝐹 ⇝ 𝑚 ) |
10 |
1 5 7 8 9
|
climi |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝐹 ⇝ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑚 ) ) < 1 ) ) |
11 |
|
simpl |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑚 ) ) < 1 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
12 |
11
|
ralimi |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑚 ) ) < 1 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
13 |
12
|
reximi |
⊢ ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑚 ) ) < 1 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
14 |
10 13
|
syl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝐹 ⇝ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
15 |
14
|
ex |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ 𝑚 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
16 |
4 15
|
syl5bir |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 〈 𝐹 , 𝑚 〉 ∈ ⇝ → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
17 |
16
|
exlimdv |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ∃ 𝑚 〈 𝐹 , 𝑚 〉 ∈ ⇝ → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
18 |
3 17
|
syl5 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
19 |
|
fveq2 |
⊢ ( 𝑗 = 𝑛 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑛 ) ) |
20 |
19
|
raleqdv |
⊢ ( 𝑗 = 𝑛 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
21 |
20
|
cbvrexvw |
⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
22 |
21
|
a1i |
⊢ ( 𝑥 = 1 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
23 |
|
simpl |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
24 |
23
|
ralimi |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
25 |
24
|
reximi |
⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
26 |
25
|
ralimi |
⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
27 |
6
|
a1i |
⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → 1 ∈ ℝ+ ) |
28 |
22 26 27
|
rspcdva |
⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
29 |
28
|
a1i |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
30 |
|
eluzelz |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑛 ∈ ℤ ) |
31 |
30 1
|
eleq2s |
⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ ) |
32 |
|
eqid |
⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 ) |
33 |
32
|
climcau |
⊢ ( ( 𝑛 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
34 |
31 33
|
sylan |
⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
35 |
32
|
r19.29uz |
⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) |
36 |
35
|
ex |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ) |
37 |
36
|
ralimdv |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ) |
38 |
34 37
|
mpan9 |
⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ 𝐹 ∈ dom ⇝ ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) |
39 |
38
|
an32s |
⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) |
40 |
39
|
adantll |
⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) |
41 |
|
simplrr |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
42 |
|
fveq2 |
⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) ) |
43 |
42
|
eleq1d |
⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑚 ) ∈ ℂ ) ) |
44 |
43
|
rspccva |
⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ ) |
45 |
41 44
|
sylan |
⊢ ( ( ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ ) |
46 |
|
simpr |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
47 |
46
|
ralimi |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
48 |
42
|
fvoveq1d |
⊢ ( 𝑘 = 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ) |
49 |
48
|
breq1d |
⊢ ( 𝑘 = 𝑚 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) |
50 |
49
|
cbvralvw |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
51 |
47 50
|
sylib |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
52 |
51
|
reximi |
⊢ ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
53 |
52
|
ralimi |
⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
54 |
53
|
adantl |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) |
55 |
|
fveq2 |
⊢ ( 𝑗 = 𝑖 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑖 ) ) |
56 |
|
fveq2 |
⊢ ( 𝑗 = 𝑖 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑖 ) ) |
57 |
56
|
oveq2d |
⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) |
58 |
57
|
fveq2d |
⊢ ( 𝑗 = 𝑖 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) ) |
59 |
58
|
breq1d |
⊢ ( 𝑗 = 𝑖 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ) |
60 |
55 59
|
raleqbidv |
⊢ ( 𝑗 = 𝑖 → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ) |
61 |
60
|
cbvrexvw |
⊢ ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ∃ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) |
62 |
|
breq2 |
⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑦 ) ) |
63 |
62
|
rexralbidv |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ↔ ∃ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑦 ) ) |
64 |
61 63
|
syl5bb |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ∃ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑦 ) ) |
65 |
64
|
cbvralvw |
⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑦 ) |
66 |
54 65
|
sylib |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑦 ) |
67 |
|
simpll |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) → 𝐹 ∈ 𝑉 ) |
68 |
32 45 66 67
|
caucvg |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) → 𝐹 ∈ dom ⇝ ) |
69 |
68
|
adantlll |
⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) → 𝐹 ∈ dom ⇝ ) |
70 |
40 69
|
impbida |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ) |
71 |
1 32
|
cau4 |
⊢ ( 𝑛 ∈ 𝑍 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ) |
72 |
71
|
ad2antrl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ) |
73 |
70 72
|
bitr4d |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ) |
74 |
73
|
rexlimdvaa |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ) ) |
75 |
18 29 74
|
pm5.21ndd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) ) |