Metamath Proof Explorer

Theorem clim0

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
Assertion clim0 ⊢ φ → F ⇝ 0 ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ 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 1 2 3 4 clim2 ⊢ φ → F ⇝ 0 ↔ 0 ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − 0 < x
6 0cn ⊢ 0 ∈ ℂ
7 6 biantrur ⊢ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − 0 < x ↔ 0 ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − 0 < x
8 subid1 ⊢ B ∈ ℂ → B − 0 = B
9 8 fveq2d ⊢ B ∈ ℂ → B − 0 = B
10 9 breq1d ⊢ B ∈ ℂ → B − 0 < x ↔ B < x
11 10 pm5.32i ⊢ B ∈ ℂ ∧ B − 0 < x ↔ B ∈ ℂ ∧ B < x
12 11 ralbii ⊢ ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − 0 < x ↔ ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B < x
13 12 rexbii ⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − 0 < x ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B < x
14 13 ralbii ⊢ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − 0 < x ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B < x
15 7 14 bitr3i ⊢ 0 ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B − 0 < x ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B < x
16 5 15 bitrdi ⊢ φ → F ⇝ 0 ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j B ∈ ℂ ∧ B < x