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∈ℤ≥jB<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∈ℤ≥jB−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∈ℤ≥jB−0<x↔∀k∈ℤ≥jB<x
15 14 rexbidva ⊢φ→∃j∈Z∀k∈ℤ≥jB−0<x↔∃j∈Z∀k∈ℤ≥jB<x
16 15 ralbidv ⊢φ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB−0<x↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB<x
17 7 16 bitrd ⊢φ→F⇝0↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB<x