Metamath Proof Explorer

Theorem clim2c

Description: Express the predicate F converges to A . (Contributed by NM, 24-Feb-2008) (Revised by Mario Carneiro, 31-Jan-2014)

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

Proof

Step Hyp Ref Expression
1 clim2.1 ⊢ Z = ℤ ≥ M
2 clim2.2 ⊢ φ → M ∈ ℤ
3 clim2.3 ⊢ φ → F ∈ V
4 clim2.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = B
5 clim2c.5 ⊢ φ → A ∈ ℂ
6 clim2c.6 ⊢ φ ∧ k ∈ Z → B ∈ ℂ
7 5 biantrurd ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x ↔ A ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
8 1 uztrn2 ⊢ j ∈ Z ∧ k ∈ ℤ ≥ j → k ∈ Z
9 6 biantrurd ⊢ φ ∧ k ∈ Z → B − A < x ↔ B ∈ ℂ ∧ B − A < x
10 8 9 sylan2 ⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → B − A < x ↔ B ∈ ℂ ∧ B − A < x
11 10 anassrs ⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → B − A < x ↔ B ∈ ℂ ∧ B − A < x
12 11 ralbidva ⊢ φ ∧ j ∈ Z → ∀ k ∈ ℤ ≥ j B − A < x ↔ ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
13 12 rexbidva ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B − A < x ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
14 13 ralbidv ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B − A < x ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
15 1 2 3 4 clim2 ⊢ φ → F ⇝ A ↔ A ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − A < x
16 7 14 15 3bitr4rd ⊢ φ → F ⇝ A ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B − A < x