Step | Hyp | Ref
| Expression |
1 | | eldm2g 5768 |
. . . 4
⊢ (𝐹 ∈ dom ⇝ →
(𝐹 ∈ dom ⇝
↔ ∃𝑚〈𝐹, 𝑚〉 ∈ ⇝ )) |
2 | 1 | ibi 270 |
. . 3
⊢ (𝐹 ∈ dom ⇝ →
∃𝑚〈𝐹, 𝑚〉 ∈ ⇝ ) |
3 | | df-br 5054 |
. . . . 5
⊢ (𝐹 ⇝ 𝑚 ↔ 〈𝐹, 𝑚〉 ∈ ⇝ ) |
4 | | caucvgb.1 |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
5 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → 𝑀 ∈ ℤ) |
6 | | 1rp 12590 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
7 | 6 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → 1 ∈
ℝ+) |
8 | | eqidd 2738 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
9 | | simpr 488 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → 𝐹 ⇝ 𝑚) |
10 | 4, 5, 7, 8, 9 | climi 15071 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝑚)) < 1)) |
11 | | simpl 486 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝑚)) < 1) → (𝐹‘𝑘) ∈ ℂ) |
12 | 11 | ralimi 3083 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝑚)) < 1) → ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
13 | 12 | reximi 3166 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝑚)) < 1) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
14 | 10, 13 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
15 | 14 | ex 416 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝑚 → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) |
16 | 3, 15 | syl5bir 246 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (〈𝐹, 𝑚〉 ∈ ⇝ → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) |
17 | 16 | exlimdv 1941 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (∃𝑚〈𝐹, 𝑚〉 ∈ ⇝ → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) |
18 | 2, 17 | syl5 34 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ dom ⇝ → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) |
19 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑗 = 𝑛 → (ℤ≥‘𝑗) =
(ℤ≥‘𝑛)) |
20 | 19 | raleqdv 3325 |
. . . . . 6
⊢ (𝑗 = 𝑛 → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) |
21 | 20 | cbvrexvw 3359 |
. . . . 5
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
22 | 21 | a1i 11 |
. . . 4
⊢ (𝑥 = 1 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) |
23 | | simpl 486 |
. . . . . . 7
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → (𝐹‘𝑘) ∈ ℂ) |
24 | 23 | ralimi 3083 |
. . . . . 6
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
25 | 24 | reximi 3166 |
. . . . 5
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
26 | 25 | ralimi 3083 |
. . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
27 | 6 | a1i 11 |
. . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → 1 ∈
ℝ+) |
28 | 22, 26, 27 | rspcdva 3539 |
. . 3
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
29 | 28 | a1i 11 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) |
30 | | eluzelz 12448 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) |
31 | 30, 4 | eleq2s 2856 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
32 | | eqid 2737 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
33 | 32 | climcau 15234 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) |
34 | 31, 33 | sylan 583 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) |
35 | 32 | r19.29uz 14914 |
. . . . . . . . . 10
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ ∧ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
36 | 35 | ex 416 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
37 | 36 | ralimdv 3101 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
38 | 34, 37 | mpan9 510 |
. . . . . . 7
⊢ (((𝑛 ∈ 𝑍 ∧ 𝐹 ∈ dom ⇝ ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
39 | 38 | an32s 652 |
. . . . . 6
⊢ (((𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
40 | 39 | adantll 714 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
41 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
42 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) |
43 | 42 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑚) ∈ ℂ)) |
44 | 43 | rspccva 3536 |
. . . . . . . 8
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑚) ∈ ℂ) |
45 | 41, 44 | sylan 583 |
. . . . . . 7
⊢ ((((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑚) ∈ ℂ) |
46 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) |
47 | 46 | ralimi 3083 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) |
48 | 42 | fvoveq1d 7235 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) = (abs‘((𝐹‘𝑚) − (𝐹‘𝑗)))) |
49 | 48 | breq1d 5063 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 ↔ (abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥)) |
50 | 49 | cbvralvw 3358 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) |
51 | 47, 50 | sylib 221 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) |
52 | 51 | reximi 3166 |
. . . . . . . . . 10
⊢
(∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) |
53 | 52 | ralimi 3083 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) |
54 | 53 | adantl 485 |
. . . . . . . 8
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) |
55 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → (ℤ≥‘𝑗) =
(ℤ≥‘𝑖)) |
56 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖)) |
57 | 56 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝐹‘𝑚) − (𝐹‘𝑗)) = ((𝐹‘𝑚) − (𝐹‘𝑖))) |
58 | 57 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) = (abs‘((𝐹‘𝑚) − (𝐹‘𝑖)))) |
59 | 58 | breq1d 5063 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → ((abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ (abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥)) |
60 | 55, 59 | raleqbidv 3313 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑖 → (∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥)) |
61 | 60 | cbvrexvw 3359 |
. . . . . . . . . 10
⊢
(∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ ∃𝑖 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥) |
62 | | breq2 5057 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥 ↔ (abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦)) |
63 | 62 | rexralbidv 3220 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (∃𝑖 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥 ↔ ∃𝑖 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦)) |
64 | 61, 63 | syl5bb 286 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ ∃𝑖 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦)) |
65 | 64 | cbvralvw 3358 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ ∀𝑦 ∈ ℝ+ ∃𝑖 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦) |
66 | 54, 65 | sylib 221 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → ∀𝑦 ∈ ℝ+ ∃𝑖 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦) |
67 | | simpll 767 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → 𝐹 ∈ 𝑉) |
68 | 32, 45, 66, 67 | caucvg 15242 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → 𝐹 ∈ dom ⇝ ) |
69 | 68 | adantlll 718 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → 𝐹 ∈ dom ⇝ ) |
70 | 40, 69 | impbida 801 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
71 | 4, 32 | cau4 14920 |
. . . . 5
⊢ (𝑛 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
72 | 71 | ad2antrl 728 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
73 | 70, 72 | bitr4d 285 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
74 | 73 | rexlimdvaa 3204 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))) |
75 | 18, 29, 74 | pm5.21ndd 384 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |