Theorem 2climnn0 7103

Description: If two sequences converge to each other, they converge to the same limit.

Hypothesis

Ref	Expression
2climnn.1	|- G e. V

Assertion

Ref	Expression
2climnn0	|- (((A e. CC /\ A.k e. NN0 ((F` k) e. CC /\ (G` k) e. CC)) /\ (A.x e. RR (0 < x -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - (F` k))) < x)) /\ F ~~> A)) -> G ~~> A)

Distinct variable groups:   x,k,j,A   j,F,k,x   x,G,k,j

Proof of Theorem 2climnn0

Step	Hyp	Ref	Expression
1		rehalfclt 6034	. . . . . . 7 |- (y e. RR -> (y / 2) e. RR)
2		breq2 2623	. . . . . . . . 9 |- (x = (y / 2) -> (0 < x <-> 0 < (y / 2)))
3		opreq12 3970	. . . . . . . . . . . . 13 |- ((x = (y / 2) /\ x = (y / 2)) -> (x + x) = ((y / 2) + (y / 2)))
4	3	anidms 434	. . . . . . . . . . . 12 |- (x = (y / 2) -> (x + x) = ((y / 2) + (y / 2)))
5	4	breq2d 2630	. . . . . . . . . . 11 |- (x = (y / 2) -> ((abs` ((G` k) - A)) < (x + x) <-> (abs` ((G` k) - A)) < ((y / 2) + (y / 2))))
6	5	imbi2d 612	. . . . . . . . . 10 |- (x = (y / 2) -> ((j <_ k -> (abs` ((G` k) - A)) < (x + x)) <-> (j <_ k -> (abs` ((G` k) - A)) < ((y / 2) + (y / 2)))))
7	6	rexralbidv 1682	. . . . . . . . 9 |- (x = (y / 2) -> (E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - A)) < (x + x)) <-> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - A)) < ((y / 2) + (y / 2)))))
8	2, 7	imbi12d 626	. . . . . . . 8 |- (x = (y / 2) -> ((0 < x -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - A)) < (x + x))) <-> (0 < (y / 2) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - A)) < ((y / 2) + (y / 2))))))
9	8	rcla4v 1873	. . . . . . 7 |- ((y / 2) e. RR -> (A.x e. RR (0 < x -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - A)) < (x + x))) -> (0 < (y / 2) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - A)) < ((y / 2) + (y / 2))))))
10	1, 9	syl 10	. . . . . 6 |- (y e. RR -> (A.x e. RR (0 < x -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - A)) < (x + x))) -> (0 < (y / 2) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((G` k) - A)) < ((y / 2) + (y / 2))))))
11		0z 6146	. . . . . . . . . . . . . . . 16 |- 0 e. ZZ
12		nn0uz 6438	. . . . . . . . . . . . . . . . 17 |- NN0 = (ZZ>` 0)
13	12	eqimss2i 2112	. . . . . . . . . . . . . . . 16 |- (ZZ>` 0) (_ NN0
14		nn0ssz 6152	. . . . . . . . . . . . . . . 16 |- NN0 (_ ZZ
15	11, 13, 14	clmi2 7087	. . . . . . . . . . . . . . 15 |- (((A e. CC /\ F ~~> A) /\ (x e. RR /\ 0 < x)) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((F` k) - A)) < x))
16	15	adantllr 397	. . . . . . . . . . . . . 14 |- ((((A e. CC /\ A.k e. NN0 ((F` k) e. CC /\ (G` k) e. CC)) /\ F ~~> A) /\ (x e. RR /\ 0 < x)) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((F` k) - A)) < x))
17	16	anassrs 441	. . . . . . . . . . . . 13 |- (((((A e. CC /\ A.k e. NN0 ((F` k) e. CC /\ (G` k) e. CC)) /\ F ~~> A) /\ x e. RR) /\ 0 < x) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (abs` ((F` k) - A)) < x))
18		lt2addt 5643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((abs` ((G` k) - (F` k))) e. RR /\ (abs` ((F` k) - A)) e. RR) /\ (x e. RR /\ x e. RR)) -> (((abs` ((G` k) - (F` k))) < x /\ (abs` ((F` k) - A)) < x) -> ((abs` ((G` k) - (F` k))) + (abs` ((F` k) - A))) < (x + x)))
19		subclt 5367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((G` k) e. CC /\ (F` k) e. CC) -> ((G` k) - (F` k)) e. CC)
20	19	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F` k) e. CC /\ (G` k) e. CC) -> ((G` k) - (F` k)) e. CC)
21		absclt 6833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((G` k) - (F` k)) e. CC -> (abs` ((G` k) - (F` k))) e. RR)
22	20, 21	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F` k) e. CC /\ (G` k) e. CC) -> (abs` ((G` k) - (F` k))) e. RR)
23	22	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A e. CC /\ ((F` k) e. CC /\ (G` k) e. CC)) -> (abs` ((G` k) - (F` k))) e. RR)
24		subclt 5367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F` k) e. CC /\ A e. CC) -> ((F` k) - A) e. CC)
25	24	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((A e. CC /\ (F` k) e. CC) -> ((F` k) - A) e. CC)
26		absclt 6833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F` k) - A) e. CC -> (abs` ((F` k) - A)) e. RR)
27	25, 26	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((A e. CC /\ (F` k) e. CC) -> (abs` ((F` k) - A)) e. RR)
28	27	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A e. CC /\ ((F` k) e. CC /\ (G` k) e. CC)) -> (abs` ((F` k) - A)) e. RR)
29	23, 28	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. CC /\ ((F` k) e. CC /\ (G` k) e. CC)) -> ((abs` ((G` k) - (F` k))) e. RR /\ (abs` ((F` k) - A)) e. RR))
30	29	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((A e. CC /\ x e. RR) /\ ((F` k) e. CC /\ (G` k) e. CC)) -> ((abs` ((G` k) - (F` k))) e. RR /\ (abs` ((F` k) - A)) e. RR))
31		pm3.2 283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. RR -> (x e. RR -> (x e. RR /\ x e. RR)))
32	31	pm2.43i 64	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. RR -> (x e. RR /\ x e. RR))
33	32	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((A e. CC /\ x e. RR) /\ ((F` k) e. CC /\ (G` k) e. CC)) -> (x e. RR /\ x e. RR))
34	18, 30, 33	sylanc 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A e. CC /\ x e. RR) /\ ((F` k) e. CC /\ (G` k) e. CC)) -> (((abs` ((G` k) - (F` k))) < x /\ (abs` ((F` k) - A)) < x) -> ((abs` ((G` k) - (F` k))) + (abs` ((F` k) - A))) < (x + x)))
35		npncant 5400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((G` k) e. CC /\ (F` k) e. CC /\ A e. CC) -> (((G` k) - (F` k)) + ((F` k) - A)) = ((G` k) - A))
36	35	3com13 838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((A e. CC /\ (F` k) e. CC /\ (G` k) e. CC) -> (((G` k) - (F` k)) + ((F` k) - A)) = ((G` k) - A))
37	36	3expb 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((A e. CC /\ ((F` k) e. CC /\ (G` k) e. CC)) -> (((G` k) - (F` k)) + ((F` k) - A)) = ((G` k) - A))
38	37	fveq2d 3728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A e. CC /\ ((F` k) e. CC /\ (G` k) e. CC)) -> (abs` (((G` k) - (F` k)) + ((F` k) - A))) = (abs` ((G` k) - A)))
39		abstrit 6898	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((G` k) - (F` k)) e. CC /\ ((F` k) - A) e. CC) -> (abs` (