Theorem lmcau 7996

Description: Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of [Kreyszig] p. 28. Warning: The HTML proof page is 0.5MB in size.

Hypothesis

Ref	Expression
lmcau.1	|- P e. V

Assertion

Ref	Expression
lmcau	|- ((D e. Met /\ F(~~>m` D)P) -> F e. (Cau` D))

Proof of Theorem lmcau

Step	Hyp	Ref	Expression
1		halfpos2t 6037	. . . . . . . . . . . . 13 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
2	1	biimpd 153	. . . . . . . . . . . 12 |- (x e. RR -> (0 < x -> 0 < (x / 2)))
3	2	adantl 388	. . . . . . . . . . 11 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> (0 < x -> 0 < (x / 2)))
4		prth 556	. . . . . . . . . . . . . . . 16 |- (((j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))) -> ((j <_ k /\ j <_ m) -> (((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))))
5		simpll 412	. . . . . . . . . . . . . . . . . 18 |- ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (F` k) e. dom dom D)
6	5	a1i 8	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (F` k) e. dom dom D))
7		simprl 414	. . . . . . . . . . . . . . . . . 18 |- ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (F` m) e. dom dom D)
8	7	a1i 8	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (F` m) e. dom dom D))
9		lt2addt 5643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((F` k)DP) e. RR /\ ((F` m)DP) e. RR) /\ ((x / 2) e. RR /\ (x / 2) e. RR)) -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> (((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2))))
10		eqid 1475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- dom dom D = dom dom D
11	10	metcl 7811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((D e. Met /\ (F` k) e. dom dom D /\ P e. dom dom D) -> ((F` k)DP) e. RR)
12	11	3expb 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ ((F` k) e. dom dom D /\ P e. dom dom D)) -> ((F` k)DP) e. RR)
13	12	adantrlr 401	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> ((F` k)DP) e. RR)
14	10	metcl 7811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((D e. Met /\ (F` m) e. dom dom D /\ P e. dom dom D) -> ((F` m)DP) e. RR)
15	14	3expb 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ ((F` m) e. dom dom D /\ P e. dom dom D)) -> ((F` m)DP) e. RR)
16	15	adantrll 400	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> ((F` m)DP) e. RR)
17	13, 16	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> (((F` k)DP) e. RR /\ ((F` m)DP) e. RR))
18	17	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> (((F` k)DP) e. RR /\ ((F` m)DP) e. RR))
19		rehalfclt 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. RR -> (x / 2) e. RR)
20	19, 19	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. RR -> ((x / 2) e. RR /\ (x / 2) e. RR))
21	20	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((x / 2) e. RR /\ (x / 2) e. RR))
22	9, 18, 21	sylanc 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> (((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2))))
23		recnt 5313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. RR -> x e. CC)
24		2halvest 6039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. CC -> ((x / 2) + (x / 2)) = x)
25	23, 24	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. RR -> ((x / 2) + (x / 2)) = x)
26	25	breq2d 2630	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. RR -> ((((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2)) <-> (((F` k)DP) + ((F` m)DP)) < x))
27	26	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2)) <-> (((F` k)DP) + ((F` m)DP)) < x))
28	10	mettri3 7818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ P e. dom dom D)) -> ((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)))
29		id 59	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ P e. dom dom D) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ P e. dom dom D))
30	29	3expa 833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ P e. dom dom D))
31	28, 30	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> ((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)))
32	31	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)))
33		lelttrt 5523	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((F` k)D(F` m)) e. RR /\ (((F` k)DP) + ((F` m)DP)) e. RR /\ x e. RR) -> ((((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)) /\ (((F` k)DP) + ((F` m)DP)) < x) -> ((F` k)D(F` m)) < x))
34	10	metcl 7811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((D e. Met /\ (F` k) e. dom dom D /\ (F` m) e. dom dom D) -> ((F` k)D(F` m)) e. RR)
35	34	3expb 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((D e. Met /\ ((F` k) e. dom dom D /\ (F` m) e. dom dom D)) -> ((F` k)D(F` m)) e. RR)
36	35	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e.