Theorem iscau4 7937

Description: Express the property "F is a Cauchy sequence of metric D."

Hypothesis

Ref	Expression
lmbr.1	|- X = dom dom D

Assertion

Ref	Expression
iscau4	|- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))))

Distinct variable groups:   j,k,x,F   D,j,k,x   j,X,k,x

Proof of Theorem iscau4

Step	Hyp	Ref	Expression
1		lmbr.1	. . 3 |- X = dom dom D
2	1	iscau 7933	. 2 |- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.m e. ZZ A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))))
3		fveq2 3730	. . . . . 6 |- (k = m -> (F` k) = (F` m))
4	3	eleq1d 1543	. . . . 5 |- (k = m -> ((F` k) e. X <-> (F` m) e. X))
5	3	opreq2d 3982	. . . . . 6 |- (k = m -> ((F` j)D(F` k)) = ((F` j)D(F` m)))
6	5	breq1d 2634	. . . . 5 |- (k = m -> (((F` j)D(F` k)) < x <-> ((F` j)D(F` m)) < x))
7	4, 6	3anbi23d 898	. . . 4 |- (k = m -> (((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x) <-> ((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < x)))
8		fveq2 3730	. . . . . 6 |- (j = k -> (F` j) = (F` k))
9	8	eleq1d 1543	. . . . 5 |- (j = k -> ((F` j) e. X <-> (F` k) e. X))
10	8	opreq1d 3981	. . . . . 6 |- (j = k -> ((F` j)D(F` m)) = ((F` k)D(F` m)))
11	10	breq1d 2634	. . . . 5 |- (j = k -> (((F` j)D(F` m)) < x <-> ((F` k)D(F` m)) < x))
12	9, 11	3anbi13d 897	. . . 4 |- (j = k -> (((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < x) <-> ((F` k) e. X /\ (F` m) e. X /\ ((F` k)D(F` m)) < x)))
13		breq2 2628	. . . . . 6 |- (x = (y / 2) -> (((F` j)D(F` k)) < x <-> ((F` j)D(F` k)) < (y / 2)))
14	13	3anbi3d 901	. . . . 5 |- (x = (y / 2) -> (((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x) <-> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < (y / 2))))
15		breq2 2628	. . . . . 6 |- (x = (y / 2) -> (((F` j)D(F` m)) < x <-> ((F` j)D(F` m)) < (y / 2)))
16	15	3anbi3d 901	. . . . 5 |- (x = (y / 2) -> (((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < x) <-> ((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < (y / 2))))
17	14, 16	anbi12d 630	. . . 4 |- (x = (y / 2) -> ((((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x) /\ ((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < x)) <-> (((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < (y / 2)) /\ ((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < (y / 2)))))
18		breq2 2628	. . . . 5 |- (x = y -> (((F` k)D(F` m)) < x <-> ((F` k)D(F` m)) < y))
19	18	3anbi3d 901	. . . 4 |- (x = y -> (((F` k) e. X /\ (F` m) e. X /\ ((F` k)D(F` m)) < x) <-> ((F` k) e. X /\ (F` m) e. X /\ ((F` k)D(F` m)) < y)))
20		3simp2 791	. . . . . . . 8 |- (((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < (y / 2)) -> (F` k) e. X)
21	20	adantr 391	. . . . . . 7 |- ((((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < (y / 2)) /\ ((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < (y / 2))) -> (F` k) e. X)
22	21	a1i 8	. . . . . 6 |- ((D e. Met /\ y e. RR) -> ((((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < (y / 2)) /\ ((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < (y / 2))) -> (F` k) e. X))
23		3simp2 791	. . . . . . . 8 |- (((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < (y / 2)) -> (F` m) e. X)
24	23	adantl 390	. . . . . . 7 |- ((((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < (y / 2)) /\ ((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < (y / 2))) -> (F` m) e. X)
25	24	a1i 8	. . . . . 6 |- ((D e. Met /\ y e. RR) -> ((((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < (y / 2)) /\ ((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < (y / 2))) -> (F` m) e. X))
26		lt2halvest 6044	. . . . . . . . . . . 12 |- ((((F` j)D(F` k)) e. RR /\ ((F` j)D(F` m)) e. RR /\ y e. RR) -> ((((F` j)D(F` k)) < (y / 2) /\ ((F` j)D(F` m)) < (y / 2)) -> (((F` j)D(F` k)) + ((F` j)D(F` m))) < y))
27	1	metcl 7808	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ (F` j) e. X /\ (F` k) e. X) -> ((F` j)D(F` k)) e. RR)
28	27	3expb 836	. . . . . . . . . . . . . 14 |- ((D e. Met /\ ((F` j) e. X /\ (F` k) e. X)) -> ((F` j)D(F` k)) e. RR)
29	28	adantlr 395	. . . . . . . . . . . . 13 |- (((D e. Met /\ y e. RR) /\ ((F` j) e. X /\ (F` k) e. X)) -> ((F` j)D(F` k)) e. RR)
30	29	adantrrr 405	. . . . . . . . . . . 12 |- (((D e. Met /\ y e. RR) /\ ((F` j) e. X /\ ((F` k) e. X /\ (F` m) e. X))) -> ((F` j)D(F` k)) e. RR)
31	1	metcl 7808	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ (F` j) e. X /\ (F` m) e. X) -> ((F` j)D(F` m)) e. RR)
32	31	3expb 836	. . . . . . . . . . . . . 14 |- ((D e. Met /\ ((F` j) e. X /\ (F` m) e. X)) -> ((F` j)D(F` m)) e. RR)
33	32	adantlr 395	. . . . . . . . . . . . 13 |- (((D e. Met /\ y e. RR) /\ ((F` j) e. X /\ (F` m) e. X)) -> ((F` j)D(F` m)) e. RR)
34	33	adantrrl 404	. . . . . . . . . . . 12 |- (((D e. Met /\ y e. RR) /\ ((F` j) e. X /\ ((F` k) e. X /\ (F` m) e. X))) -> ((F` j)D(F` m)) e. RR)
35		simplr 415	. . . . . . . . . . . 12 |- (((D e. Met /\ y e. RR) /\ ((F` j) e. X /\ ((F` k) e. X /\ (F` m) e. X))) -> y e. RR)
36	26, 30, 34, 35	syl3anc 860	. . . . . . . . . . 11 |-