Metamath Proof Explorer

Theorem clim2f

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A , with more general quantifier restrictions than clim . Similar to clim2 , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 nf ⊢Ⅎ_kF
2 clim2f.z ⊢Z=ℤ≥M
3 clim2f.m ⊢φ→M∈ℤ
4 clim2f.f ⊢φ→F∈V
5 clim2f.b ⊢φ∧k∈Z→F⁡k=B
6 eqidd ⊢φ∧k∈ℤ→F⁡k=F⁡k
7 1 4 6 climf ⊢φ→F⇝A↔A∈ℂ∧∀x∈ℝ+∃j∈ℤ∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x
8 2 uztrn2 ⊢j∈Z∧k∈ℤ≥j→k∈Z
9 5 eleq1d ⊢φ∧k∈Z→F⁡k∈ℂ↔B∈ℂ
10 5 fvoveq1d ⊢φ∧k∈Z→F⁡k−A=B−A
11 10 breq1d ⊢φ∧k∈Z→F⁡k−A<x↔B−A<x
12 9 11 anbi12d ⊢φ∧k∈Z→F⁡k∈ℂ∧F⁡k−A<x↔B∈ℂ∧B−A<x
13 8 12 sylan2 ⊢φ∧j∈Z∧k∈ℤ≥j→F⁡k∈ℂ∧F⁡k−A<x↔B∈ℂ∧B−A<x
14 13 anassrs ⊢φ∧j∈Z∧k∈ℤ≥j→F⁡k∈ℂ∧F⁡k−A<x↔B∈ℂ∧B−A<x
15 14 ralbidva ⊢φ∧j∈Z→∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x↔∀k∈ℤ≥jB∈ℂ∧B−A<x
16 15 rexbidva ⊢φ→∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x↔∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x
17 2 rexuz3 ⊢M∈ℤ→∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x↔∃j∈ℤ∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x
18 3 17 syl ⊢φ→∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x↔∃j∈ℤ∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x
19 16 18 bitr3d ⊢φ→∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x↔∃j∈ℤ∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x
20 19 ralbidv ⊢φ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x↔∀x∈ℝ+∃j∈ℤ∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x
21 20 anbi2d ⊢φ→A∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x↔A∈ℂ∧∀x∈ℝ+∃j∈ℤ∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−A<x
22 7 21 bitr4d ⊢φ→F⇝A↔A∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jB∈ℂ∧B−A<x