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

Metamath Proof Explorer

Theorem caucvgbf

Description: A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of Gleason p. 180. (Contributed by Glauco Siliprandi, 15-Feb-2025)

Ref Expression
Hypotheses caucvgbf.1 ⊢ Ⅎ 𝑗 𝐹
caucvgbf.2 ⊢ Ⅎ 𝑘 𝐹
caucvgbf.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion caucvgbf ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 caucvgbf.1 ⊢ Ⅎ 𝑗 𝐹
2 caucvgbf.2 ⊢ Ⅎ 𝑘 𝐹
3 caucvgbf.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 3 caucvgb ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ) )
5 nfcv ⊢ Ⅎ 𝑗 ( ℤ≥ ‘ 𝑖 )
6 nfcv ⊢ Ⅎ 𝑗 𝑙
7 1 6 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
8 7 nfel1 ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ∈ ℂ
9 nfcv ⊢ Ⅎ 𝑗 abs
10 nfcv ⊢ Ⅎ 𝑗 −
11 nfcv ⊢ Ⅎ 𝑗 𝑖
12 1 11 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑖 )
13 7 10 12 nfov ⊢ Ⅎ 𝑗 ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) )
14 9 13 nffv ⊢ Ⅎ 𝑗 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) )
15 nfcv ⊢ Ⅎ 𝑗 <
16 nfcv ⊢ Ⅎ 𝑗 𝑥
17 14 15 16 nfbr ⊢ Ⅎ 𝑗 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥
18 8 17 nfan ⊢ Ⅎ 𝑗 ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 )
19 5 18 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 )
20 nfv ⊢ Ⅎ 𝑖 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )
21 nfcv ⊢ Ⅎ 𝑘 𝑙
22 2 21 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 )
23 22 nfel1 ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 ) ∈ ℂ
24 nfcv ⊢ Ⅎ 𝑘 abs
25 nfcv ⊢ Ⅎ 𝑘 −
26 nfcv ⊢ Ⅎ 𝑘 𝑖
27 2 26 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑖 )
28 22 25 27 nfov ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) )
29 24 28 nffv ⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) )
30 nfcv ⊢ Ⅎ 𝑘 <
31 nfcv ⊢ Ⅎ 𝑘 𝑥
32 29 30 31 nfbr ⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥
33 23 32 nfan ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 )
34 nfv ⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 )
35 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑘 ) )
36 35 eleq1d ⊢ ( 𝑙 = 𝑘 → ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
37 35 fvoveq1d ⊢ ( 𝑙 = 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) )
38 37 breq1d ⊢ ( 𝑙 = 𝑘 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) )
39 36 38 anbi12d ⊢ ( 𝑙 = 𝑘 → ( ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ) )
40 33 34 39 cbvralw ⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) )
41 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑗 ) )
42 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) )
43 42 oveq2d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) )
44 43 fveq2d ⊢ ( 𝑖 = 𝑗 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
45 44 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
46 45 anbi2d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
47 41 46 raleqbidv ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
48 40 47 bitrid ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
49 19 20 48 cbvrexw ⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
50 49 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
51 4 50 bitrdi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )