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 ⊢Ⅎ_kF
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∈ℤ≥jB∈ℂ∧B−A<X

Proof

Step Hyp Ref Expression
1 clim2d.k ⊢Ⅎkφ
2 clim2d.f ⊢Ⅎ_kF
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∈ℤ≥jB∈ℂ∧B−A<x
13 5 12 mpbid ⊢φ→A∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x
14 13 simprd ⊢φ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧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∈ℤ≥jB∈ℂ∧B−A<x↔∀k∈ℤ≥jB∈ℂ∧B−A<X
18 17 rexbidv ⊢x=X→∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x↔∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<X
19 18 rspcva ⊢X∈ℝ+∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x→∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<X
20 7 14 19 syl2anc ⊢φ→∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<X