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∈ℤ≥jB∈ℂ∧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∈ℤ≥jB∈ℂ∧B−0<x
6 0cn ⊢0∈ℂ
7 6 biantrur ⊢∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−0<x↔0∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧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∈ℤ≥jB∈ℂ∧B−0<x↔∀k∈ℤ≥jB∈ℂ∧B<x
13 12 rexbii ⊢∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−0<x↔∃j∈Z∀k∈ℤ≥jB∈ℂ∧B<x
14 13 ralbii ⊢∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−0<x↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B<x
15 7 14 bitr3i ⊢0∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−0<x↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B<x
16 5 15 bitrdi ⊢φ→F⇝0↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B<x