Step |
Hyp |
Ref |
Expression |
1 |
|
caucvg.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
caurcvg2.2 |
⊢ ( 𝜑 → 𝐹 ∈ 𝑉 ) |
3 |
|
caurcvg2.3 |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) |
4 |
|
1rp |
⊢ 1 ∈ ℝ+ |
5 |
4
|
ne0ii |
⊢ ℝ+ ≠ ∅ |
6 |
|
r19.2z |
⊢ ( ( ℝ+ ≠ ∅ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) → ∃ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) |
7 |
5 3 6
|
sylancr |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) |
8 |
|
simpl |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) |
9 |
8
|
ralimi |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) |
10 |
|
eqid |
⊢ ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑗 ) |
11 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) |
12 |
|
fveq2 |
⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) ) |
13 |
12
|
eleq1d |
⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) ) |
14 |
13
|
rspccva |
⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) |
15 |
11 14
|
sylan |
⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) |
16 |
15
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |
17 |
|
fveq2 |
⊢ ( 𝑗 = 𝑚 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑚 ) ) |
18 |
|
fveq2 |
⊢ ( 𝑗 = 𝑚 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑚 ) ) |
19 |
18
|
oveq2d |
⊢ ( 𝑗 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) |
20 |
19
|
fveq2d |
⊢ ( 𝑗 = 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) ) |
21 |
20
|
breq1d |
⊢ ( 𝑗 = 𝑚 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
22 |
21
|
anbi2d |
⊢ ( 𝑗 = 𝑚 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) ) |
23 |
17 22
|
raleqbidv |
⊢ ( 𝑗 = 𝑚 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) ) |
24 |
23
|
cbvrexvw |
⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
25 |
|
fveq2 |
⊢ ( 𝑘 = 𝑖 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑖 ) ) |
26 |
25
|
eleq1d |
⊢ ( 𝑘 = 𝑖 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑖 ) ∈ ℝ ) ) |
27 |
25
|
fvoveq1d |
⊢ ( 𝑘 = 𝑖 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) ) |
28 |
27
|
breq1d |
⊢ ( 𝑘 = 𝑖 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
29 |
26 28
|
anbi12d |
⊢ ( 𝑘 = 𝑖 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) ) |
30 |
29
|
cbvralvw |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
31 |
|
recn |
⊢ ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ → ( 𝐹 ‘ 𝑖 ) ∈ ℂ ) |
32 |
31
|
anim1i |
⊢ ( ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
33 |
32
|
ralimi |
⊢ ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
34 |
30 33
|
sylbi |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
35 |
34
|
reximi |
⊢ ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
36 |
24 35
|
sylbi |
⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
37 |
36
|
ralimi |
⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
38 |
3 37
|
syl |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
39 |
38
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
40 |
1 10
|
cau4 |
⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) ) |
41 |
40
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) ) |
42 |
39 41
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
43 |
|
simpr |
⊢ ( ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) |
44 |
10
|
uztrn2 |
⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) |
45 |
|
fveq2 |
⊢ ( 𝑛 = 𝑖 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑖 ) ) |
46 |
|
eqid |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) |
47 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑖 ) ∈ V |
48 |
45 46 47
|
fvmpt |
⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) ) |
49 |
44 48
|
syl |
⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) ) |
50 |
|
fveq2 |
⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) ) |
51 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑚 ) ∈ V |
52 |
50 46 51
|
fvmpt |
⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) ) |
53 |
52
|
adantr |
⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) ) |
54 |
49 53
|
oveq12d |
⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) |
55 |
54
|
fveq2d |
⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) ) |
56 |
55
|
breq1d |
⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) |
57 |
43 56
|
syl5ibr |
⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ) ) |
58 |
57
|
ralimdva |
⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ) ) |
59 |
58
|
reximia |
⊢ ( ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ) |
60 |
59
|
ralimi |
⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ) |
61 |
42 60
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ) |
62 |
10 16 61
|
caurcvg |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ) ) |
63 |
|
eluzelz |
⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ ) |
64 |
63 1
|
eleq2s |
⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ ) |
65 |
64
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → 𝑗 ∈ ℤ ) |
66 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → 𝐹 ∈ 𝑉 ) |
67 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) |
68 |
67
|
cbvmptv |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑘 ) ) |
69 |
10 68
|
climmpt |
⊢ ( ( 𝑗 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
70 |
65 66 69
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → ( 𝐹 ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
71 |
62 70
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → 𝐹 ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ) ) |
72 |
|
climrel |
⊢ Rel ⇝ |
73 |
72
|
releldmi |
⊢ ( 𝐹 ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ↦ ( 𝐹 ‘ 𝑛 ) ) ) → 𝐹 ∈ dom ⇝ ) |
74 |
71 73
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) → 𝐹 ∈ dom ⇝ ) |
75 |
74
|
expr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → 𝐹 ∈ dom ⇝ ) ) |
76 |
9 75
|
syl5 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → 𝐹 ∈ dom ⇝ ) ) |
77 |
76
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → 𝐹 ∈ dom ⇝ ) ) |
78 |
77
|
rexlimdvw |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → 𝐹 ∈ dom ⇝ ) ) |
79 |
7 78
|
mpd |
⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ ) |