Theorem lmuni 7913

Description: A sequence converges to at most one limit. Part of Lemma 1.4-2(a) of [Kreyszig] p. 26.

Hypotheses

Ref	Expression
lmuni.1	|- A e. V
lmuni.2	|- B e. V

Assertion

Ref	Expression
lmuni	|- ((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) -> A = B)

Proof of Theorem lmuni

Step	Hyp	Ref	Expression
1		squeeze0 5882	. . 3 |- (((ADB) e. RR /\ 0 <_ (ADB) /\ A.x e. RR (0 < x -> (ADB) < x)) -> (ADB) = 0)
2		3simp1 787	. . . . 5 |- ((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) -> D e. Met)
3		lmuni.1	. . . . . . 7 |- A e. V
4		eqid 1474	. . . . . . . 8 |- dom dom D = dom dom D
5	4	lmcl 7911	. . . . . . 7 |- ((D e. Met /\ A e. V /\ F(~~>m` D)A) -> A e. dom dom D)
6	3, 5	mp3an2 903	. . . . . 6 |- ((D e. Met /\ F(~~>m` D)A) -> A e. dom dom D)
7	6	3adant3 798	. . . . 5 |- ((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) -> A e. dom dom D)
8		lmuni.2	. . . . . . 7 |- B e. V
9	4	lmcl 7911	. . . . . . 7 |- ((D e. Met /\ B e. V /\ F(~~>m` D)B) -> B e. dom dom D)
10	8, 9	mp3an2 903	. . . . . 6 |- ((D e. Met /\ F(~~>m` D)B) -> B e. dom dom D)
11	10	3adant2 797	. . . . 5 |- ((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) -> B e. dom dom D)
12	2, 7, 11	3jca 818	. . . 4 |- ((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) -> (D e. Met /\ A e. dom dom D /\ B e. dom dom D))
13	4	metcl 7771	. . . 4 |- ((D e. Met /\ A e. dom dom D /\ B e. dom dom D) -> (ADB) e. RR)
14	12, 13	syl 10	. . 3 |- ((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) -> (ADB) e. RR)
15	4	metge0 7781	. . . 4 |- ((D e. Met /\ A e. dom dom D /\ B e. dom dom D) -> 0 <_ (ADB))
16	12, 15	syl 10	. . 3 |- ((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) -> 0 <_ (ADB))
17		1z 6116	. . . . . . . . . . . 12 |- 1 e. ZZ
18		nnuz 6384	. . . . . . . . . . . 12 |- NN = (ZZ>` 1)
19	4, 17, 18	lmcvg 7894	. . . . . . . . . . 11 |- (((D e. Met /\ A e. V /\ F(~~>m` D)A) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DA) < (x / 2))))
20	3, 19	mp3anl2 910	. . . . . . . . . 10 |- (((D e. Met /\ F(~~>m` D)A) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DA) < (x / 2))))
21	20	3adantl3 804	. . . . . . . . 9 |- (((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DA) < (x / 2))))
22	4, 17, 18	lmcvg 7894	. . . . . . . . . . 11 |- (((D e. Met /\ B e. V /\ F(~~>m` D)B) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DB) < (x / 2))))
23	8, 22	mp3anl2 910	. . . . . . . . . 10 |- (((D e. Met /\ F(~~>m` D)B) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DB) < (x / 2))))
24	23	3adantl2 803	. . . . . . . . 9 |- (((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DB) < (x / 2))))
25	21, 24	jca 288	. . . . . . . 8 |- (((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> (E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DA) < (x / 2))) /\ E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DB) < (x / 2)))))
26	17, 18	cvganuz 6877	. . . . . . . 8 |- ((E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DA) < (x / 2))) /\ E.j e. NN A.k e. NN (j <_ k -> ((F` k) e. dom dom D /\ ((F` k)DB) < (x / 2)))) <-> E.j e. NN A.k e. NN (j <_ k -> (((F` k) e. dom dom D /\ ((F` k)DA) < (x / 2)) /\ ((F` k) e. dom dom D /\ ((F` k)DB) < (x / 2)))))
27	25, 26	sylib 198	. . . . . . 7 |- (((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.j e. NN A.k e. NN (j <_ k -> (((F` k) e. dom dom D /\ ((F` k)DA) < (x / 2)) /\ ((F` k) e. dom dom D /\ ((F` k)DB) < (x / 2)))))
28		rehalfclt 5991	. . . . . . . . 9 |- (x e. RR -> (x / 2) e. RR)
29	28	adantr 389	. . . . . . . 8 |- ((x e. RR /\ 0 < x) -> (x / 2) e. RR)
30		halfpos2t 5994	. . . . . . . . 9 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
31	30	biimpa 416	. . . . . . . 8 |- ((x e. RR /\ 0 < x) -> 0 < (x / 2))
32	29, 31	jca 288	. . . . . . 7 |- ((x e. RR /\ 0 < x) -> ((x / 2) e. RR /\ 0 < (x / 2)))
33	27, 32	sylan2 451	. . . . . 6 |- (((D e. Met /\ F(~~>m` D)A /\ F(~~>m` D)B) /\ (x e. RR /\ 0 < x)) -> E.j e. NN A.k e. NN (j <_ k -> (((F` k) e. dom dom D /\ ((F` k)DA) < (x / 2)) /\ ((F` k) e. dom dom D /\ ((F` k)DB) < (x / 2)))))
34		nnret 5887	. . . . . . . . . . 11 |- (j e. NN -> j e. RR)
35		leidt 5514	. . . . . . . . . . 11 |- (j e. RR -> j <_ j)
36	34, 35	syl 10	. . . . . . . . . 10 |- (j e. NN -> j <_ j)
37		breq2 2619	. . . . . . . . . . 11 |- (k = j -> (j <_ k <-> j <_ j))
38	37	rcla4ev 1874	. . . . . . . . . 10 |- ((j e. NN /\ j <_ j) -> E.k e. NN j <_ k)
39	36, 38	mpdan 703	. . . . . . . . 9 |- (j e. NN -> E.k e. NN j <_ k)
40	39	rgen 1696	. . . . . . . 8 |- A.j e. NN E.k e. NN j <_ k
41		lt2addt 5627	. . . . . . . . . . . . . . . . . . . 20 |- (((((F` k)DA) e. RR /\ ((F` k)DB) e. RR) /\ ((x / 2) e. RR /\ (x / 2) e. RR)) -> ((((F` k)DA) < (x / 2) /\ ((F` k)DB) < (x / 2)) -> (((F` k)DA) + ((F` k)DB)) < ((x / 2) + (x / 2))))
42	4	metcl 7771	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ (F` k) e. dom dom D /\ A e. dom dom D) -> ((F` k)DA) e. RR)
43	42	3com23 838	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((D e. Met /\ A e. dom dom D /\ (F` k) e. dom dom D) -> ((F` k)DA) e. RR)
44	43	3expa 832	. . . . . . . . . . . . . . . . . . . . . 22 |- (((D e. Met /\ A e. dom dom D) /\ (F` k) e. dom dom D) -> ((F` k)DA) e. RR)
45	44	3adantl3 804	. . . . . . . . . . . . . . . . . . . . 21 |- (((D e. Met /\ A e. dom dom D /\ B e. dom dom D) /\ (F` k) e. dom dom D) -> ((F` k)DA) e. RR)
46	4	metcl 7771	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ (F` k) e. dom dom D /\ B e. dom dom D) -> ((F` k)DB) e. RR)
47	46	3com23 838	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((D e. Met /\ B e. dom dom D /\ (F` k) e. dom dom D) -> ((F` k)DB) e. RR)
48	47	3expa 832	. . . . . . . . . . . . . . . . . . . . . 22 |- (((D e. Met /\ B e. dom dom D) /\ (F` k) e. dom dom D) -> ((F` k)DB) e. RR)
49	48	3adantl2 803	. . . . . . . . . . . . . . . . . . . . 21 |- (((D e. Met /\ A e. dom dom D /\ B e. dom dom D) /\ (F` k) e. dom dom D) -> ((F` k)DB