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	$$⊢\phi \to A\subseteq ℝ$$
	caucvgr.2	$$⊢\phi \to F:A⟶ℂ$$
	caucvgr.3	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
	caucvgr.4	$$⊢\phi \to \forall x\in {ℝ}^{+}\exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<x\right)$$
Assertion	caucvgr	$$⊢\phi \to F\in \mathrm{dom}\underset{ℝ}{⇝}$$

Proof

Step	Hyp	Ref	Expression
1		caucvgr.1	$$⊢\phi \to A\subseteq ℝ$$
2		caucvgr.2	$$⊢\phi \to F:A⟶ℂ$$
3		caucvgr.3	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
4		caucvgr.4	$$⊢\phi \to \forall x\in {ℝ}^{+}\exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<x\right)$$
5	2	feqmptd	$$⊢\phi \to F=\left(n\in A⟼F\left(n\right)\right)$$
6	2	ffvelcdmda	$$⊢\left(\phi \wedge n\in A\right)\to F\left(n\right)\in ℂ$$
7	6	replimd	$$⊢\left(\phi \wedge n\in A\right)\to F\left(n\right)=\Re \left(F\left(n\right)\right)+\mathrm{i}\Im \left(F\left(n\right)\right)$$
8	7	mpteq2dva	$$⊢\phi \to \left(n\in A⟼F\left(n\right)\right)=\left(n\in A⟼\Re \left(F\left(n\right)\right)+\mathrm{i}\Im \left(F\left(n\right)\right)\right)$$
9	5 8	eqtrd	$$⊢\phi \to F=\left(n\in A⟼\Re \left(F\left(n\right)\right)+\mathrm{i}\Im \left(F\left(n\right)\right)\right)$$
10		fvexd	$$⊢\left(\phi \wedge n\in A\right)\to \Re \left(F\left(n\right)\right)\in \mathrm{V}$$
11		ovexd	$$⊢\left(\phi \wedge n\in A\right)\to \mathrm{i}\Im \left(F\left(n\right)\right)\in \mathrm{V}$$
12		ref	$$⊢\Re :ℂ⟶ℝ$$
13		resub	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \Re \left(F\left(k\right)-F\left(j\right)\right)=\Re \left(F\left(k\right)\right)-\Re \left(F\left(j\right)\right)$$
14	13	fveq2d	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \left|\Re \left(F\left(k\right)-F\left(j\right)\right)\right|=\left|\Re \left(F\left(k\right)\right)-\Re \left(F\left(j\right)\right)\right|$$
15		subcl	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to F\left(k\right)-F\left(j\right)\in ℂ$$
16		absrele	$$⊢F\left(k\right)-F\left(j\right)\in ℂ\to \left|\Re \left(F\left(k\right)-F\left(j\right)\right)\right|\le \left|F\left(k\right)-F\left(j\right)\right|$$
17	15 16	syl	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \left|\Re \left(F\left(k\right)-F\left(j\right)\right)\right|\le \left|F\left(k\right)-F\left(j\right)\right|$$
18	14 17	eqbrtrrd	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \left|\Re \left(F\left(k\right)\right)-\Re \left(F\left(j\right)\right)\right|\le \left|F\left(k\right)-F\left(j\right)\right|$$
19	1 2 3 4 12 18	caucvgrlem2	$$⊢\phi \to \left(n\in A⟼\Re \left(F\left(n\right)\right)\right)\underset{ℝ}{⇝}\underset{ℝ}{⇝}\left(\Re \circ F\right)$$
20		ax-icn	$$⊢\mathrm{i}\in ℂ$$
21	20	elexi	$$⊢\mathrm{i}\in \mathrm{V}$$
22	21	a1i	$$⊢\left(\phi \wedge n\in A\right)\to \mathrm{i}\in \mathrm{V}$$
23		fvexd	$$⊢\left(\phi \wedge n\in A\right)\to \Im \left(F\left(n\right)\right)\in \mathrm{V}$$
24		rlimconst	$$⊢\left(A\subseteq ℝ\wedge \mathrm{i}\in ℂ\right)\to \left(n\in A⟼\mathrm{i}\right)\underset{ℝ}{⇝}\mathrm{i}$$
25	1 20 24	sylancl	$$⊢\phi \to \left(n\in A⟼\mathrm{i}\right)\underset{ℝ}{⇝}\mathrm{i}$$
26		imf	$$⊢\Im :ℂ⟶ℝ$$
27		imsub	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \Im \left(F\left(k\right)-F\left(j\right)\right)=\Im \left(F\left(k\right)\right)-\Im \left(F\left(j\right)\right)$$
28	27	fveq2d	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \left|\Im \left(F\left(k\right)-F\left(j\right)\right)\right|=\left|\Im \left(F\left(k\right)\right)-\Im \left(F\left(j\right)\right)\right|$$
29		absimle	$$⊢F\left(k\right)-F\left(j\right)\in ℂ\to \left|\Im \left(F\left(k\right)-F\left(j\right)\right)\right|\le \left|F\left(k\right)-F\left(j\right)\right|$$
30	15 29	syl	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \left|\Im \left(F\left(k\right)-F\left(j\right)\right)\right|\le \left|F\left(k\right)-F\left(j\right)\right|$$
31	28 30	eqbrtrrd	$$⊢\left(F\left(k\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \left|\Im \left(F\left(k\right)\right)-\Im \left(F\left(j\right)\right)\right|\le \left|F\left(k\right)-F\left(j\right)\right|$$
32	1 2 3 4 26 31	caucvgrlem2	$$⊢\phi \to \left(n\in A⟼\Im \left(F\left(n\right)\right)\right)\underset{ℝ}{⇝}\underset{ℝ}{⇝}\left(\Im \circ F\right)$$
33	22 23 25 32	rlimmul	$$⊢\phi \to \left(n\in A⟼\mathrm{i}\Im \left(F\left(n\right)\right)\right)\underset{ℝ}{⇝}\mathrm{i}\underset{ℝ}{⇝}\left(\Im \circ F\right)$$
34	10 11 19 33	rlimadd	$$⊢\phi \to \left(n\in A⟼\Re \left(F\left(n\right)\right)+\mathrm{i}\Im \left(F\left(n\right)\right)\right)\underset{ℝ}{⇝}\left(\underset{ℝ}{⇝}\left(\Re \circ F\right)+\mathrm{i}\underset{ℝ}{⇝}\left(\Im \circ F\right)\right)$$
35	9 34	eqbrtrd	$$⊢\phi \to F\underset{ℝ}{⇝}\left(\underset{ℝ}{⇝}\left(\Re \circ F\right)+\mathrm{i}\underset{ℝ}{⇝}\left(\Im \circ F\right)\right)$$
36		rlimrel	$$⊢\mathrm{Rel}\underset{ℝ}{⇝}$$
37	36	releldmi	$$⊢F\underset{ℝ}{⇝}\left(\underset{ℝ}{⇝}\left(\Re \circ F\right)+\mathrm{i}\underset{ℝ}{⇝}\left(\Im \circ F\right)\right)\to F\in \mathrm{dom}\underset{ℝ}{⇝}$$
38	35 37	syl	$$⊢\phi \to F\in \mathrm{dom}\underset{ℝ}{⇝}$$