Metamath Proof Explorer

Theorem clim0c

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

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

Proof

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