Theorem cvgcau

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

	Ref	Expression
Hypotheses	cvgcau.1	⊢ Ⅎ 𝑗 𝐹
	cvgcau.2	⊢ Ⅎ 𝑘 𝐹
	cvgcau.3	⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
	cvgcau.4	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	cvgcau.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	cvgcau.6	⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
	cvgcau.7	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
Assertion	cvgcau	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		cvgcau.1	⊢ Ⅎ 𝑗 𝐹
2		cvgcau.2	⊢ Ⅎ 𝑘 𝐹
3		cvgcau.3	⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
4		cvgcau.4	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
5		cvgcau.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6		cvgcau.6	⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
7		cvgcau.7	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
8		breq2	⊢ ( 𝑥 = 𝑋 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )
9	8	anbi2d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) )
10	9	rexralbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) )
11	5 3	eluzelz2d	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
12	1 2 5	caucvgbf	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
13	11 4 12	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
14	6 13	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
15	10 14 7	rspcdva	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )