Metamath Proof Explorer

Theorem climi

Description: Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climi.1 ⊢ Z = ℤ ≥ M
climi.2 ⊢ φ → M ∈ ℤ
climi.3 ⊢ φ → C ∈ ℝ +
climi.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = B
climi.5 ⊢ φ → F ⇝ A
Assertion climi ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < C

Proof

Step Hyp Ref Expression
1 climi.1 ⊢ Z = ℤ ≥ M
2 climi.2 ⊢ φ → M ∈ ℤ
3 climi.3 ⊢ φ → C ∈ ℝ +
4 climi.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = B
5 climi.5 ⊢ φ → F ⇝ A
6 breq2 ⊢ x = C → B − A < x ↔ B − A < C
7 6 anbi2d ⊢ x = C → B ∈ ℂ ∧ B − A < x ↔ B ∈ ℂ ∧ B − A < C
8 7 rexralbidv ⊢ x = C → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < C
9 climrel ⊢ Rel ⁡ ⇝
10 9 brrelex1i ⊢ F ⇝ A → F ∈ V
11 5 10 syl ⊢ φ → F ∈ V
12 1 2 11 4 clim2 ⊢ φ → 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 8 14 3 rspcdva ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < C