Metamath Proof Explorer

Theorem clim0cf

Description: Express the predicate F converges to 0 . Similar to clim , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses clim0cf.nf ⊢ Ⅎ _ k F
clim0cf.z ⊢ Z = ℤ ≥ M
clim0cf.m ⊢ φ → M ∈ ℤ
clim0cf.f ⊢ φ → F ∈ V
clim0cf.fv ⊢ φ ∧ k ∈ Z → F ⁡ k = B
clim0cf.b ⊢ φ ∧ k ∈ Z → B ∈ ℂ
Assertion clim0cf ⊢ φ → F ⇝ 0 ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B < x

Proof

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