Theorem climunii 4883

Description: A sequence of complex numbers converges to at most one limit.

Hypotheses

Ref	Expression
climuni.1	|- A e. V
climuni.2	|- B e. V
climuni.3	|- F e. V
climunii.3	|- (F ~~> A /\ F ~~> B)

Assertion

Ref	Expression
climunii	|- A = B

Proof of Theorem climunii

Step	Hyp	Ref	Expression
1		nn2get 4438	. . . . 5 |- ((y e. NN /\ w e. NN) -> E.z e. NN (y <_ z /\ w <_ z))
2	1	rgen2 1248	. . . 4 |- A.y e. NN A.w e. NN E.z e. NN (y <_ z /\ w <_ z)
3		climunii.3	. . . . . . . . . 10 |- (F ~~> A /\ F ~~> B)
4	3	pm3.26i 257	. . . . . . . . 9 |- F ~~> A
5		climuni.3	. . . . . . . . . 10 |- F e. V
6		climuni.1	. . . . . . . . . 10 |- A e. V
7	5, 6	climcn 4879	. . . . . . . . 9 |- (F ~~> A -> A e. CC)
8	4, 7	ax-mp 6	. . . . . . . 8 |- A e. CC
9	3	pm3.27i 261	. . . . . . . . 9 |- F ~~> B
10		climuni.2	. . . . . . . . . 10 |- B e. V
11	5, 10	climcn 4879	. . . . . . . . 9 |- (F ~~> B -> B e. CC)
12	9, 11	ax-mp 6	. . . . . . . 8 |- B e. CC
13	8, 12	subcl 4139	. . . . . . 7 |- (A - B) e. CC
14	13	abscl 4840	. . . . . 6 |- (abs` (A - B)) e. RR
15		2re 4470	. . . . . 6 |- 2 e. RR
16		2pos 4479	. . . . . 6 |- 0 < 2
17	14, 15, 16	divgt0lem 4389	. . . . 5 |- (0 < (abs` (A - B)) -> 0 < ((abs` (A - B)) / 2))
18	15, 16	gt0ne0i 4345	. . . . . . . 8 |- 2 =/= 0
19	14, 15, 18	redivcl 4274	. . . . . . 7 |- ((abs` (A - B)) / 2) e. RR
20		breq2 2066	. . . . . . . . 9 |- (x = ((abs` (A - B)) / 2) -> (0 < x <-> 0 < ((abs` (A - B)) / 2)))
21		breq2 2066	. . . . . . . . . . . 12 |- (x = ((abs` (A - B)) / 2) -> ((abs` ((F` z) - A)) < x <-> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2)))
22	21	imbi2d 464	. . . . . . . . . . 11 |- (x = ((abs` (A - B)) / 2) -> ((y <_ z -> (abs` ((F` z) - A)) < x) <-> (y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2))))
23	22	biraldv 1219	. . . . . . . . . 10 |- (x = ((abs` (A - B)) / 2) -> (A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < x) <-> A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2))))
24	23	birexdv 1220	. . . . . . . . 9 |- (x = ((abs` (A - B)) / 2) -> (E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < x) <-> E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2))))
25	20, 24	imbi12d 474	. . . . . . . 8 |- (x = ((abs` (A - B)) / 2) -> ((0 < x -> E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < x)) <-> (0 < ((abs` (A - B)) / 2) -> E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2)))))
26	5, 6	climconv 4880	. . . . . . . . 9 |- (F ~~> A -> A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < x)))
27	4, 26	ax-mp 6	. . . . . . . 8 |- A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < x))
28	25, 27	vtoclri 1393	. . . . . . 7 |- (((abs` (A - B)) / 2) e. RR -> (0 < ((abs` (A - B)) / 2) -> E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2))))
29	19, 28	ax-mp 6	. . . . . 6 |- (0 < ((abs` (A - B)) / 2) -> E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2)))
30		breq2 2066	. . . . . . . . . . . 12 |- (x = ((abs` (A - B)) / 2) -> ((abs` ((F` z) - B)) < x <-> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2)))
31	30	imbi2d 464	. . . . . . . . . . 11 |- (x = ((abs` (A - B)) / 2) -> ((w <_ z -> (abs` ((F` z) - B)) < x) <-> (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2))))
32	31	biraldv 1219	. . . . . . . . . 10 |- (x = ((abs` (A - B)) / 2) -> (A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < x) <-> A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2))))
33	32	birexdv 1220	. . . . . . . . 9 |- (x = ((abs` (A - B)) / 2) -> (E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < x) <-> E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2))))
34	20, 33	imbi12d 474	. . . . . . . 8 |- (x = ((abs` (A - B)) / 2) -> ((0 < x -> E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < x)) <-> (0 < ((abs` (A - B)) / 2) -> E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2)))))
35	5, 10	climconv 4880	. . . . . . . . 9 |- (F ~~> B -> A.x e. RR (0 < x -> E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < x)))
36	9, 35	ax-mp 6	. . . . . . . 8 |- A.x e. RR (0 < x -> E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < x))
37	34, 36	vtoclri 1393	. . . . . . 7 |- (((abs` (A - B)) / 2) e. RR -> (0 < ((abs` (A - B)) / 2) -> E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2))))
38	19, 37	ax-mp 6	. . . . . 6 |- (0 < ((abs` (A - B)) / 2) -> E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2)))
39	29, 38	jca 236	. . . . 5 |- (0 < ((abs` (A - B)) / 2) -> (E.y e. NN A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2)) /\ E.w e. NN A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2))))
40		r19.26 1289	. . . . . . . . 9 |- (A.z e. NN ((y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2)) /\ (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2))) <-> (A.z e. NN (y <_ z -> (abs` ((F` z) - A)) < ((abs` (A - B)) / 2)) /\ A.z e. NN (w <_ z -> (abs` ((F` z) - B)) < ((abs` (A - B)) / 2))))
41	14	ltnr 4338	. . . . . . . . . . . . 13 |- -. (abs` (A - B)) < (abs` (A - B))
42	5, 6	climseq 4878	. . . . . . . . . . . . . . . . . . 19 |- (F ~~> A -> F:NN-->CC)
43	4, 42	ax-mp 6	. . . . . . . . . . . . . . . . . 18 |- F:NN-->CC
44		ffvrn 2890	. . . . . . . . . . . . . . . . . 18 |- ((F:NN-->CC /\ z e. NN) -> (F` z) e. CC)
45	43, 44	mpan 518	. . . . . . . . . . . . . . . . 17 |- (z e. NN -> (F` z) e. CC)
46		abssubt 4864	. . . . . . . . . . . . . . . . . 18 |- (((F` z) e. CC /\ A e. CC) -> (abs` ((F` z) - A)) = (abs` (A - (F` z))))
47	8, 46	mpan2 519	. . . . . . . . . . . . . . . . 17 |- ((F` z) e. CC -> (abs` ((F` z) - A)) = (abs` (A - (F` z))))
48	45, 47	syl 12	. . . . . . . . . . . . . . . 16 |- (z e. NN -> (abs` ((F` z) - A)) = (abs` (A - (F` z))))
49	48	breq1d 2071	. . . . . . . . . . . . . . 15 |- (z e. NN -> ((abs` ((F` z) - A)) < ((abs` (A - B)) / 2) <-> (abs` (A - (F` z))) < ((abs` (A - B)) / 2)))
50	49	anbi1d 469	. . . . . . . . . . . . . 14 |- (z e. NN -> (((abs` ((F` z) - A)) < ((