Theorem caubnd 6871

Description: A Cauchy sequence of complex numbers is bounded.

Hypotheses

Ref	Expression
caubnd.1	|- F:NN-->CC
caubnd.2	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))

Assertion

Ref	Expression
caubnd	|- E.x e. RR A.y e. NN (abs` (F` y)) < x

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

Proof of Theorem caubnd

Step	Hyp	Ref	Expression
1		lt01 5661	. . . 4 |- 0 < 1
2		1re 5415	. . . . 5 |- 1 e. RR
3		caubnd.2	. . . . 5 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
4		breq2 2618	. . . . . . 7 |- (z = 1 -> (0 < z <-> 0 < 1))
5		breq2 2618	. . . . . . . . 9 |- (z = 1 -> ((abs` ((F` y) - (F` w))) < z <-> (abs` ((F` y) - (F` w))) < 1))
6	5	imbi2d 611	. . . . . . . 8 |- (z = 1 -> ((w < y -> (abs` ((F` y) - (F` w))) < z) <-> (w < y -> (abs` ((F` y) - (F` w))) < 1)))
7	6	rexralbidv 1679	. . . . . . 7 |- (z = 1 -> (E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z) <-> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < 1)))
8	4, 7	imbi12d 625	. . . . . 6 |- (z = 1 -> ((0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z)) <-> (0 < 1 -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < 1))))
9	8	rcla4v 1869	. . . . 5 |- (1 e. RR -> (A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z)) -> (0 < 1 -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < 1))))
10	2, 3, 9	mp2 43	. . . 4 |- (0 < 1 -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < 1))
11	1, 10	ax-mp 7	. . 3 |- E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < 1)
12		ltadd1t 5605	. . . . . . . . . . . 12 |- (((abs` ((F` y) - (F` w))) e. RR /\ 1 e. RR /\ (abs` (F` w)) e. RR) -> ((abs` ((F` y) - (F` w))) < 1 <-> ((abs` ((F` y) - (F` w))) + (abs` (F` w))) < (1 + (abs` (F` w)))))
13	2, 12	mp3an2 902	. . . . . . . . . . 11 |- (((abs` ((F` y) - (F` w))) e. RR /\ (abs` (F` w)) e. RR) -> ((abs` ((F` y) - (F` w))) < 1 <-> ((abs` ((F` y) - (F` w))) + (abs` (F` w))) < (1 + (abs` (F` w)))))
14		subclt 5347	. . . . . . . . . . . . 13 |- (((F` y) e. CC /\ (F` w) e. CC) -> ((F` y) - (F` w)) e. CC)
15		caubnd.1	. . . . . . . . . . . . . 14 |- F:NN-->CC
16	15	ffvelrni 3806	. . . . . . . . . . . . 13 |- (y e. NN -> (F` y) e. CC)
17	15	ffvelrni 3806	. . . . . . . . . . . . 13 |- (w e. NN -> (F` w) e. CC)
18	14, 16, 17	syl2an 454	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> ((F` y) - (F` w)) e. CC)
19		absclt 6776	. . . . . . . . . . . 12 |- (((F` y) - (F` w)) e. CC -> (abs` ((F` y) - (F` w))) e. RR)
20	18, 19	syl 10	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN) -> (abs` ((F` y) - (F` w))) e. RR)
21		absclt 6776	. . . . . . . . . . . . 13 |- ((F` w) e. CC -> (abs` (F` w)) e. RR)
22	17, 21	syl 10	. . . . . . . . . . . 12 |- (w e. NN -> (abs` (F` w)) e. RR)
23	22	adantl 388	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN) -> (abs` (F` w)) e. RR)
24	13, 20, 23	sylanc 471	. . . . . . . . . 10 |- ((y e. NN /\ w e. NN) -> ((abs` ((F` y) - (F` w))) < 1 <-> ((abs` ((F` y) - (F` w))) + (abs` (F` w))) < (1 + (abs` (F` w)))))
25		npcant 5379	. . . . . . . . . . . . . 14 |- (((F` y) e. CC /\ (F` w) e. CC) -> (((F` y) - (F` w)) + (F` w)) = (F` y))
26	25, 16, 17	syl2an 454	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> (((F` y) - (F` w)) + (F` w)) = (F` y))
27	26	fveq2d 3719	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` (((F` y) - (F` w)) + (F` w))) = (abs` (F` y)))
28		abstrit 6843	. . . . . . . . . . . . 13 |- ((((F` y) - (F` w)) e. CC /\ (F` w) e. CC) -> (abs` (((F` y) - (F` w)) + (F` w))) <_ ((abs` ((F` y) - (F` w))) + (abs` (F` w))))
29	17	adantl 388	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> (F` w) e. CC)
30	28, 18, 29	sylanc 471	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` (((F` y) - (F` w)) + (F` w))) <_ ((abs` ((F` y) - (F` w))) + (abs` (F` w))))
31	27, 30	eqbrtrrd 2632	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN) -> (abs` (F` y)) <_ ((abs` ((F` y) - (F` w))) + (abs` (F` w))))
32		lelttrt 5504	. . . . . . . . . . . 12 |- (((abs` (F` y)) e. RR /\ ((abs` ((F` y) - (F` w))) + (abs` (F` w))) e. RR /\ (1 + (abs` (F` w))) e. RR) -> (((abs` (F` y)) <_ ((abs` ((F` y) - (F` w))) + (abs` (F` w))) /\ ((abs` ((F` y) - (F` w))) + (abs` (F` w))) < (1 + (abs` (F` w)))) -> (abs` (F` y)) < (1 + (abs` (F` w)))))
33		absclt 6776	. . . . . . . . . . . . . 14 |- ((F` y) e. CC -> (abs` (F` y)) e. RR)
34	16, 33	syl 10	. . . . . . . . . . . . 13 |- (y e. NN -> (abs` (F` y)) e. RR)
35	34	adantr 389	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` (F` y)) e. RR)
36		axaddrcl 5252	. . . . . . . . . . . . 13 |- (((abs` ((F` y) - (F` w))) e. RR /\ (abs` (F` w)) e. RR) -> ((abs` ((F` y) - (F` w))) + (abs` (F` w))) e. RR)
37	36, 20, 23	sylanc 471	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> ((abs` ((F` y) - (F` w))) + (abs` (F` w))) e. RR)
38		axaddrcl 5252	. . . . . . . . . . . . . . 15 |- ((1 e. RR /\ (abs` (F` w)) e. RR) -> (1 + (abs` (F` w))) e. RR)
39	2, 38	mpan 694	. . . . . . . . . . . . . 14 |- ((abs` (F` w)) e. RR -> (1 + (abs` (F` w))) e. RR)
40	22, 39	syl 10	. . . . . . . . . . . . 13 |- (w e. NN -> (1 + (abs` (F` w))) e. RR)
41	40	adantl 388	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (1 + (abs` (F` w))) e. RR)
42	32, 35, 37, 41	syl3anc 857	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN) -> (((abs` (F` y)) <_ ((abs` ((F` y) - (F` w))) + (abs` (F` w))) /\ ((abs` ((F` y) - (F` w))) + (abs` (F` w))) < (1 + (abs` (F` w)))) -> (abs` (F` y)) < (1 + (abs` (F` w)))))
43	31, 42	mpand 700	. . . . . . . . . 10 |- ((y e. NN /\ w e. NN) -> (((abs` ((F` y) - (F` w))) +