Metamath Proof Explorer

Theorem cvgcau

Description: A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025)

Ref Expression
Hypotheses cvgcau.1 ⊢Ⅎ_jF
cvgcau.2 ⊢Ⅎ_kF
cvgcau.3 ⊢φ→M∈Z
cvgcau.4 ⊢φ→F∈V
cvgcau.5 ⊢Z=ℤ≥M
cvgcau.6 ⊢φ→F∈dom⁡⇝
cvgcau.7 ⊢φ→X∈ℝ+
Assertion cvgcau ⊢φ→∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<X

Proof

Step Hyp Ref Expression
1 cvgcau.1 ⊢Ⅎ_jF
2 cvgcau.2 ⊢Ⅎ_kF
3 cvgcau.3 ⊢φ→M∈Z
4 cvgcau.4 ⊢φ→F∈V
5 cvgcau.5 ⊢Z=ℤ≥M
6 cvgcau.6 ⊢φ→F∈dom⁡⇝
7 cvgcau.7 ⊢φ→X∈ℝ+
8 breq2 ⊢x=X→F⁡k−F⁡j<x↔F⁡k−F⁡j<X
9 8 anbi2d ⊢x=X→F⁡k∈ℂ∧F⁡k−F⁡j<x↔F⁡k∈ℂ∧F⁡k−F⁡j<X
10 9 rexralbidv ⊢x=X→∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<x↔∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<X
11 5 3 eluzelz2d ⊢φ→M∈ℤ
12 1 2 5 caucvgbf ⊢M∈ℤ∧F∈V→F∈dom⁡⇝↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<x
13 11 4 12 syl2anc ⊢φ→F∈dom⁡⇝↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<x
14 6 13 mpbid ⊢φ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<x
15 10 14 7 rspcdva ⊢φ→∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<X