Theorem lmcau 8207

Description: Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of [Kreyszig] p. 28. Warning: The HTML proof page is 0.5MB in size.

Hypothesis

Ref	Expression
lmcau.1	|- P e. V

Assertion

Ref	Expression
lmcau	|- ((D e. Met /\ F(~~>m` D)P) -> F e. (Cau` D))

Proof of Theorem lmcau

Step	Hyp	Ref	Expression
1		halfpos2 6183	. . . . . . . . . . . 12 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
2	1	biimpd 151	. . . . . . . . . . 11 |- (x e. RR -> (0 < x -> 0 < (x / 2)))
3	2	adantl 388	. . . . . . . . . 10 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> (0 < x -> 0 < (x / 2)))
4		prth 559	. . . . . . . . . . . . . . 15 |- (((j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))) -> ((j <_ k /\ j <_ m) -> (((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))))
5		simpll 412	. . . . . . . . . . . . . . . . 17 |- ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (F` k) e. dom dom D)
6	5	a1i 8	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (F` k) e. dom dom D))
7		simprl 414	. . . . . . . . . . . . . . . . 17 |- ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (F` m) e. dom dom D)
8	7	a1i 8	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (F` m) e. dom dom D))
9		lt2add 5797	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((F` k)DP) e. RR /\ ((F` m)DP) e. RR) /\ ((x / 2) e. RR /\ (x / 2) e. RR)) -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> (((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2))))
10		eqid 1518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- dom dom D = dom dom D
11	10	metcl 8021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ (F` k) e. dom dom D /\ P e. dom dom D) -> ((F` k)DP) e. RR)
12	11	3expb 840	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ ((F` k) e. dom dom D /\ P e. dom dom D)) -> ((F` k)DP) e. RR)
13	12	adantrlr 401	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> ((F` k)DP) e. RR)
14	10	metcl 8021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ (F` m) e. dom dom D /\ P e. dom dom D) -> ((F` m)DP) e. RR)
15	14	3expb 840	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ ((F` m) e. dom dom D /\ P e. dom dom D)) -> ((F` m)DP) e. RR)
16	15	adantrll 400	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> ((F` m)DP) e. RR)
17	13, 16	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> (((F` k)DP) e. RR /\ ((F` m)DP) e. RR))
18	17	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> (((F` k)DP) e. RR /\ ((F` m)DP) e. RR))
19		rehalfcl 6180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. RR -> (x / 2) e. RR)
20	19, 19	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. RR -> ((x / 2) e. RR /\ (x / 2) e. RR))
21	20	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((x / 2) e. RR /\ (x / 2) e. RR))
22	9, 18, 21	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> (((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2))))
23		recn 5467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. RR -> x e. CC)
24		2halves 6185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. CC -> ((x / 2) + (x / 2)) = x)
25	23, 24	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. RR -> ((x / 2) + (x / 2)) = x)
26	25	breq2d 2703	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. RR -> ((((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2)) <-> (((F` k)DP) + ((F` m)DP)) < x))
27	26	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2)) <-> (((F` k)DP) + ((F` m)DP)) < x))
28	10	mettri3 8028	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ P e. dom dom D)) -> ((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)))
29		id 59	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ P e. dom dom D) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ P e. dom dom D))
30	29	3expa 839	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ P e. dom dom D))
31	28, 30	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> ((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)))
32	31	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)))
33		lelttr 5677	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((F` k)D(F` m)) e. RR /\ (((F` k)DP) + ((F` m)DP)) e. RR /\ x e. RR) -> ((((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)) /\ (((F` k)DP) + ((F` m)DP)) < x) -> ((F` k)D(F` m)) < x))
34	10	metcl 8021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((D e. Met /\ (F` k) e. dom dom D /\ (F` m) e. dom dom D) -> ((F` k)D(F` m)) e. RR)
35	34	3expb 840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ ((F` k) e. dom dom D /\ (F` m) e. dom dom D)) -> ((F` k)D(F` m)) e. RR)
36	35	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> ((F` k)D(F` m)) e. RR)
37	36	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((F` k)D(F` m)) e. RR)
38		readdcl 5456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((F` k)DP) e. RR /\ ((F` m)DP) e. RR) -> (((F` k)DP) + ((F` m)DP)) e. RR)
39	17, 38	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ (((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D)) -> (((F` k)DP) + ((F` m)DP)) e. RR)
40	39	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> (((F` k)DP) + ((F` m)DP)) e. RR)
41		simprr 415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> x e. RR)
42	33, 37, 40, 41	syl3anc 864	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((((F` k)D(F` m)) <_ (((F` k)DP) + ((F` m)DP)) /\ (((F` k)DP) + ((F` m)DP)) < x) -> ((F` k)D(F` m)) < x))
43	32, 42	mpand 705	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((((F` k)DP) + ((F` m)DP)) < x -> ((F` k)D(F` m)) < x))
44	27, 43	sylbid 201	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2)) -> ((F` k)D(F` m)) < x))
45	22, 44	syld 27	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((D e. Met /\ ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ P e. dom dom D) /\ x e. RR)) -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> ((F` k)D(F` m)) < x))
46	45	exp44 385	. . . . . . . . . . . . . . . . . . . . . 22 |- (D e. Met -> (((F` k) e. dom dom D /\ (F` m) e. dom dom D) -> (P e. dom dom D -> (x e. RR -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> ((F` k)D(F` m)) < x)))))
47	46	com12 11	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` k) e. dom dom D /\ (F` m) e. dom dom D) -> (D e. Met -> (P e. dom dom D -> (x e. RR -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> ((F` k)D(F` m)) < x)))))
48	47	imp4c 364	. . . . . . . . . . . . . . . . . . . 20 |- (((F` k) e. dom dom D /\ (F` m) e. dom dom D) -> (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> ((F` k)D(F` m)) < x)))
49	48	com23 32	. . . . . . . . . . . . . . . . . . 19 |- (((F` k) e. dom dom D /\ (F` m) e. dom dom D) -> ((((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2)) -> (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((F` k)D(F` m)) < x)))
50	49	imp 348	. . . . . . . . . . . . . . . . . 18 |- ((((F` k) e. dom dom D /\ (F` m) e. dom dom D) /\ (((F` k)DP) < (x / 2) /\ ((F` m)DP) < (x / 2))) -> (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((F` k)D(F` m)) < x))
51	50	an4s 511	. . . . . . . . . . . . . . . . 17 |- ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((F` k)D(F` m)) < x))
52	51	com12 11	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> ((F` k)D(F` m)) < x))
53	6, 8, 52	3jcad 826	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)) /\ ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x)))
54	4, 53	syl9r 58	. . . . . . . . . . . . . 14 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> (((j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))) -> ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))
55	54	r19.20sdv 1756	. . . . . . . . . . . . 13 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> (A.m e. ZZ ((j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))) -> A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))
56	55	r19.20sdv 1756	. . . . . . . . . . . 12 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> (A.k e. ZZ A.m e. ZZ ((j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))) -> A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))
57		breq2 2696	. . . . . . . . . . . . . . . . 17 |- (n = k -> (j <_ n <-> j <_ k))
58		fveq2 3835	. . . . . . . . . . . . . . . . . . 19 |- (n = k -> (F` n) = (F` k))
59	58	eleq1d 1583	. . . . . . . . . . . . . . . . . 18 |- (n = k -> ((F` n) e. dom dom D <-> (F` k) e. dom dom D))
60	58	opreq1d 4033	. . . . . . . . . . . . . . . . . . 19 |- (n = k -> ((F` n)DP) = ((F` k)DP))
61	60	breq1d 2702	. . . . . . . . . . . . . . . . . 18 |- (n = k -> (((F` n)DP) < (x / 2) <-> ((F` k)DP) < (x / 2)))
62	59, 61	anbi12d 631	. . . . . . . . . . . . . . . . 17 |- (n = k -> (((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)) <-> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))))
63	57, 62	imbi12d 629	. . . . . . . . . . . . . . . 16 |- (n = k -> ((j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) <-> (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)))))
64	63	rcla4cv 1920	. . . . . . . . . . . . . . 15 |- (A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) -> (k e. ZZ -> (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2)))))
65	64	r19.21aiv 1759	. . . . . . . . . . . . . 14 |- (A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) -> A.k e. ZZ (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))))
66		breq2 2696	. . . . . . . . . . . . . . . . 17 |- (n = m -> (j <_ n <-> j <_ m))
67		fveq2 3835	. . . . . . . . . . . . . . . . . . 19 |- (n = m -> (F` n) = (F` m))
68	67	eleq1d 1583	. . . . . . . . . . . . . . . . . 18 |- (n = m -> ((F` n) e. dom dom D <-> (F` m) e. dom dom D))
69	67	opreq1d 4033	. . . . . . . . . . . . . . . . . . 19 |- (n = m -> ((F` n)DP) = ((F` m)DP))
70	69	breq1d 2702	. . . . . . . . . . . . . . . . . 18 |- (n = m -> (((F` n)DP) < (x / 2) <-> ((F` m)DP) < (x / 2)))
71	68, 70	anbi12d 631	. . . . . . . . . . . . . . . . 17 |- (n = m -> (((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)) <-> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))))
72	66, 71	imbi12d 629	. . . . . . . . . . . . . . . 16 |- (n = m -> ((j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) <-> (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))))
73	72	rcla4cv 1920	. . . . . . . . . . . . . . 15 |- (A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) -> (m e. ZZ -> (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))))
74	73	r19.21aiv 1759	. . . . . . . . . . . . . 14 |- (A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) -> A.m e. ZZ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))))
75	65, 74	jca 286	. . . . . . . . . . . . 13 |- (A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) -> (A.k e. ZZ (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ A.m e. ZZ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))))
76		raaan 2414	. . . . . . . . . . . . 13 |- (A.k e. ZZ A.m e. ZZ ((j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))) <-> (A.k e. ZZ (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ A.m e. ZZ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))))
77	75, 76	sylibr 198	. . . . . . . . . . . 12 |- (A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) -> A.k e. ZZ A.m e. ZZ ((j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))) /\ (j <_ m -> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2)))))
78	56, 77	syl5 21	. . . . . . . . . . 11 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> (A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) -> A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))
79	78	r19.22sdv 1784	. . . . . . . . . 10 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> (E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))) -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))
80	3, 79	imim12d 29	. . . . . . . . 9 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> ((0 < (x / 2) -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)))) -> (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x)))))
81	80	r19.20dva 1755	. . . . . . . 8 |- ((D e. Met /\ P e. dom dom D) -> (A.x e. RR (0 < (x / 2) -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)))) -> A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x)))))
82	81	expimpd 373	. . . . . . 7 |- (D e. Met -> ((P e. dom dom D /\ A.x e. RR (0 < (x / 2) -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))))) -> A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x)))))
83		breq2 2696	. . . . . . . . . . 11 |- (q = (x / 2) -> (0 < q <-> 0 < (x / 2)))
84		breq2 2696	. . . . . . . . . . . . . 14 |- (q = (x / 2) -> (((F` n)DP) < q <-> ((F` n)DP) < (x / 2)))
85	84	anbi2d 619	. . . . . . . . . . . . 13 |- (q = (x / 2) -> (((F` n) e. dom dom D /\ ((F` n)DP) < q) <-> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))))
86	85	imbi2d 615	. . . . . . . . . . . 12 |- (q = (x / 2) -> ((j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q)) <-> (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)))))
87	86	rexralbidv 1728	. . . . . . . . . . 11 |- (q = (x / 2) -> (E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q)) <-> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)))))
88	83, 87	imbi12d 629	. . . . . . . . . 10 |- (q = (x / 2) -> ((0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q))) <-> (0 < (x / 2) -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))))))
89	88	rcla4cv 1920	. . . . . . . . 9 |- (A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q))) -> ((x / 2) e. RR -> (0 < (x / 2) -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))))))
90	89, 19	syl5 21	. . . . . . . 8 |- (A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q))) -> (x e. RR -> (0 < (x / 2) -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2))))))
91	90	r19.21aiv 1759	. . . . . . 7 |- (A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q))) -> A.x e. RR (0 < (x / 2) -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)))))
92	82, 91	sylan2i 467	. . . . . 6 |- (D e. Met -> ((P e. dom dom D /\ A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q)))) -> A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x)))))
93	92	anim2d 564	. . . . 5 |- (D e. Met -> ((F (_ (CC X. dom dom D) /\ (P e. dom dom D /\ A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q))))) -> (F (_ (CC X. dom dom D) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))))
94	93	exp4d 381	. . . 4 |- (D e. Met -> (F (_ (CC X. dom dom D) -> (P e. dom dom D -> (A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q))) -> (F (_ (CC X. dom dom D) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))))))
95	94	3impd 853	. . 3 |- (D e. Met -> ((F (_ (CC X. dom dom D) /\ P e. dom dom D /\ A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q)))) -> (F (_ (CC X. dom dom D) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))))
96		lmcau.1	. . . 4 |- P e. V
97	10	lmbr 8139	. . . 4 |- ((D e. Met /\ P e. V) -> (F(~~>m` D)P <-> (F (_ (CC X. dom dom D) /\ P e. dom dom D /\ A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q))))))
98	96, 97	mpan2 700	. . 3 |- (D e. Met -> (F(~~>m` D)P <-> (F (_ (CC X. dom dom D) /\ P e. dom dom D /\ A.q e. RR (0 < q -> E.j e. ZZ A.n e. ZZ (j <_ n -> ((F` n) e. dom dom D /\ ((F` n)DP) < q))))))
99	10	iscau 8147	. . 3 |- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. dom dom D) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((F` k) e. dom dom D /\ (F` m) e. dom dom D /\ ((F` k)D(F` m)) < x))))))
100	95, 98, 99	3imtr4d 546	. 2 |- (D e. Met -> (F(~~>m` D)P -> F e. (Cau` D)))
101	100	imp 348	1 |- ((D e. Met /\ F(~~>m` D)P) -> F e. (Cau` D))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   /\ w3a 781   = wceq 992   e. wcel 994  A.wral 1691  E.wrex 1692  Vcvv 1857   (_ wss 2099   class class class wbr 2692   X. cxp 3249  dom cdm 3251  ` cfv 3263  (class class class)co 4021  CCcc 5386  RRcr 5387  0cc0 5388   + caddc 5391   / cdiv 5448   <_ cle 5449  ZZcz 5452   < clt 5640  2c2 6107  Metcme 7999  ~~>mclm 8130  Caucca 8131

This theorem is referenced by:  cmsss 8208

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-inf2 4770

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-nel 1631  df-ral 1695  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-int 2601  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-1st 4140  df-2nd 4141  df-rdg 4233  df-1o 4269  df-oadd 4271  df-omul 4272  df-er 4401  df-ec 4403  df-qs 4406  df-en 4509  df-dom 4510  df-sdom 4511  df-ni 5154  df-pli 5155  df-mi 5156  df-lti 5157  df-plpq 5189  df-mpq 5190  df-enq 5191  df-nq 5192  df-plq 5193  df-mq 5194  df-rq 5195  df-ltq 5196  df-1q 5197  df-np 5240  df-1p 5241  df-plp 5242  df-mp 5243  df-ltp 5244  df-plpr 5318  df-mpr 5319  df-enr 5320  df-nr 5321  df-plr 5322  df-mr 5323  df-ltr 5324  df-0r 5325  df-1r 5326  df-m1r 5327  df-c 5394  df-0 5395  df-1 5396  df-i 5397  df-r 5398  df-plus 5399  df-mul 5400  df-lt 5401  df-sub 5510  df-neg 5512  df-pnf 5641  df-mnf 5642  df-xr 5643  df-ltxr 5644  df-le 5645  df-div 5855  df-2 6116  df-met 8003  df-lm 8133  df-cau 8134

Copyright terms: Public domain