Metamath Proof Explorer

Theorem clim2d

Description: The limit of complex number sequence F is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses clim2d.k ⊢ Ⅎ k φ
clim2d.f ⊢ Ⅎ _ k F
clim2d.m ⊢ φ → M ∈ ℤ
clim2d.z ⊢ Z = ℤ ≥ M
clim2d.c ⊢ φ → F ⇝ A
clim2d.b ⊢ φ ∧ k ∈ Z → F ⁡ k = B
clim2d.x ⊢ φ → X ∈ ℝ +
Assertion clim2d ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < X

Proof

Step Hyp Ref Expression
1 clim2d.k ⊢ Ⅎ k φ
2 clim2d.f ⊢ Ⅎ _ k F
3 clim2d.m ⊢ φ → M ∈ ℤ
4 clim2d.z ⊢ Z = ℤ ≥ M
5 clim2d.c ⊢ φ → F ⇝ A
6 clim2d.b ⊢ φ ∧ k ∈ Z → F ⁡ k = B
7 clim2d.x ⊢ φ → X ∈ ℝ +
8 climrel ⊢ Rel ⁡ ⇝
9 8 a1i ⊢ φ → Rel ⁡ ⇝
10 brrelex1 ⊢ Rel ⁡ ⇝ ∧ F ⇝ A → F ∈ V
11 9 5 10 syl2anc ⊢ φ → F ∈ V
12 1 2 4 3 11 6 clim2f2 ⊢ φ → F ⇝ A ↔ A ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
13 5 12 mpbid ⊢ φ → A ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
14 13 simprd ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
15 breq2 ⊢ x = X → B − A < x ↔ B − A < X
16 15 anbi2d ⊢ x = X → B ∈ ℂ ∧ B − A < x ↔ B ∈ ℂ ∧ B − A < X
17 16 ralbidv ⊢ x = X → ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x ↔ ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < X
18 17 rexbidv ⊢ x = X → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < X
19 18 rspcva ⊢ X ∈ ℝ + ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < X
20 7 14 19 syl2anc ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < X