HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem lmle 7895
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
StepHypRef Expression
1 lmfex.1 . . . . . . . . 9 |- X = dom dom D
21metcl 7750 . . . . . . . 8 |- ((D e. Met /\ P e. X /\ Q e. X) -> (PDQ) e. RR)
323expa 831 . . . . . . 7 |- (((D e. Met /\ P e. X) /\ Q e. X) -> (PDQ) e. RR)
4 ltnrt 5503 . . . . . . 7 |- ((PDQ) e. RR -> -. (PDQ) < (PDQ))
53, 4syl 10 . . . . . 6 |- (((D e. Met /\ P e. X) /\ Q e. X) -> -. (PDQ) < (PDQ))
653adantl3 803 . . . . 5 |- (((D e. Met /\ P e. X /\ F(~~>m` D)P) /\ Q e. X) -> -. (PDQ) < (PDQ))
763ad2antr1 810 . . . 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)
101, 8, 9lmcvg 7870 . . . . . . . . 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 412 . . . . . . . . 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 5410 . . . . . . . . . . . . . 14 |- (((PDQ) e. RR /\ R e. RR) -> ((PDQ) - R) e. RR)
1312, 3sylan 448 . . . . . . . . . . . . 13 |- ((((D e. Met /\ P e. X) /\ Q e. X) /\ R e. RR) -> ((PDQ) - R) e. RR)
1413anasss 440 . . . . . . . . . . . 12 |- (((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) -> ((PDQ) - R) e. RR)
1514adantr 389 . . . . . . . . . . 11 |- ((((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) /\ R < (PDQ)) -> ((PDQ) - R) e. RR)
16 posdift 5627 . . . . . . . . . . . . 13 |- ((R e. RR /\ (PDQ) e. RR) -> (R < (PDQ) <-> 0 < ((PDQ) - R)))
17 simprr 415 . . . . . . . . . . . . 13 |- (((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) -> R e. RR)
183adantrr 395 . . . . . . . . . . . . 13 |- (((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) -> (PDQ) e. RR)
1916, 17, 18sylanc 471 . . . . . . . . . . . 12 |- (((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) -> (R < (PDQ) <-> 0 < ((PDQ) - R)))
2019biimpa 416 . . . . . . . . . . 11 |- ((((D e. Met /\ P e. X) /\ (Q e. X /\ R e. RR)) /\ R < (PDQ)) -> 0 < ((PDQ) - R))
2115, 20jca 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 783 . . . . . . . . . 10 |- ((D e. Met /\ P e. X /\ F(~~>m` D)P) -> (D e. Met /\ P e. X))
2321, 22sylanl1 460 . . . . . . . . 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)))
2410, 11, 23sylanc 471 . . . . . . . 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 783 . . . . . . . 8 |- ((Q e. X /\ R e. RR /\ A.k e. Z ((F` k)DQ) <_ R) -> (Q e. X /\ R e. RR))
2624, 25sylanl2 461 . . . . . . 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))))
279eleq2i 1530 . . . . . . . . . . . . . 14 |- (j e. Z <-> j e. (ZZ>` N))
28 eluzelz 6355 . . . . . . . . . . . . . . 15 |- (j e. (ZZ>` N) -> j e. ZZ)
29 zret 6086 . . . . . . . . . . . . . . 15 |- (j e. ZZ -> j e. RR)
30 leidt 5504 . . . . . . . . . . . . . . 15 |- (j e. RR -> j <_ j)
3128, 29, 303syl 20 . . . . . . . . . . . . . 14 |- (j e. (ZZ>` N) -> j <_ j)
3227, 31sylbi 199 . . . . . . . . . . . . 13 |- (j e. Z -> j <_ j)
33 breq2 2613 . . . . . . . . . . . . . . 15 |- (k = j -> (j <_ k <-> j <_ j))
34 fveq2 3709 . . . . . . . . . . . . . . . . 17 |- (k = j -> (F` k) = (F` j))
3534eleq1d 1532 . . . . . . . . . . . . . . . 16 |- (k = j -> ((F` k) e. X <-> (F` j) e. X))
3634opreq1d 3960 . . . . . . . . . . . . . . . . 17 |- (k = j -> ((F` k)DP) = ((F` j)DP))
3736breq1d 2619 . . . . . . . . . . . . . . . 16 |- (k = j -> (((F` k)DP) < ((PDQ) - R) <-> ((F` j)DP) < ((PDQ) - R)))
3835, 37anbi12d 626 . . . . . . . . . . . . . . 15 |- (k = j -> (((F` k) e. X /\ ((F` k)DP) < ((PDQ) - R)) <-> ((F` j) e. X /\ ((F` j)DP) < ((PDQ) - R))))
3933, 38imbi12d 624 . . . . . . . . . . . . . 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)))))
4039rcla4v 1864 . . . . . . . . . . . . 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)))))
4132, 40mpid 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))))
4241adantl 388 . . . . . . . . . . 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))))
4334opreq1d 3960 . . . . . . . . . . . . . . . . . . 19 |- (k = j -> ((F` k)DQ) = ((F` j)DQ))
4443breq1d 2619 . . . . . . . . . . . . . . . . . 18 |- (k = j -> (((F` k)DQ) <_ R <-> ((F` j)DQ) <_ R))
4544rcla4v 1864 . . . . . . . . . . . . . . . . 17 |- (j e. Z -> (A.k e. Z ((F` k)DQ) <_ R -> ((F` j)DQ) <_ R))
46 ltleaddt 5619 . . . . . . . . . . . . . . . . . . . . . 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)))
471metcl 7750 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((D e. Met /\ (F` j) e. X /\ P e. X) -> ((F` j)DP) e. RR)
48473com23 837 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ P e. X /\ (F` j) e. X) -> ((F`