This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climi2

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 climi2 ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j 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 1 2 3 4 5 climi ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < C
7 simpr ⊢ B ∈ ℂ ∧ B − A < C → B − A < C
8 7 ralimi ⊢ ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < C → ∀ k ∈ ℤ ≥ j B − A < C
9 8 reximi ⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < C → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B − A < C
10 6 9 syl ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B − A < C