Theorem hlimcaui 5141

Description: If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence.

Hypotheses

Ref	Expression
hlimcau.1	|- A e. V
hlimcau.2	|- F e. V
hlimcaui.4	|- F ~~>v A

Assertion

Ref	Expression
hlimcaui	|- F e. Cauchy

Proof of Theorem hlimcaui

Step	Hyp	Ref	Expression
1		hlimcaui.4	. . . 4 |- F ~~>v A
2		hlimcau.2	. . . . 5 |- F e. V
3		hlimcau.1	. . . . 5 |- A e. V
4	2, 3	hlimseq 5109	. . . 4 |- (F ~~>v A -> F:NN-->H~)
5	1, 4	ax-mp 6	. . 3 |- F:NN-->H~
6		breq2 2066	. . . . . . . . 9 |- (v = (x / 2) -> (0 < v <-> 0 < (x / 2)))
7		breq2 2066	. . . . . . . . . . . 12 |- (v = (x / 2) -> ((norm` ((F` z) -v A)) < v <-> (norm` ((F` z) -v A)) < (x / 2)))
8	7	imbi2d 464	. . . . . . . . . . 11 |- (v = (x / 2) -> ((y <_ z -> (norm` ((F` z) -v A)) < v) <-> (y <_ z -> (norm` ((F` z) -v A)) < (x / 2))))
9	8	biraldv 1219	. . . . . . . . . 10 |- (v = (x / 2) -> (A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < v) <-> A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < (x / 2))))
10	9	birexdv 1220	. . . . . . . . 9 |- (v = (x / 2) -> (E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < v) <-> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < (x / 2))))
11	6, 10	imbi12d 474	. . . . . . . 8 |- (v = (x / 2) -> ((0 < v -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < v)) <-> (0 < (x / 2) -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < (x / 2)))))
12	2, 3	hlimvec 5110	. . . . . . . . . 10 |- (F ~~>v A -> A e. H~)
13	1, 12	ax-mp 6	. . . . . . . . 9 |- A e. H~
14		hlim2 5112	. . . . . . . . . 10 |- ((F:NN-->H~ /\ A e. H~) -> (F ~~>v A <-> A.v e. RR (0 < v -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < v))))
15	1, 14	mpbii 168	. . . . . . . . 9 |- ((F:NN-->H~ /\ A e. H~) -> A.v e. RR (0 < v -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < v)))
16	5, 13, 15	mp2an 520	. . . . . . . 8 |- A.v e. RR (0 < v -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < v))
17	11, 16	vtoclri 1393	. . . . . . 7 |- ((x / 2) e. RR -> (0 < (x / 2) -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < (x / 2))))
18		opreq1 3006	. . . . . . . . . 10 |- (x = if(x e. RR, x, 0) -> (x / 2) = (if(x e. RR, x, 0) / 2))
19	18	eleq1d 1155	. . . . . . . . 9 |- (x = if(x e. RR, x, 0) -> ((x / 2) e. RR <-> (if(x e. RR, x, 0) / 2) e. RR))
20		ax0re 4063	. . . . . . . . . . 11 |- 0 e. RR
21	20	elimel 1793	. . . . . . . . . 10 |- if(x e. RR, x, 0) e. RR
22		2re 4470	. . . . . . . . . 10 |- 2 e. RR
23		2pos 4479	. . . . . . . . . . 11 |- 0 < 2
24	22, 23	gt0ne0i 4345	. . . . . . . . . 10 |- 2 =/= 0
25	21, 22, 24	redivcl 4274	. . . . . . . . 9 |- (if(x e. RR, x, 0) / 2) e. RR
26	19, 25	dedth 1784	. . . . . . . 8 |- (x e. RR -> (x / 2) e. RR)
27	26	adantr 306	. . . . . . 7 |- ((x e. RR /\ 0 < x) -> (x / 2) e. RR)
28		breq2 2066	. . . . . . . . . 10 |- (x = if(x e. RR, x, 0) -> (0 < x <-> 0 < if(x e. RR, x, 0)))
29	18	breq2d 2072	. . . . . . . . . 10 |- (x = if(x e. RR, x, 0) -> (0 < (x / 2) <-> 0 < (if(x e. RR, x, 0) / 2)))
30	28, 29	imbi12d 474	. . . . . . . . 9 |- (x = if(x e. RR, x, 0) -> ((0 < x -> 0 < (x / 2)) <-> (0 < if(x e. RR, x, 0) -> 0 < (if(x e. RR, x, 0) / 2))))
31	21, 22, 23	divgt0lem 4389	. . . . . . . . 9 |- (0 < if(x e. RR, x, 0) -> 0 < (if(x e. RR, x, 0) / 2))
32	30, 31	dedth 1784	. . . . . . . 8 |- (x e. RR -> (0 < x -> 0 < (x / 2)))
33	32	imp 277	. . . . . . 7 |- ((x e. RR /\ 0 < x) -> 0 < (x / 2))
34	17, 27, 33	sylc 62	. . . . . 6 |- ((x e. RR /\ 0 < x) -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < (x / 2)))
35		prth 429	. . . . . . . . . . . 12 |- (((y <_ z -> (norm` ((F` z) -v A)) < (x / 2)) /\ (y <_ w -> (norm` ((F` w) -v A)) < (x / 2))) -> ((y <_ z /\ y <_ w) -> ((norm` ((F` z) -v A)) < (x / 2) /\ (norm` ((F` w) -v A)) < (x / 2))))
36		normsubt 5091	. . . . . . . . . . . . . . . . 17 |- ((A e. H~ /\ (F` w) e. H~) -> (norm` (A -v (F` w))) = (norm` ((F` w) -v A)))
37	36	breq1d 2071	. . . . . . . . . . . . . . . 16 |- ((A e. H~ /\ (F` w) e. H~) -> ((norm` (A -v (F` w))) < (x / 2) <-> (norm` ((F` w) -v A)) < (x / 2)))
38	37	anbi2d 468	. . . . . . . . . . . . . . 15 |- ((A e. H~ /\ (F` w) e. H~) -> (((norm` ((F` z) -v A)) < (x / 2) /\ (norm` (A -v (F` w))) < (x / 2)) <-> ((norm` ((F` z) -v A)) < (x / 2) /\ (norm` ((F` w) -v A)) < (x / 2))))
39	38	adantl 305	. . . . . . . . . . . . . 14 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((norm` ((F` z) -v A)) < (x / 2) /\ (norm` (A -v (F` w))) < (x / 2)) <-> ((norm` ((F` z) -v A)) < (x / 2) /\ (norm` ((F` w) -v A)) < (x / 2))))
40		ffvrn 2890	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:NN-->H~ /\ z e. NN) -> (F` z) e. H~)
41	5, 40	mpan 518	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. NN -> (F` z) e. H~)
42	41	anim1i 269	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. NN /\ (F` w) e. H~) -> ((F` z) e. H~ /\ (F` w) e. H~))
43	42	ancoms 334	. . . . . . . . . . . . . . . . . . 19 |- (((F` w) e. H~ /\ z e. NN) -> ((F` z) e. H~ /\ (F` w) e. H~))
44	43	anim1i 269	. . . . . . . . . . . . . . . . . 18 |- ((((F` w) e. H~ /\ z e. NN) /\ (A e. H~ /\ x e. RR)) -> (((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)))
45	44	ancoms 334	. . . . . . . . . . . . . . . . 17 |- (((A e. H~ /\ x e. RR) /\ ((F` w) e. H~ /\ z e. NN)) -> (((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)))
46	45	an4s 390	. . . . . . . . . . . . . . . 16 |- (((A e. H~ /\ (F` w) e. H~) /\ (x e. RR /\ z e. NN)) -> (((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)))
47	46	ancoms 334	. . . . . . . . . . . . . . 15 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)))
48		norm3lemt 5097	. . . . . . . . . . . . . . 15 |- ((((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)) -> (((norm` ((F` z) -v A)) < (x / 2) /\ (norm` (A -v (F` w))) < (x / 2)) -> (norm` ((F` z) -v (F` w))) < x))
49	47, 48	syl 12	. . . . . . . . . . . . . 14 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((norm` ((F` z) -v A)) < (x / 2) /\ (norm` (A -v (F` w))) < (x / 2)) -> (norm` ((F` z) -v (F` w))) < x))
50	39, 49	sylbird 180	. . . . . . . . . . . . 13 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((norm` ((F` z) -v A)) < (x / 2) /\ (norm` ((F` w) -v A)) < (x / 2)) -> (norm` ((F` z) -v (F` w))) < x))
51		ffvrn 2890	. . . . . . . . . . . . . . 15 |- (