Theorem lmle 7957

Description: If the distance from each member of a converging sequence to a given point is less than or equal to a given amount, so is the convergence value. Warning: The HTML proof page is 0.5MB in size.

Hypotheses

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

Assertion

Ref	Expression
lmle	|- (((D e. Met /\ P e. A /\ F(~~>m` D)P) /\ (Q e. X /\ R e. RR /\ A.k e. Z ((F` k)DQ) <_ R)) -> (PDQ) <_ R)

Distinct variable groups:   D,k   k,F   k,N   P,k   Q,k   R,k   k,X   k,Z

Proof of Theorem lmle

Step	Hyp	Ref	Expression
1		lmfex.1	. . . . . . . . 9 |- X = dom dom D
2	1	metcl 7808	. . . . . . . 8 |- ((D e. Met /\ P e. X /\ Q e. X) -> (PDQ) e. RR)
3	2	3expa 835	. . . . . . 7 |- (((D e. Met /\ P e. X) /\ Q e. X) -> (PDQ) e. RR)
4		ltnrt 5542	. . . . . . 7 |- ((PDQ) e. RR -> -. (PDQ) < (PDQ))
5	3, 4	syl 10	. . . . . 6 |- (((D e. Met /\ P e. X) /\ Q e. X) -> -. (PDQ) < (PDQ))
6	5	3adantl3 807	. . . . 5 |- (((D e. Met /\ P e. X /\ F(~~>m` D)P) /\ Q e. X) -> -. (PDQ) < (PDQ))
7	6	3ad2antr1 814	. . . 4 |- (((D e. Met /\ P e. X /\ F(~~>m` D)P) /\ (Q e. X /\ R e. RR /\ A.k e. Z ((F` k)DQ) <_ R)) -> -. (PDQ) < (PDQ))
8		lmfex.3	. . . . . . . . . 10 |- N e. ZZ
9		lmfex.4	. . . . . . . . . 10 |- Z = (ZZ>` N)
10	1, 8, 9	lmcvg 7929	. . . . . . . . 9 |- (((D e. Met /\ P e. X /\ F(~~>m` D)P) /\ (((PDQ) - R) e. RR /\ 0 < ((PDQ) - R))) -> E.j e. Z A.k e. Z (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R))))
11		simpll 414	. . . . . . . . 9 |- ((((D e. Met /\ P e. X /\ F(~~>m` D)P) /\ (Q e. X /\ R e. RR)) /\ R < (PDQ)) -> (D e. Met /\ P e. X /\ F(~~>m` D)P))
12		resubclt 5450	. . . . . . . . . . . . . 14 |- (((PDQ) e. RR /\ R e. RR) -> ((PDQ) - R) e. RR)
13	12, 3	sylan 450	. . . . . . . . . . . . 13 |- ((((D e. Met /\ P e. X) /\ Q e. X) /\ R e. RR) -> ((PDQ) - R) e. RR)
14	13	anasss 442	. . . . . . . . . . . 12 |- (((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) -> ((PDQ) - R) e. RR)
15	14	adantr 391	. . . . . . . . . . 11 |- ((((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) /\ R < (PDQ)) -> ((PDQ) - R) e. RR)
16		posdift 5666	. . . . . . . . . . . . 13 |- ((R e. RR /\ (PDQ) e. RR) -> (R < (PDQ) <-> 0 < ((PDQ) - R)))
17		simprr 417	. . . . . . . . . . . . 13 |- (((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) -> R e. RR)
18	3	adantrr 397	. . . . . . . . . . . . 13 |- (((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) -> (PDQ) e. RR)
19	16, 17, 18	sylanc 473	. . . . . . . . . . . 12 |- (((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) -> (R < (PDQ) <-> 0 < ((PDQ) - R)))
20	19	biimpa 418	. . . . . . . . . . 11 |- ((((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) /\ R < (PDQ)) -> 0 < ((PDQ) - R))
21	15, 20	jca 288	. . . . . . . . . 10 |- ((((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) /\ R < (PDQ)) -> (((PDQ) - R) e. RR /\ 0 < ((PDQ) - R)))
22		3simpa 787	. . . . . . . . . 10 |- ((D e. Met /\ P e. X /\ F(~~>m` D)P) -> (D e. Met /\ P e. X))
23	21, 22	sylanl1 462	. . . . . . . . 9 |- ((((D e. Met /\ P e. X /\ F(~~>m` D)P) /\ (Q e. X /\ R e. RR)) /\ R < (PDQ)) -> (((PDQ) - R) e. RR /\ 0 < ((PDQ) - R)))
24	10, 11, 23	sylanc 473	. . . . . . . 8 |- ((((D e. Met /\ P e. X /\ F(~~>m` D)P) /\ (Q e. X /\ R e. RR)) /\ R < (PDQ)) -> E.j e. Z A.k e. Z (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R))))
25		3simpa 787	. . . . . . . 8 |- ((Q e. X /\ R e. RR /\ A.k e. Z ((F` k)DQ) <_ R) -> (Q e. X /\ R e. RR))
26	24, 25	sylanl2 463	. . . . . . 7 |- ((((D e. Met /\ P e. X /\ F(~~>m` D)P) /\ (Q e. X /\ R e. RR /\ A.k e. Z ((F` k)DQ) <_ R)) /\ R < (PDQ)) -> E.j e. Z A.k e. Z (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R))))
27	9	eleq2i 1541	. . . . . . . . . . . . . 14 |- (j e. Z <-> j e. (ZZ>` N))
28		eluzelz 6424	. . . . . . . . . . . . . . 15 |- (j e. (ZZ>` N) -> j e. ZZ)
29		zret 6141	. . . . . . . . . . . . . . 15 |- (j e. ZZ -> j e. RR)
30		leidt 5543	. . . . . . . . . . . . . . 15 |- (j e. RR -> j <_ j)
31	28, 29, 30	3syl 20	. . . . . . . . . . . . . 14 |- (j e. (ZZ>` N) -> j <_ j)
32	27, 31	sylbi 199	. . . . . . . . . . . . 13 |- (j e. Z -> j <_ j)
33		breq2 2628	. . . . . . . . . . . . . . 15 |- (k = j -> (j <_ k <-> j <_ j))
34		fveq2 3730	. . . . . . . . . . . . . . . . 17 |- (k = j -> (F` k) = (F` j))
35	34	eleq1d 1543	. . . . . . . . . . . . . . . 16 |- (k = j -> ((F` k) e. X <-> (F` j) e. X))
36	34	opreq1d 3981	. . . . . . . . . . . . . . . . 17 |- (k = j -> ((F` k)DP) = ((F` j)DP))
37	36	breq1d 2634	. . . . . . . . . . . . . . . 16 |- (k = j -> (((F` k)DP) < ((PDQ) - R) <-> ((F` j)DP) < ((PDQ) - R)))
38	35, 37	anbi12d 630	. . . . . . . . . . . . . . 15 |- (k = j -> (((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R)) <-> ((F` j) e. X /\ ((F` j)DP) < ((PDQ) - R))))
39	33, 38	imbi12d 628	. . . . . . . . . . . . . 14 |- (k = j -> ((j <_ k -> ((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R))) <-> (j <_ j -> ((F` j) e. X /\ ((F` j)DP) < ((PDQ) - R)))))
40	39	rcla4v 1876	. . . . . . . . . . . . 13 |- (j e. Z -> (A.k e. Z (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R))) -> (j <_ j -> ((F` j) e. X /\ ((F` j)DP) < ((PDQ) - R)))))
41	32, 40	mpid 47	. . . . . . . . . . . 12 |- (j e. Z -> (A.k e. Z (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R))) -> ((F` j) e. X /\ ((F` j)DP) < ((PDQ) - R))))
42	41	adantl 390	. . . . . . . . . . 11 |- ((((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR /\ A.k e. Z ((F` k)DQ) <_ R)) /\ j e. Z) -> (A.k e. Z (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R))) -> ((F` j) e. X /\ ((F` j)DP) < ((PDQ) - R))))
43	34	opreq1d 3981	. . . . . . . . . . . . . . . . . . 19 |- (k = j -> ((F` k)DQ) = ((F` j)DQ))
44	43	breq1d 2634	. . . . . . . . . . . . . . . . . 18 |- (k = j -> (((F` k)DQ) <_ R <-> ((F` j)DQ) <_ R))
45	44	rcla4v 1876	. . . . . . . . . . . . . . . . 17 |- (j e. Z -> (A.k e. Z ((F` k)DQ) <_ R -> ((F` j)DQ) <_ R))
46		ltleaddt 5657	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F` j)DP) e. RR /\ ((F` j)DQ) e. RR) /\ (((PDQ) - R) e. RR /\ R e. RR)) -> ((((F` j)DP) < ((PDQ) - R) /\ ((F` j)DQ) <_ R) -> (((F` j)DP) + ((F` j)DQ)) < (((PDQ) - R) + R)))
47	1	metcl 7808	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((D e. Met /\ (F` j) e. X /\ P e. X) -> ((F` j)DP) e. RR)
48	47	3com23 841	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ P e. X /\ (F` j) e. X) -> ((F