This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvgcau

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

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

Proof

Step Hyp Ref Expression
1 cvgcau.1 ⊢ Ⅎ _ j F
2 cvgcau.2 ⊢ Ⅎ _ k F
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 ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ F ⁡ k − F ⁡ j < x ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ 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 ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ F ⁡ k − F ⁡ j < x
13 11 4 12 syl2anc ⊢ φ → F ∈ dom ⁡ ⇝ ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ F ⁡ k − F ⁡ j < x
14 6 13 mpbid ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ F ⁡ k − F ⁡ j < x
15 10 14 7 rspcdva ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ F ⁡ k − F ⁡ j < X