Theorem hcau2 8976

Description: Alternate representation of a Hilbert space Cauchy sequence.

Assertion

Ref	Expression
hcau2	|- (F e. Cauchy <-> (F:NN-->H~ /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((F` k) -h (F` j))) < x))))

Distinct variable group:   j,k,x,F

Proof of Theorem hcau2

Step	Hyp	Ref	Expression
1		hcau 8972	. 2 |- (F e. Cauchy <-> (F:NN-->H~ /\ A.x e. RR (0 < x -> E.m e. NN A.j e. NN A.k e. NN ((m <_ j /\ m <_ k) -> (normh` ((F` j) -h (F` k))) < x))))
2		normsubt 8931	. . . . . . . . . . . . 13 |- (((F` j) e. H~ /\ (F` k) e. H~) -> (normh` ((F` j) -h (F` k))) = (normh` ((F` k) -h (F` j))))
3		ffvelrn 3799	. . . . . . . . . . . . 13 |- ((F:NN-->H~ /\ j e. NN) -> (F` j) e. H~)
4		ffvelrn 3799	. . . . . . . . . . . . 13 |- ((F:NN-->H~ /\ k e. NN) -> (F` k) e. H~)
5	2, 3, 4	syl2an 454	. . . . . . . . . . . 12 |- (((F:NN-->H~ /\ j e. NN) /\ (F:NN-->H~ /\ k e. NN)) -> (normh` ((F` j) -h (F` k))) = (normh` ((F` k) -h (F` j))))
6	5	anandis 511	. . . . . . . . . . 11 |- ((F:NN-->H~ /\ (j e. NN /\ k e. NN)) -> (normh` ((F` j) -h (F` k))) = (normh` ((F` k) -h (F` j))))
7	6	anassrs 441	. . . . . . . . . 10 |- (((F:NN-->H~ /\ j e. NN) /\ k e. NN) -> (normh` ((F` j) -h (F` k))) = (normh` ((F` k) -h (F` j))))
8	7	breq1d 2619	. . . . . . . . 9 |- (((F:NN-->H~ /\ j e. NN) /\ k e. NN) -> ((normh` ((F` j) -h (F` k))) < x <-> (normh` ((F` k) -h (F` j))) < x))
9	8	imbi2d 610	. . . . . . . 8 |- (((F:NN-->H~ /\ j e. NN) /\ k e. NN) -> ((j <_ k -> (normh` ((F` j) -h (F` k))) < x) <-> (j <_ k -> (normh` ((F` k) -h (F` j))) < x)))
10	9	ralbidva 1651	. . . . . . 7 |- ((F:NN-->H~ /\ j e. NN) -> (A.k e. NN (j <_ k -> (normh` ((F` j) -h (F` k))) < x) <-> A.k e. NN (j <_ k -> (normh` ((F` k) -h (F` j))) < x)))
11	10	rexbidva 1652	. . . . . 6 |- (F:NN-->H~ -> (E.j e. NN A.k e. NN (j <_ k -> (normh` ((F` j) -h (F` k))) < x) <-> E.j e. NN A.k e. NN (j <_ k -> (normh` ((F` k) -h (F` j))) < x)))
12	11	imbi2d 610	. . . . 5 |- (F:NN-->H~ -> ((0 < x -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((F` j) -h (F` k))) < x)) <-> (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((F` k) -h (F` j))) < x))))
13	12	ralbidv 1655	. . . 4 |- (F:NN-->H~ -> (A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((F` j) -h (F` k))) < x)) <-> A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((F` k) -h (F` j))) < x))))
14		fveq2 3709	. . . . . . . 8 |- (k = m -> (F` k) = (F` m))
15	14	opreq2d 3961	. . . . . . 7 |- (k = m -> ((F` j) -h (F` k)) = ((F` j) -h (F` m)))
16	15	fveq2d 3713	. . . . . 6 |- (k = m -> (normh` ((F` j) -h (F` k))) = (normh` ((F` j) -h (F` m))))
17	16	breq1d 2619	. . . . 5 |- (k = m -> ((normh` ((F` j) -h (F` k))) < x <-> (normh` ((F` j) -h (F` m))) < x))
18		fveq2 3709	. . . . . . . 8 |- (j = k -> (F` j) = (F` k))
19	18	opreq1d 3960	. . . . . . 7 |- (j = k -> ((F` j) -h (F` m)) = ((F` k) -h (F` m)))
20	19	fveq2d 3713	. . . . . 6 |- (j = k -> (normh` ((F` j) -h (F` m))) = (normh` ((F` k) -h (F` m))))
21	20	breq1d 2619	. . . . 5 |- (j = k -> ((normh` ((F` j) -h (F` m))) < x <-> (normh` ((F` k) -h (F` m))) < x))
22		breq2 2613	. . . . . 6 |- (x = (y / 2) -> ((normh` ((F` j) -h (F` k))) < x <-> (normh` ((F` j) -h (F` k))) < (y / 2)))
23		breq2 2613	. . . . . 6 |- (x = (y / 2) -> ((normh` ((F` j) -h (F` m))) < x <-> (normh` ((F` j) -h (F` m))) < (y / 2)))
24	22, 23	anbi12d 626	. . . . 5 |- (x = (y / 2) -> (((normh` ((F` j) -h (F` k))) < x /\ (normh` ((F` j) -h (F` m))) < x) <-> ((normh` ((F` j) -h (F` k))) < (y / 2) /\ (normh` ((F` j) -h (F` m))) < (y / 2))))
25		breq2 2613	. . . . 5 |- (x = y -> ((normh` ((F` k) -h (F` m))) < x <-> (normh` ((F` k) -h (F` m))) < y))
26		lt2halvest 5989	. . . . . . . . 9 |- (((normh` ((F` j) -h (F` k))) e. RR /\ (normh` ((F` j) -h (F` m))) e. RR /\ y e. RR) -> (((normh` ((F` j) -h (F` k))) < (y / 2) /\ (normh` ((F` j) -h (F` m))) < (y / 2)) -> ((normh` ((F` j) -h (F` k))) + (normh` ((F` j) -h (F` m)))) < y))
27		hvsubclt 8808	. . . . . . . . . . . . 13 |- (((F` j) e. H~ /\ (F` k) e. H~) -> ((F` j) -h (F` k)) e. H~)
28	27	ancoms 436	. . . . . . . . . . . 12 |- (((F` k) e. H~ /\ (F` j) e. H~) -> ((F` j) -h (F` k)) e. H~)
29		normclt 8912	. . . . . . . . . . . 12 |- (((F` j) -h (F` k)) e. H~ -> (normh` ((F` j) -h (F` k))) e. RR)
30	28, 29	syl 10	. . . . . . . . . . 11 |- (((F` k) e. H~ /\ (F` j) e. H~) -> (normh` ((F` j) -h (F` k))) e. RR)
31	30	3adant2 796	. . . . . . . . . 10 |- (((F` k) e. H~ /\ (F` m) e. H~ /\ (F` j) e. H~) -> (normh` ((F` j) -h (F` k))) e. RR)
32	31	adantr 389	. . . . . . . . 9 |- ((((F` k) e. H~ /\ (F` m) e. H~ /\ (F` j) e. H~) /\ y e. RR) -> (normh` ((F` j) -h (F` k))) e. RR)
33		hvsubclt 8808	. . . . . . . . . . . . 13 |- (((F` j) e. H~ /\ (F` m) e. H~) -> ((F` j) -h (F` m)) e. H~)
34	33	ancoms 436	. . . . . . . . . . . 12 |- (((F` m) e. H~ /\ (F` j) e. H~) -> ((F` j) -h (F` m)) e. H~)
35		normclt 8912	. . . . . . . . . . . 12 |- (((F` j) -h (F` m)) e. H~ -> (normh` ((F` j) -h (F` m))) e. RR)
36	34, 35	syl 10	. . . . . . . . . . 11 |- (((F` m) e. H~ /\ (F` j) e. H~) -> (normh` ((F` j) -h (F` m))) e. RR)
37	36	3adant1 795	. . . . . . . . . 10 |- (((F` k) e. H~ /\ (F` m) e. H~ /\ (F` j) e. H~) -> (normh` ((F` j) -h (F` m))) e. RR)
38	37	adantr 389	. . . . . . . . 9 |- ((((F` k) e. H~ /\ (F` m) e. H~ /\ (F` j) e. H~) /\ y e. RR) -> (normh` ((F` j) -h (F` m))) e. RR)
39		pm3.27 323	. . . . . . . . 9 |- ((((F` k) e. H~ /\ (F` m) e. H~