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 biimtrrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ⟨ 𝐹 , 𝑚 ⟩ ∈ ⇝ → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
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 bitrid ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 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 ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )