| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eldm2g 5910 | . . . 4
⊢ (𝐹 ∈ dom ⇝ →
(𝐹 ∈ dom ⇝
↔ ∃𝑚〈𝐹, 𝑚〉 ∈ ⇝ )) | 
| 2 | 1 | ibi 267 | . . 3
⊢ (𝐹 ∈ dom ⇝ →
∃𝑚〈𝐹, 𝑚〉 ∈ ⇝ ) | 
| 3 |  | df-br 5144 | . . . . 5
⊢ (𝐹 ⇝ 𝑚 ↔ 〈𝐹, 𝑚〉 ∈ ⇝ ) | 
| 4 |  | caucvgb.1 | . . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 5 |  | simpll 767 | . . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → 𝑀 ∈ ℤ) | 
| 6 |  | 1rp 13038 | . . . . . . . . 9
⊢ 1 ∈
ℝ+ | 
| 7 | 6 | a1i 11 | . . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → 1 ∈
ℝ+) | 
| 8 |  | eqidd 2738 | . . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) | 
| 9 |  | simpr 484 | . . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → 𝐹 ⇝ 𝑚) | 
| 10 | 4, 5, 7, 8, 9 | climi 15546 | . . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝑚)) < 1)) | 
| 11 |  | simpl 482 | . . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝑚)) < 1) → (𝐹‘𝑘) ∈ ℂ) | 
| 12 | 11 | ralimi 3083 | . . . . . . . 8
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝑚)) < 1) → ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) | 
| 13 | 12 | reximi 3084 | . . . . . . 7
⊢
(∃𝑛 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝑚)) < 1) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) | 
| 14 | 10, 13 | syl 17 | . . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ 𝐹 ⇝ 𝑚) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) | 
| 15 | 14 | ex 412 | . . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝑚 → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) | 
| 16 | 3, 15 | biimtrrid 243 | . . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (〈𝐹, 𝑚〉 ∈ ⇝ → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) | 
| 17 | 16 | exlimdv 1933 | . . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (∃𝑚〈𝐹, 𝑚〉 ∈ ⇝ → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) | 
| 18 | 2, 17 | syl5 34 | . 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ dom ⇝ → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) | 
| 19 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑗 = 𝑛 → (ℤ≥‘𝑗) =
(ℤ≥‘𝑛)) | 
| 20 | 19 | raleqdv 3326 | . . . . . 6
⊢ (𝑗 = 𝑛 → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) | 
| 21 | 20 | cbvrexvw 3238 | . . . . 5
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) | 
| 22 | 21 | a1i 11 | . . . 4
⊢ (𝑥 = 1 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) | 
| 23 |  | simpl 482 | . . . . . . 7
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → (𝐹‘𝑘) ∈ ℂ) | 
| 24 | 23 | ralimi 3083 | . . . . . 6
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) | 
| 25 | 24 | reximi 3084 | . . . . 5
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) | 
| 26 | 25 | ralimi 3083 | . . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) | 
| 27 | 6 | a1i 11 | . . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → 1 ∈
ℝ+) | 
| 28 | 22, 26, 27 | rspcdva 3623 | . . 3
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) | 
| 29 | 28 | a1i 11 | . 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) | 
| 30 |  | eluzelz 12888 | . . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) | 
| 31 | 30, 4 | eleq2s 2859 | . . . . . . . . 9
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) | 
| 32 |  | eqid 2737 | . . . . . . . . . 10
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) | 
| 33 | 32 | climcau 15707 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) | 
| 34 | 31, 33 | sylan 580 | . . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) | 
| 35 | 32 | r19.29uz 15389 | . . . . . . . . . 10
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ ∧ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) | 
| 36 | 35 | ex 412 | . . . . . . . . 9
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | 
| 37 | 36 | ralimdv 3169 | . . . . . . . 8
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | 
| 38 | 34, 37 | mpan9 506 | . . . . . . 7
⊢ (((𝑛 ∈ 𝑍 ∧ 𝐹 ∈ dom ⇝ ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) | 
| 39 | 38 | an32s 652 | . . . . . 6
⊢ (((𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) | 
| 40 | 39 | adantll 714 | . . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) | 
| 41 |  | simplrr 778 | . . . . . . . 8
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) | 
| 42 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) | 
| 43 | 42 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑚) ∈ ℂ)) | 
| 44 | 43 | rspccva 3621 | . . . . . . . 8
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑚) ∈ ℂ) | 
| 45 | 41, 44 | sylan 580 | . . . . . . 7
⊢ ((((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑚) ∈ ℂ) | 
| 46 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) | 
| 47 | 46 | ralimi 3083 | . . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) | 
| 48 | 42 | fvoveq1d 7453 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) = (abs‘((𝐹‘𝑚) − (𝐹‘𝑗)))) | 
| 49 | 48 | breq1d 5153 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 ↔ (abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥)) | 
| 50 | 49 | cbvralvw 3237 | . . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) | 
| 51 | 47, 50 | sylib 218 | . . . . . . . . . . 11
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) | 
| 52 | 51 | reximi 3084 | . . . . . . . . . 10
⊢
(∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) | 
| 53 | 52 | ralimi 3083 | . . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) | 
| 54 | 53 | adantl 481 | . . . . . . . 8
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥) | 
| 55 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → (ℤ≥‘𝑗) =
(ℤ≥‘𝑖)) | 
| 56 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖)) | 
| 57 | 56 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝐹‘𝑚) − (𝐹‘𝑗)) = ((𝐹‘𝑚) − (𝐹‘𝑖))) | 
| 58 | 57 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) = (abs‘((𝐹‘𝑚) − (𝐹‘𝑖)))) | 
| 59 | 58 | breq1d 5153 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → ((abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ (abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥)) | 
| 60 | 55, 59 | raleqbidv 3346 | . . . . . . . . . . 11
⊢ (𝑗 = 𝑖 → (∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥)) | 
| 61 | 60 | cbvrexvw 3238 | . . . . . . . . . 10
⊢
(∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ ∃𝑖 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥) | 
| 62 |  | breq2 5147 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥 ↔ (abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦)) | 
| 63 | 62 | rexralbidv 3223 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (∃𝑖 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑥 ↔ ∃𝑖 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦)) | 
| 64 | 61, 63 | bitrid 283 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ ∃𝑖 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦)) | 
| 65 | 64 | cbvralvw 3237 | . . . . . . . 8
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑚) − (𝐹‘𝑗))) < 𝑥 ↔ ∀𝑦 ∈ ℝ+ ∃𝑖 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦) | 
| 66 | 54, 65 | sylib 218 | . . . . . . 7
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → ∀𝑦 ∈ ℝ+ ∃𝑖 ∈
(ℤ≥‘𝑛)∀𝑚 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑚) − (𝐹‘𝑖))) < 𝑦) | 
| 67 |  | simpll 767 | . . . . . . 7
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → 𝐹 ∈ 𝑉) | 
| 68 | 32, 45, 66, 67 | caucvg 15715 | . . . . . 6
⊢ (((𝐹 ∈ 𝑉 ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → 𝐹 ∈ dom ⇝ ) | 
| 69 | 68 | adantlll 718 | . . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → 𝐹 ∈ dom ⇝ ) | 
| 70 | 40, 69 | impbida 801 | . . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | 
| 71 | 4, 32 | cau4 15395 | . . . . 5
⊢ (𝑛 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | 
| 72 | 71 | ad2antrl 728 | . . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | 
| 73 | 70, 72 | bitr4d 282 | . . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | 
| 74 | 73 | rexlimdvaa 3156 | . 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))) | 
| 75 | 18, 29, 74 | pm5.21ndd 379 | 1
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |