Metamath Proof Explorer


Theorem caucvgb

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

Ref Expression
Hypothesis caucvgb.1 𝑍 = ( ℤ𝑀 )
Assertion caucvgb ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 caucvgb.1 𝑍 = ( ℤ𝑀 )
2 eldm2g ( 𝐹 ∈ dom ⇝ → ( 𝐹 ∈ dom ⇝ ↔ ∃ 𝑚𝐹 , 𝑚 ⟩ ∈ ⇝ ) )
3 2 ibi ( 𝐹 ∈ dom ⇝ → ∃ 𝑚𝐹 , 𝑚 ⟩ ∈ ⇝ )
4 df-br ( 𝐹𝑚 ↔ ⟨ 𝐹 , 𝑚 ⟩ ∈ ⇝ )
5 simpll ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ 𝐹𝑚 ) → 𝑀 ∈ ℤ )
6 1rp 1 ∈ ℝ+
7 6 a1i ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ 𝐹𝑚 ) → 1 ∈ ℝ+ )
8 eqidd ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ 𝐹𝑚 ) ∧ 𝑘𝑍 ) → ( 𝐹𝑘 ) = ( 𝐹𝑘 ) )
9 simpr ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ 𝐹𝑚 ) → 𝐹𝑚 )
10 1 5 7 8 9 climi ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ 𝐹𝑚 ) → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝑚 ) ) < 1 ) )
11 simpl ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝑚 ) ) < 1 ) → ( 𝐹𝑘 ) ∈ ℂ )
12 11 ralimi ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝑚 ) ) < 1 ) → ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ )
13 12 reximi ( ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝑚 ) ) < 1 ) → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ )
14 10 13 syl ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ 𝐹𝑚 ) → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ )
15 14 ex ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( 𝐹𝑚 → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) )
16 4 15 syl5bir ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( ⟨ 𝐹 , 𝑚 ⟩ ∈ ⇝ → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) )
17 16 exlimdv ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( ∃ 𝑚𝐹 , 𝑚 ⟩ ∈ ⇝ → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) )
18 3 17 syl5 ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( 𝐹 ∈ dom ⇝ → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) )
19 fveq2 ( 𝑗 = 𝑛 → ( ℤ𝑗 ) = ( ℤ𝑛 ) )
20 19 raleqdv ( 𝑗 = 𝑛 → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℂ ↔ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) )
21 20 cbvrexvw ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℂ ↔ ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ )
22 21 a1i ( 𝑥 = 1 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℂ ↔ ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) )
23 simpl ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ( 𝐹𝑘 ) ∈ ℂ )
24 23 ralimi ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℂ )
25 24 reximi ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℂ )
26 25 ralimi ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℂ )
27 6 a1i ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → 1 ∈ ℝ+ )
28 22 26 27 rspcdva ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ )
29 28 a1i ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) )
30 eluzelz ( 𝑛 ∈ ( ℤ𝑀 ) → 𝑛 ∈ ℤ )
31 30 1 eleq2s ( 𝑛𝑍𝑛 ∈ ℤ )
32 eqid ( ℤ𝑛 ) = ( ℤ𝑛 )
33 32 climcau ( ( 𝑛 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
34 31 33 sylan ( ( 𝑛𝑍𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
35 32 r19.29uz ( ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ∧ ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
36 35 ex ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ → ( ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 → ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )
37 36 ralimdv ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ → ( ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )
38 34 37 mpan9 ( ( ( 𝑛𝑍𝐹 ∈ dom ⇝ ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
39 38 an32s ( ( ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
40 39 adantll ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
41 simplrr ( ( ( 𝐹𝑉 ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) → ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ )
42 fveq2 ( 𝑘 = 𝑚 → ( 𝐹𝑘 ) = ( 𝐹𝑚 ) )
43 42 eleq1d ( 𝑘 = 𝑚 → ( ( 𝐹𝑘 ) ∈ ℂ ↔ ( 𝐹𝑚 ) ∈ ℂ ) )
44 43 rspccva ( ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑚 ) ∈ ℂ )
45 41 44 sylan ( ( ( ( 𝐹𝑉 ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑚 ) ∈ ℂ )
46 simpr ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
47 46 ralimi ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
48 42 fvoveq1d ( 𝑘 = 𝑚 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) = ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) )
49 48 breq1d ( 𝑘 = 𝑚 → ( ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
50 49 cbvralvw ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
51 47 50 sylib ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
52 51 reximi ( ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
53 52 ralimi ( ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
54 53 adantl ( ( ( 𝐹𝑉 ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 )
55 fveq2 ( 𝑗 = 𝑖 → ( ℤ𝑗 ) = ( ℤ𝑖 ) )
56 fveq2 ( 𝑗 = 𝑖 → ( 𝐹𝑗 ) = ( 𝐹𝑖 ) )
57 56 oveq2d ( 𝑗 = 𝑖 → ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) = ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) )
58 57 fveq2d ( 𝑗 = 𝑖 → ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) = ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) )
59 58 breq1d ( 𝑗 = 𝑖 → ( ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑥 ) )
60 55 59 raleqbidv ( 𝑗 = 𝑖 → ( ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑥 ) )
61 60 cbvrexvw ( ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ↔ ∃ 𝑖 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑥 )
62 breq2 ( 𝑥 = 𝑦 → ( ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑦 ) )
63 62 rexralbidv ( 𝑥 = 𝑦 → ( ∃ 𝑖 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑥 ↔ ∃ 𝑖 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑦 ) )
64 61 63 syl5bb ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ↔ ∃ 𝑖 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑦 ) )
65 64 cbvralvw ( ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ↔ ∀ 𝑦 ∈ ℝ+𝑖 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑦 )
66 54 65 sylib ( ( ( 𝐹𝑉 ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) → ∀ 𝑦 ∈ ℝ+𝑖 ∈ ( ℤ𝑛 ) ∀ 𝑚 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝐹𝑚 ) − ( 𝐹𝑖 ) ) ) < 𝑦 )
67 simpll ( ( ( 𝐹𝑉 ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) → 𝐹𝑉 )
68 32 45 66 67 caucvg ( ( ( 𝐹𝑉 ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) → 𝐹 ∈ dom ⇝ )
69 68 adantlll ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) → 𝐹 ∈ dom ⇝ )
70 40 69 impbida ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )
71 1 32 cau4 ( 𝑛𝑍 → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )
72 71 ad2antrl ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )
73 70 72 bitr4d ( ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) ∧ ( 𝑛𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ ) ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )
74 73 rexlimdvaa ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( ∃ 𝑛𝑍𝑘 ∈ ( ℤ𝑛 ) ( 𝐹𝑘 ) ∈ ℂ → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) ) )
75 18 29 74 pm5.21ndd ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )