Metamath Proof Explorer

Theorem climd

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 climd.1 ⊢ Ⅎ k φ
2 climd.2 ⊢ Ⅎ _ k F
3 climd.3 ⊢ Z = ℤ ≥ M
4 climd.4 ⊢ φ → M ∈ ℤ
5 climd.5 ⊢ φ → F ⇝ A
6 climd.6 ⊢ φ ∧ k ∈ Z → F ⁡ k = B
7 climd.7 ⊢ φ → X ∈ ℝ +
8 climrel ⊢ Rel ⁡ ⇝
9 8 brrelex1i ⊢ F ⇝ A → F ∈ V
10 5 9 syl ⊢ φ → F ∈ V
11 1 2 3 4 10 6 clim2f2 ⊢ φ → F ⇝ A ↔ A ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
12 5 11 mpbid ⊢ φ → A ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
13 12 simprd ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
14 breq2 ⊢ x = X → B − A < x ↔ B − A < X
15 14 anbi2d ⊢ x = X → B ∈ ℂ ∧ B − A < x ↔ B ∈ ℂ ∧ B − A < X
16 15 rexralbidv ⊢ x = X → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < X
17 16 rspcva ⊢ X ∈ ℝ + ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < X
18 7 13 17 syl2anc ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < X