Theorem hlimcaui 9027

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		hcau 8972	. 2 |- (F e. Cauchy <-> (F:NN-->H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((F` z) -h (F` w))) < x))))
2		hlimcaui.4	. . 3 |- F ~~>v A
3		hlimcau.2	. . . 4 |- F e. V
4		hlimcau.1	. . . 4 |- A e. V
5	3, 4	hlimseq 8978	. . 3 |- (F ~~>v A -> F:NN-->H~)
6	2, 5	ax-mp 7	. 2 |- F:NN-->H~
7		breq2 2613	. . . . . . . 8 |- (v = (x / 2) -> (0 < v <-> 0 < (x / 2)))
8		breq2 2613	. . . . . . . . . 10 |- (v = (x / 2) -> ((normh` ((F` z) -h A)) < v <-> (normh` ((F` z) -h A)) < (x / 2)))
9	8	imbi2d 610	. . . . . . . . 9 |- (v = (x / 2) -> ((y <_ z -> (normh` ((F` z) -h A)) < v) <-> (y <_ z -> (normh` ((F` z) -h A)) < (x / 2))))
10	9	rexralbidv 1674	. . . . . . . 8 |- (v = (x / 2) -> (E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v) <-> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < (x / 2))))
11	7, 10	imbi12d 624	. . . . . . 7 |- (v = (x / 2) -> ((0 < v -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v)) <-> (0 < (x / 2) -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < (x / 2)))))
12	3, 4	hlimvec 8979	. . . . . . . . 9 |- (F ~~>v A -> A e. H~)
13	2, 12	ax-mp 7	. . . . . . . 8 |- A e. H~
14		hlim2 8981	. . . . . . . . 9 |- ((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 -> (normh` ((F` z) -h A)) < v))))
15	2, 14	mpbii 193	. . . . . . . 8 |- ((F:NN-->H~ /\ A e. H~) -> A.v e. RR (0 < v -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v)))
16	6, 13, 15	mp2an 695	. . . . . . 7 |- A.v e. RR (0 < v -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v))
17	11, 16	vtoclri 1850	. . . . . 6 |- ((x / 2) e. RR -> (0 < (x / 2) -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < (x / 2))))
18		rehalfclt 5981	. . . . . . 7 |- (x e. RR -> (x / 2) e. RR)
19	18	adantr 389	. . . . . 6 |- ((x e. RR /\ 0 < x) -> (x / 2) e. RR)
20		breq2 2613	. . . . . . . . 9 |- (x = if(x e. RR, x, 0) -> (0 < x <-> 0 < if(x e. RR, x, 0)))
21		opreq1 3953	. . . . . . . . . 10 |- (x = if(x e. RR, x, 0) -> (x / 2) = (if(x e. RR, x, 0) / 2))
22	21	breq2d 2620	. . . . . . . . 9 |- (x = if(x e. RR, x, 0) -> (0 < (x / 2) <-> 0 < (if(x e. RR, x, 0) / 2)))
23	20, 22	imbi12d 624	. . . . . . . 8 |- (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))))
24		0re 5412	. . . . . . . . . 10 |- 0 e. RR
25	24	elimel 2384	. . . . . . . . 9 |- if(x e. RR, x, 0) e. RR
26		2re 5926	. . . . . . . . 9 |- 2 e. RR
27		2pos 5936	. . . . . . . . 9 |- 0 < 2
28	25, 26, 27	divgt0i2 5813	. . . . . . . 8 |- (0 < if(x e. RR, x, 0) -> 0 < (if(x e. RR, x, 0) / 2))
29	23, 28	dedth 2373	. . . . . . 7 |- (x e. RR -> (0 < x -> 0 < (x / 2)))
30	29	imp 350	. . . . . 6 |- ((x e. RR /\ 0 < x) -> 0 < (x / 2))
31	17, 19, 30	sylc 68	. . . . 5 |- ((x e. RR /\ 0 < x) -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < (x / 2)))
32		prth 554	. . . . . . . . . . 11 |- (((y <_ z -> (normh` ((F` z) -h A)) < (x / 2)) /\ (y <_ w -> (normh` ((F` w) -h A)) < (x / 2))) -> ((y <_ z /\ y <_ w) -> ((normh` ((F` z) -h A)) < (x / 2) /\ (normh` ((F` w) -h A)) < (x / 2))))
33		normsubt 8931	. . . . . . . . . . . . . . . 16 |- ((A e. H~ /\ (F` w) e. H~) -> (normh` (A -h (F` w))) = (normh` ((F` w) -h A)))
34	33	breq1d 2619	. . . . . . . . . . . . . . 15 |- ((A e. H~ /\ (F` w) e. H~) -> ((normh` (A -h (F` w))) < (x / 2) <-> (normh` ((F` w) -h A)) < (x / 2)))
35	34	anbi2d 614	. . . . . . . . . . . . . 14 |- ((A e. H~ /\ (F` w) e. H~) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` (A -h (F` w))) < (x / 2)) <-> ((normh` ((F` z) -h A)) < (x / 2) /\ (normh` ((F` w) -h A)) < (x / 2))))
36	35	adantl 388	. . . . . . . . . . . . 13 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` (A -h (F` w))) < (x / 2)) <-> ((normh` ((F` z) -h A)) < (x / 2) /\ (normh` ((F` w) -h A)) < (x / 2))))
37	6	ffvelrni 3800	. . . . . . . . . . . . . . . . . . . 20 |- (z e. NN -> (F` z) e. H~)
38	37	anim1i 334	. . . . . . . . . . . . . . . . . . 19 |- ((z e. NN /\ (F` w) e. H~) -> ((F` z) e. H~ /\ (F` w) e. H~))
39	38	ancoms 436	. . . . . . . . . . . . . . . . . 18 |- (((F` w) e. H~ /\ z e. NN) -> ((F` z) e. H~ /\ (F` w) e. H~))
40	39	anim1i 334	. . . . . . . . . . . . . . . . 17 |- ((((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)))
41	40	ancoms 436	. . . . . . . . . . . . . . . 16 |- (((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)))
42	41	an4s 507	. . . . . . . . . . . . . . 15 |- (((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)))
43	42	ancoms 436	. . . . . . . . . . . . . 14 |- (((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)))
44		norm3lemt 8940	. . . . . . . . . . . . . 14 |- ((((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` (A -h (F` w))) < (x / 2)) -> (normh` ((F` z) -h (F` w))) < x))
45	43, 44	syl 10	. . . . . . . . . . . . 13 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` (A -h (F` w))) < (x / 2)) -> (normh` ((F` z) -h (F` w))) < x))
46	36, 45	sylbird 205	. . . . . . . . . . . 12 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` ((F` w) -h A)) < (x / 2)) -> (normh` ((F` z) -h (F` w))) < x))
47	6	ffvelrni 3800	. . . . . . . . . . . . 13 |- (w e. NN -> (F` w) e. H~)
48	47, 13	jctil 292	. . . . . . . . . . . 12 |- (w e. NN -> (A e. H~ /\ (F` w) e. H~))
49	46, 48	sylan2 451	. . . . . . . . . . 11 |- (((x