Theorem caucvg3t 7168

Description: A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). Warning: The HTML proof page is 0.6 megabyte in size.

Assertion

Ref	Expression
caucvg3t	|- ((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))) -> E.x e. CC F ~~> x)

Distinct variable group:   x,w,y,z,F

Proof of Theorem caucvg3t

Step	Hyp	Ref	Expression
1		breq1 2622	. . 3 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> (F ~~> x <-> if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) ~~> x))
2	1	rexbidv 1664	. 2 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> (E.x e. CC F ~~> x <-> E.x e. CC if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) ~~> x))
3		feq1 3620	. . . . . 6 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> (F:NN-->CC <-> if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})):NN-->CC))
4		fveq1 3723	. . . . . . . . . . . . . 14 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> (F` u) = (if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` u))
5		fveq1 3723	. . . . . . . . . . . . . 14 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> (F` t) = (if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` t))
6	4, 5	opreq12d 3978	. . . . . . . . . . . . 13 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> ((F` u) - (F` t)) = ((if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` u) - (if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` t)))
7	6	fveq2d 3728	. . . . . . . . . . . 12 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> (abs` ((F` u) - (F` t))) = (abs` ((if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` u) - (if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` t))))
8	7	breq1d 2629	. . . . . . . . . . 11 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> ((abs` ((F` u) - (F` t))) < v <-> (abs` ((if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` u) - (if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` t))) < v))
9	8	imbi2d 612	. . . . . . . . . 10 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> ((t <_ u -> (abs` ((F` u) - (F` t))) < v) <-> (t <_ u -> (abs` ((if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` u) - (if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` t))) < v)))
10	9	rexralbidv 1682	. . . . . . . . 9 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> (E.t e. NN A.u e. NN (t <_ u -> (abs` ((F` u) - (F` t))) < v) <-> E.t e. NN A.u e. NN (t <_ u -> (abs` ((if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` u) - (if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` t))) < v)))
11	10	imbi2d 612	. . . . . . . 8 |- (F = if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0})) -> ((0 < v -> E.t e. NN A.u e. NN (t <_ u -> (abs` ((F` u) - (F` t))) < v)) <-> (0 < v -> E.t e. NN A.u e. NN (t <_ u -> (abs` ((if((F:NN-->CC /\ A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w <_ y -> (abs` ((F` y) - (F` w))) < z))), F, (NN X. {0}))` u) - (if((F:NN-->CC /\ A.z