Theorem lmcau 9274

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 7223	. . . . . . . . . . . 12 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
2	1	biimpd 170	. . . . . . . . . . 11 |- (x e. RR -> (0 < x -> 0 < (x / 2)))
3	2	adantl 424	. . . . . . . . . 10 |- (((D e. Met /\ P e. dom dom D) /\ x e. RR) -> (0 < x -> 0 < (x / 2)))
4		prth 615	. . . . . . . . . . . . . . 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 448	. . . . . . . . . . . . . . . . 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 450	. . . . . . . . . . . . . . . . 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		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- dom dom D = dom dom D
10	9	metcl 9088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ (F` k) e. dom dom D /\ P e. dom dom D) -> ((F` k)DP) e. RR)
11	10	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ ((F` k) e. dom dom D /\ P e. dom dom D)) -> ((F` k)DP) e. RR)
12	11	adantrlr 437	. . . . . . . . . . . . . . . . . . . . . . . . . . 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)
13	9	metcl 9088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ (F` m) e. dom dom D /\ P e. dom dom D) -> ((F` m)DP) e. RR)
14	13	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((D e. Met /\ ((F` m) e. dom dom D /\ P e. dom dom D)) -> ((F` m)DP) e. RR)
15	14	adantrll 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 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)
16	12, 15	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . 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))
17	16	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . 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))
18		rehalfcl 7220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. RR -> (x / 2) e. RR)
19	18, 18	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. RR -> ((x / 2) e. RR /\ (x / 2) e. RR))
20	19	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . 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))
21		lt2add 6827	. . . . . . . . . . . . . . . . . . . . . . . . 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))))
22	17, 20, 21	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . 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 6466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. RR -> x e. CC)
24		2halves 7225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. CC -> ((x / 2) + (x / 2)) = x)
25	23, 24	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. RR -> ((x / 2) + (x / 2)) = x)
26	25	breq2d 3350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. RR -> ((((F` k)DP) + ((F` m)DP)) < ((x / 2) + (x / 2)) <-> (((F` k)DP) + ((F` m)DP)) < x))
27	26	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . 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	9	mettri3 9095	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1067	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 431	. . . . . . . . . . . . . . . . . . . . . . . . . 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	9	metcl 9088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((D e. Met /\ (F` k) e. dom dom D /\ (F` m) e. dom dom D) -> ((F` k)D(F` m)) e. RR)
34	33	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((D e. Met /\ ((F` k) e. dom dom D /\ (F` m) e. dom dom D)) -> ((F` k)D(F` m)) e. RR)
35	34	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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)
36	35	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 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)
37		readdcl 6455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((F` k)DP) e. RR /\ ((F` m)DP) e. RR) -> (((F` k)DP) + ((F` m)DP)) e. RR)
38	12, 15, 37	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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)
39	38	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 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)
40		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 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)
41		lelttr 6693	. . . . . . . . . . . . . . . . . . . . . . . . . . 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))
42	36, 39, 40, 41	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . 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 765	. . . . . . . . . . . . . . . . . . . . . . . . 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 220	. . . . . . . . . . . . . . . . . . . . . . . 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 30	. . . . . . . . . . . . . . . . . . . . . . 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 416	. . . . . . . . . . . . . . . . . . . . . 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 14	. . . . . . . . . . . . . . . . . . . . 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 393	. . . . . . . . . . . . . . . . . . . 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 36	. . . . . . . . . . . . . . . . . . 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 377	. . . . . . . . . . . . . . . . . 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 566	. . . . . . . . . . . . . . . . 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 14	. . . . . . . . . . . . . . . 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 1051	. . . . . . . . . . . . . . 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 72	. . . . . . . . . . . . . 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	ralimdv 2172	. . . . . . . . . . . . 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	ralimdv 2172	. . . . . . . . . . . 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		raaanv 2977	. . . . . . . . . . . . 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)))))
58		breq2 3342	. . . . . . . . . . . . . . . 16 |- (n = k -> (j <_ n <-> j <_ k))
59		fveq2 4681	. . . . . . . . . . . . . . . . . 18 |- (n = k -> (F` n) = (F` k))
60	59	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (n = k -> ((F` n) e. dom dom D <-> (F` k) e. dom dom D))
61	59	opreq1d 4897	. . . . . . . . . . . . . . . . . 18 |- (n = k -> ((F` n)DP) = ((F` k)DP))
62	61	breq1d 3348	. . . . . . . . . . . . . . . . 17 |- (n = k -> (((F` n)DP) < (x / 2) <-> ((F` k)DP) < (x / 2)))
63	60, 62	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (n = k -> (((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)) <-> ((F` k) e. dom dom D /\ ((F` k)DP) < (x / 2))))
64	58, 63	imbi12d 688	. . . . . . . . . . . . . . 15 |- (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)))))
65	64	rcla4cv 2377	. . . . . . . . . . . . . 14 |- (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)))))
66	65	r19.21aiv 2175	. . . . . . . . . . . . 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))))
67		breq2 3342	. . . . . . . . . . . . . . . 16 |- (n = m -> (j <_ n <-> j <_ m))
68		fveq2 4681	. . . . . . . . . . . . . . . . . 18 |- (n = m -> (F` n) = (F` m))
69	68	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (n = m -> ((F` n) e. dom dom D <-> (F` m) e. dom dom D))
70	68	opreq1d 4897	. . . . . . . . . . . . . . . . . 18 |- (n = m -> ((F` n)DP) = ((F` m)DP))
71	70	breq1d 3348	. . . . . . . . . . . . . . . . 17 |- (n = m -> (((F` n)DP) < (x / 2) <-> ((F` m)DP) < (x / 2)))
72	69, 71	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (n = m -> (((F` n) e. dom dom D /\ ((F` n)DP) < (x / 2)) <-> ((F` m) e. dom dom D /\ ((F` m)DP) < (x / 2))))
73	67, 72	imbi12d 688	. . . . . . . . . . . . . . 15 |- (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)))))
74	73	rcla4cv 2377	. . . . . . . . . . . . . 14 |- (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)))))
75	74	r19.21aiv 2175	. . . . . . . . . . . . 13 |- (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))))
76	57, 66, 75	sylanbrc 527	. . . . . . . . . . . 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)))))
77	56, 76	syl5 20	. . . . . . . . . . 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))))
78	77	reximdv 2202	. . . . . . . . . 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))))
79	3, 78	imim12d 69	. . . . . . . . 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)))))
80	79	ralimdvaa 2171	. . . . . . . 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)))))
81	80	expimpd 404	. . . . . . 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)))))
82		breq2 3342	. . . . . . . . . . 11 |- (q = (x / 2) -> (0 < q <-> 0 < (x / 2)))
83		breq2 3342	. . . . . . . . . . . . . 14 |- (q = (x / 2) -> (((F` n)DP) < q <-> ((F` n)DP) < (x / 2)))
84	83	anbi2d 678	. . . . . . . . . . . . 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))))
85	84	imbi2d 674	. . . . . . . . . . . 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)))))
86	85	rexralbidv 2142	. . . . . . . . . . 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)))))
87	82, 86	imbi12d 688	. . . . . . . . . 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))))))
88	87	rcla4cv 2377	. . . . . . . . 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))))))
89	88, 18	syl5 20	. . . . . . . 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))))))
90	89	r19.21aiv 2175	. . . . . . 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)))))
91	81, 90	sylan2i 514	. . . . . 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)))))
92	91	anim2d 620	. . . . 5 |- (D e. Met -> ((F C_ (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 C_ (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))))))
93	92	exp4d 412	. . . 4 |- (D e. Met -> (F C_ (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 C_ (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	3impd 1082	. . 3 |- (D e. Met -> ((F C_ (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 C_ (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		lmcau.1	. . . 4 |- P e. _V
96	9	lmbr 9206	. . . 4 |- ((D e. Met /\ P e. _V) -> (F(~~>m` D)P <-> (F C_ (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))))))
97	95, 96	mpan2 760	. . 3 |- (D e. Met -> (F(~~>m` D)P <-> (F C_ (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	9	iscau 9214	. . 3 |- (D e. Met -> (F e. (Cau` D) <-> (F C_ (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))))))
99	94, 97, 98	3imtr4d 602	. 2 |- (D e. Met -> (F(~~>m` D)P -> F e. (Cau` D)))
100	99	imp 377	1 |- ((D e. Met /\ F(~~>m` D)P) -> F e. (Cau` D))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593   class class class wbr 3338   X. cxp 3984  dom cdm 3986  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386   + caddc 6389   / cdiv 6447   <_ cle 6448  ZZcz 6451   < clt 6653  2c2 7145  Metcme 9066  ~~>mclm 9197  Caucca 9198

This theorem is referenced by:  cmsss 9275

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-2 7154  df-met 9070  df-lm 9200  df-cau 9201

Copyright terms: Public domain