Metamath Proof Explorer

Theorem caucvg

Description: A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of Gleason p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006) (Proof shortened by Mario Carneiro, 15-Feb-2014) (Revised by Mario Carneiro, 8-May-2016)

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

Proof

Step Hyp Ref Expression
1 caucvg.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 caucvg.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
3 caucvg.3 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )
4 caucvg.4 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
5 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
6 5 cbvmptv ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) )
7 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
8 1 7 eqsstri ⊢ 𝑍 ⊆ ℤ
9 zssre ⊢ ℤ ⊆ ℝ
10 8 9 sstri ⊢ 𝑍 ⊆ ℝ
11 10 a1i ⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
12 6 eqcomi ⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
13 2 12 fmptd ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) : 𝑍 ⟶ ℂ )
14 1rp ⊢ 1 ∈ ℝ+
15 14 ne0ii ⊢ ℝ+ ≠ ∅
16 r19.2z ⊢ ( ( ℝ+ ≠ ∅ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )
17 15 3 16 sylancr ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )
18 eluzel2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
19 18 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑀 ∈ ℤ )
20 19 a1d ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → 𝑀 ∈ ℤ ) )
21 20 rexlimiv ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → 𝑀 ∈ ℤ )
22 21 rexlimivw ⊢ ( ∃ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → 𝑀 ∈ ℤ )
23 17 22 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
24 1 uzsup ⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ )
25 23 24 syl ⊢ ( 𝜑 → sup ( 𝑍 , ℝ* , < ) = +∞ )
26 8 sseli ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
27 8 sseli ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
28 eluz ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ↔ 𝑗 ≤ 𝑘 ) )
29 26 27 28 syl2an ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ↔ 𝑗 ≤ 𝑘 ) )
30 29 biimprd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑗 ≤ 𝑘 → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) )
31 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
32 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) )
33 fvex ⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
34 31 32 33 fvmpt3i ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
35 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) )
36 35 32 33 fvmpt3i ⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
37 34 36 oveqan12rd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) )
38 37 fveq2d ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
39 38 breq1d ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
40 39 biimprd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ) )
41 30 40 imim12d ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
42 41 ex ⊢ ( 𝑗 ∈ 𝑍 → ( 𝑘 ∈ 𝑍 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ) ) ) )
43 42 com23 ⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ( 𝑘 ∈ 𝑍 → ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ) ) ) )
44 43 ralimdv2 ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
45 44 reximia ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ) )
46 45 ralimi ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ) )
47 3 46 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑗 ) ) ) < 𝑥 ) )
48 11 13 25 47 caucvgr ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ∈ dom ⇝𝑟 )
49 13 25 rlimdm ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ∈ dom ⇝𝑟 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) ) )
50 48 49 mpbid ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) )
51 6 50 eqbrtrid ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) )
52 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
53 2 52 fmptd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) : 𝑍 ⟶ ℂ )
54 1 23 53 rlimclim ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) ) )
55 51 54 mpbid ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) )
56 1 52 climmpt ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) ) )
57 23 4 56 syl2anc ⊢ ( 𝜑 → ( 𝐹 ⇝ ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) ) )
58 55 57 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) )
59 climrel ⊢ Rel ⇝
60 59 releldmi ⊢ ( 𝐹 ⇝ ( ⇝𝑟 ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ) → 𝐹 ∈ dom ⇝ )
61 58 60 syl ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )