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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
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 ⇝𝑟 )