Metamath Proof Explorer

Theorem cvgcaule

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

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

Proof

Step Hyp Ref Expression
1 cvgcaule.1 ⊢ Ⅎ 𝑗 𝐹
2 cvgcaule.2 ⊢ Ⅎ 𝑘 𝐹
3 cvgcaule.3 ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
4 cvgcaule.4 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
5 cvgcaule.5 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6 cvgcaule.6 ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
7 cvgcaule.7 ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
8 1 2 3 4 5 6 7 cvgcau ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )
9 nfv ⊢ Ⅎ 𝑘 ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 )
10 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 )
11 9 10 nfan ⊢ Ⅎ 𝑘 ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )
12 rspa ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )
13 12 simpld ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
14 13 adantll ⊢ ( ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
15 13 adantll ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
16 5 uzid3 ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
17 nfcv ⊢ Ⅎ 𝑘 𝑗
18 2 17 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
19 18 nfel1 ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) ∈ ℂ
20 nfcv ⊢ Ⅎ 𝑘 abs
21 nfcv ⊢ Ⅎ 𝑘 −
22 18 21 18 nfov ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) )
23 20 22 nffv ⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) )
24 nfcv ⊢ Ⅎ 𝑘 <
25 nfcv ⊢ Ⅎ 𝑘 𝑋
26 23 24 25 nfbr ⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋
27 19 26 nfan ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 )
28 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
29 28 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) )
30 28 fvoveq1d ⊢ ( 𝑘 = 𝑗 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
31 30 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )
32 29 31 anbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ↔ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) )
33 27 32 rspc ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) )
34 16 33 syl ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) )
35 34 imp ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )
36 35 simpld ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
37 36 adantr ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
38 15 37 subcld ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ )
39 38 abscld ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
40 39 adantlll ⊢ ( ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
41 simplll ⊢ ( ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑋 ∈ ℝ+ )
42 41 rpred ⊢ ( ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑋 ∈ ℝ )
43 12 adantll ⊢ ( ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) )
44 43 simprd ⊢ ( ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 )
45 40 42 44 ltled ⊢ ( ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑋 )
46 14 45 jca ⊢ ( ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑋 ) )
47 11 46 ralrimia ⊢ ( ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑋 ) )
48 47 ex ⊢ ( ( 𝑋 ∈ ℝ+ ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑋 ) ) )
49 48 reximdva ⊢ ( 𝑋 ∈ ℝ+ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑋 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑋 ) ) )
50 7 8 49 sylc ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑋 ) )