Theorem iscau3 7876

Description: Express the property "F is a Cauchy sequence of metric D " with one less quantifier.

Hypotheses

Ref	Expression
lmbr.1	|- X = dom dom D
iscau3.3	|- N e. ZZ
iscau3.4	|- Z = (ZZ>` N)

Assertion

Ref	Expression
iscau3	|- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.j e. Z A.k e. Z (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,N,k   j,X,k,x   j,Z,k,x

Proof of Theorem iscau3

Step	Hyp	Ref	Expression
1		lmbr.1	. . 3 |- X = dom dom D
2		iscau3.3	. . 3 |- N e. ZZ
3		iscau3.4	. . 3 |- Z = (ZZ>` N)
4	1, 2, 3	iscau2 7875	. 2 |- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.m e. Z A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))))
5		fveq2 3709	. . . . . 6 |- (k = m -> (F` k) = (F` m))
6	5	eleq1d 1532	. . . . 5 |- (k = m -> ((F` k) e. X <-> (F` m) e. X))
7	5	opreq2d 3961	. . . . . 6 |- (k = m -> ((F` j)D(F` k)) = ((F` j)D(F` m)))
8	7	breq1d 2619	. . . . 5 |- (k = m -> (((F` j)D(F` k)) < x <-> ((F` j)D(F` m)) < x))
9	6, 8	3anbi23d 893	. . . 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)))
10		fveq2 3709	. . . . . 6 |- (j = k -> (F` j) = (F` k))
11	10	eleq1d 1532	. . . . 5 |- (j = k -> ((F` j) e. X <-> (F` k) e. X))
12	10	opreq1d 3960	. . . . . 6 |- (j = k -> ((F` j)D(F` m)) = ((F` k)D(F` m)))
13	12	breq1d 2619	. . . . 5 |- (j = k -> (((F` j)D(F` m)) < x <-> ((F` k)D(F` m)) < x))
14	11, 13	3anbi13d 892	. . . 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)))
15		breq2 2613	. . . . . 6 |- (x = (y / 2) -> (((F` j)D(F` k)) < x <-> ((F` j)D(F` k)) < (y / 2)))
16	15	3anbi3d 896	. . . . 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))))
17		breq2 2613	. . . . . 6 |- (x = (y / 2) -> (((F` j)D(F` m)) < x <-> ((F` j)D(F` m)) < (y / 2)))
18	17	3anbi3d 896	. . . . 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))))
19	16, 18	anbi12d 626	. . . 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)))))
20		breq2 2613	. . . . 5 |- (x = y -> (((F` k)D(F` m)) < x <-> ((F` k)D(F` m)) < y))
21	20	3anbi3d 896	. . . 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)))
22		3simp2 787	. . . . . . . 8 |- (((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < (y / 2)) -> (F` k) e. X)
23	22	adantr 389	. . . . . . 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)
24	23	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))
25		3simp2 787	. . . . . . . 8 |- (((F` j) e. X /\ (F` m) e. X /\ ((F` j)D(F` m)) < (y / 2)) -> (F` m) e. X)
26	25	adantl 388	. . . . . . 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)
27	26	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))
28		lt2halvest 5989	. . . . . . . . . . . 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))
29	1	metcl 7750	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ (F` j) e. X /\ (F` k) e. X) -> ((F` j)D(F` k)) e. RR)
30	29	3expb 832	. . . . . . . . . . . . . 14 |- ((D e. Met /\ ((F` j) e. X /\ (F` k) e. X)) -> ((F` j)D(F` k)) e. RR)
31	30	adantlr 393	. . . . . . . . . . . . 13 |- (((D e. Met /\ y e. RR) /\ ((F` j) e. X /\ (F` k) e. X)) -> ((F` j)D(F` k)) e. RR)
32	31	adantrrr 403	. . . . . . . . . . . 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)
33	1	metcl 7750	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ (F` j) e. X /\ (F` m) e. X) -> ((F` j)D(F` m)) e. RR)
34	33	3expb 832	. . . . . . . . . . . . . 14 |- ((D e. Met /\ ((F` j) e. X /\ (F` m) e. X)) -> ((F` j)D(F` m)) e. RR)
35	34	adantlr 393	. . . . . . . . . . . . 13 |- (((D e. Met /\ y e. RR) /\ ((F` j) e. X /\ (F` m) e. X)) -> ((F` j)D(F` m)) e. RR)
36	35	adantrrl 402	. . . . . . . . . . . 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)
37		simplr 413	. . . . . . . . . . . 12 |- (((D e. Met /\ y e. RR) /\ ((F