Metamath Proof Explorer

Theorem caucvgr

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) (Revised by Mario Carneiro, 8-May-2016)

Ref Expression
Hypotheses caucvgr.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
caucvgr.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
caucvgr.3 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
caucvgr.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
Assertion caucvgr ( 𝜑 → 𝐹 ∈ dom ⇝𝑟 )

Proof

Step Hyp Ref Expression
1 caucvgr.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 caucvgr.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3 caucvgr.3 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
4 caucvgr.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
5 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑛 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑛 ) ) )
6 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
7 6 replimd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑛 ) = ( ( ℜ ‘ ( 𝐹 ‘ 𝑛 ) ) + ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
8 7 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝐴 ↦ ( ( ℜ ‘ ( 𝐹 ‘ 𝑛 ) ) + ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
9 5 8 eqtrd ⊢ ( 𝜑 → 𝐹 = ( 𝑛 ∈ 𝐴 ↦ ( ( ℜ ‘ ( 𝐹 ‘ 𝑛 ) ) + ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
10 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V )
11 ovexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ V )
12 ref ⊢ ℜ : ℂ ⟶ ℝ
13 resub ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( ℜ ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) = ( ( ℜ ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ℜ ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
14 13 fveq2d ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( abs ‘ ( ℜ ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ) = ( abs ‘ ( ( ℜ ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ℜ ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) )
15 subcl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ )
16 absrele ⊢ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ → ( abs ‘ ( ℜ ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
17 15 16 syl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( abs ‘ ( ℜ ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
18 14 17 eqbrtrrd ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( abs ‘ ( ( ℜ ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ℜ ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
19 1 2 3 4 12 18 caucvgrlem2 ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( ℜ ∘ 𝐹 ) ) )
20 ax-icn ⊢ i ∈ ℂ
21 20 elexi ⊢ i ∈ V
22 21 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → i ∈ V )
23 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V )
24 rlimconst ⊢ ( ( 𝐴 ⊆ ℝ ∧ i ∈ ℂ ) → ( 𝑛 ∈ 𝐴 ↦ i ) ⇝𝑟 i )
25 1 20 24 sylancl ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐴 ↦ i ) ⇝𝑟 i )
26 imf ⊢ ℑ : ℂ ⟶ ℝ
27 imsub ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( ℑ ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) = ( ( ℑ ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ℑ ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
28 27 fveq2d ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( abs ‘ ( ℑ ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ) = ( abs ‘ ( ( ℑ ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ℑ ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) )
29 absimle ⊢ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ → ( abs ‘ ( ℑ ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
30 15 29 syl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( abs ‘ ( ℑ ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
31 28 30 eqbrtrrd ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ( abs ‘ ( ( ℑ ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ℑ ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
32 1 2 3 4 26 31 caucvgrlem2 ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( ℑ ∘ 𝐹 ) ) )
33 22 23 25 32 rlimmul ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐴 ↦ ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ⇝𝑟 ( i · ( ⇝𝑟 ‘ ( ℑ ∘ 𝐹 ) ) ) )
34 10 11 19 33 rlimadd ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐴 ↦ ( ( ℜ ‘ ( 𝐹 ‘ 𝑛 ) ) + ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ⇝𝑟 ( ( ⇝𝑟 ‘ ( ℜ ∘ 𝐹 ) ) + ( i · ( ⇝𝑟 ‘ ( ℑ ∘ 𝐹 ) ) ) ) )
35 9 34 eqbrtrd ⊢ ( 𝜑 → 𝐹 ⇝𝑟 ( ( ⇝𝑟 ‘ ( ℜ ∘ 𝐹 ) ) + ( i · ( ⇝𝑟 ‘ ( ℑ ∘ 𝐹 ) ) ) ) )
36 rlimrel ⊢ Rel ⇝𝑟
37 36 releldmi ⊢ ( 𝐹 ⇝𝑟 ( ( ⇝𝑟 ‘ ( ℜ ∘ 𝐹 ) ) + ( i · ( ⇝𝑟 ‘ ( ℑ ∘ 𝐹 ) ) ) ) → 𝐹 ∈ dom ⇝𝑟 )
38 35 37 syl ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝𝑟 )