Metamath Proof Explorer

Theorem clim2c

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

Ref Expression
Hypotheses clim2.1 ⊢Z=ℤ≥M
clim2.2 ⊢φ→M∈ℤ
clim2.3 ⊢φ→F∈V
clim2.4 ⊢φ∧k∈Z→F⁡k=B
clim2c.5 ⊢φ→A∈ℂ
clim2c.6 ⊢φ∧k∈Z→B∈ℂ
Assertion clim2c ⊢φ→F⇝A↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB−A<x

Proof

Step Hyp Ref Expression
1 clim2.1 ⊢Z=ℤ≥M
2 clim2.2 ⊢φ→M∈ℤ
3 clim2.3 ⊢φ→F∈V
4 clim2.4 ⊢φ∧k∈Z→F⁡k=B
5 clim2c.5 ⊢φ→A∈ℂ
6 clim2c.6 ⊢φ∧k∈Z→B∈ℂ
7 5 biantrurd ⊢φ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x↔A∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x
8 1 uztrn2 ⊢j∈Z∧k∈ℤ≥j→k∈Z
9 6 biantrurd ⊢φ∧k∈Z→B−A<x↔B∈ℂ∧B−A<x
10 8 9 sylan2 ⊢φ∧j∈Z∧k∈ℤ≥j→B−A<x↔B∈ℂ∧B−A<x
11 10 anassrs ⊢φ∧j∈Z∧k∈ℤ≥j→B−A<x↔B∈ℂ∧B−A<x
12 11 ralbidva ⊢φ∧j∈Z→∀k∈ℤ≥jB−A<x↔∀k∈ℤ≥jB∈ℂ∧B−A<x
13 12 rexbidva ⊢φ→∃j∈Z∀k∈ℤ≥jB−A<x↔∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x
14 13 ralbidv ⊢φ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB−A<x↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x
15 1 2 3 4 clim2 ⊢φ→F⇝A↔A∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x
16 7 14 15 3bitr4rd ⊢φ→F⇝A↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB−A<x