Theorem climunii 7035

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

Hypotheses

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

Assertion

Ref	Expression
climunii	|- A = B

Proof of Theorem climunii

Step	Hyp	Ref	Expression
1		z2get 6135	. . . . 5 |- ((k e. ZZ /\ m e. ZZ) -> E.j e. ZZ (k <_ j /\ m <_ j))
2	1	rgen2a 1691	. . . 4 |- A.k e. ZZ A.m e. ZZ E.j e. ZZ (k <_ j /\ m <_ j)
3		climuni.1	. . . . . . . . 9 |- A e. V
4		climunii.3	. . . . . . . . . 10 |- (F ~~> A /\ F ~~> B)
5	4	pm3.26i 320	. . . . . . . . 9 |- F ~~> A
6		climcl 6916	. . . . . . . . 9 |- ((A e. V /\ F ~~> A) -> A e. CC)
7	3, 5, 6	mp2an 695	. . . . . . . 8 |- A e. CC
8		climuni.2	. . . . . . . . 9 |- B e. V
9	4	pm3.27i 324	. . . . . . . . 9 |- F ~~> B
10		climcl 6916	. . . . . . . . 9 |- ((B e. V /\ F ~~> B) -> B e. CC)
11	8, 9, 10	mp2an 695	. . . . . . . 8 |- B e. CC
12	7, 11	subcl 5338	. . . . . . 7 |- (A - B) e. CC
13	12	abscl 6774	. . . . . 6 |- (abs` (A - B)) e. RR
14		2re 5926	. . . . . 6 |- 2 e. RR
15		2pos 5936	. . . . . 6 |- 0 < 2
16	13, 14, 15	divgt0i2 5813	. . . . 5 |- (0 < (abs` (A - B)) -> 0 < ((abs` (A - B)) / 2))
17		2ne0 5937	. . . . . . . 8 |- 2 =/= 0
18	13, 14, 17	redivcl 5754	. . . . . . 7 |- ((abs` (A - B)) / 2) e. RR
19		0z 6093	. . . . . . . . 9 |- 0 e. ZZ
20		uzssz 6362	. . . . . . . . 9 |- (ZZ>` 0) (_ ZZ
21		ssid 2070	. . . . . . . . 9 |- ZZ (_ ZZ
22	19, 20, 21	clmi1 7024	. . . . . . . 8 |- (((A e. V /\ F ~~> A) /\ (((abs` (A - B)) / 2) e. RR /\ 0 < ((abs` (A - B)) / 2))) -> E.k e. ZZ A.j e. ZZ (k <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - A)) < ((abs` (A - B)) / 2))))
23	3, 5, 22	mpanl12 706	. . . . . . 7 |- ((((abs` (A - B)) / 2) e. RR /\ 0 < ((abs` (A - B)) / 2)) -> E.k e. ZZ A.j e. ZZ (k <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - A)) < ((abs` (A - B)) / 2))))
24	18, 23	mpan 693	. . . . . 6 |- (0 < ((abs` (A - B)) / 2) -> E.k e. ZZ A.j e. ZZ (k <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - A)) < ((abs` (A - B)) / 2))))
25	19, 20, 21	clmi1 7024	. . . . . . . 8 |- (((B e. V /\ F ~~> B) /\ (((abs` (A - B)) / 2) e. RR /\ 0 < ((abs` (A - B)) / 2))) -> E.m e. ZZ A.j e. ZZ (m <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2))))
26	8, 9, 25	mpanl12 706	. . . . . . 7 |- ((((abs` (A - B)) / 2) e. RR /\ 0 < ((abs` (A - B)) / 2)) -> E.m e. ZZ A.j e. ZZ (m <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2))))
27	18, 26	mpan 693	. . . . . 6 |- (0 < ((abs` (A - B)) / 2) -> E.m e. ZZ A.j e. ZZ (m <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2))))
28	24, 27	jca 288	. . . . 5 |- (0 < ((abs` (A - B)) / 2) -> (E.k e. ZZ A.j e. ZZ (k <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - A)) < ((abs` (A - B)) / 2))) /\ E.m e. ZZ A.j e. ZZ (m <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2)))))
29		r19.26 1742	. . . . . . . . 9 |- (A.j e. ZZ ((k <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - A)) < ((abs` (A - B)) / 2))) /\ (m <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2)))) <-> (A.j e. ZZ (k <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - A)) < ((abs` (A - B)) / 2))) /\ A.j e. ZZ (m <_ j -> ((F` j) e. CC /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2)))))
30	13	ltnr 5583	. . . . . . . . . . . 12 |- -. (abs` (A - B)) < (abs` (A - B))
31		anandi 509	. . . . . . . . . . . . 13 |- (((F` j) e. CC /\ ((abs` ((F` j) - A)) < ((abs` (A - B)) / 2) /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2))) <-> (((F` j) e. CC /\ (abs` ((F` j) - A)) < ((abs` (A - B)) / 2)) /\ ((F` j) e. CC /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2))))
32		abssubt 6832	. . . . . . . . . . . . . . . . . 18 |- (((F` j) e. CC /\ A e. CC) -> (abs` ((F` j) - A)) = (abs` (A - (F` j))))
33	7, 32	mpan2 694	. . . . . . . . . . . . . . . . 17 |- ((F` j) e. CC -> (abs` ((F` j) - A)) = (abs` (A - (F` j))))
34	33	breq1d 2619	. . . . . . . . . . . . . . . 16 |- ((F` j) e. CC -> ((abs` ((F` j) - A)) < ((abs` (A - B)) / 2) <-> (abs` (A - (F` j))) < ((abs` (A - B)) / 2)))
35	34	anbi1d 615	. . . . . . . . . . . . . . 15 |- ((F` j) e. CC -> (((abs` ((F` j) - A)) < ((abs` (A - B)) / 2) /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2)) <-> ((abs` (A - (F` j))) < ((abs` (A - B)) / 2) /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2))))
36		abs3lemt 6844	. . . . . . . . . . . . . . . . 17 |- (((A e. CC /\ B e. CC) /\ ((F` j) e. CC /\ (abs` (A - B)) e. RR)) -> (((abs` (A - (F` j))) < ((abs` (A - B)) / 2) /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2)) -> (abs` (A - B)) < (abs` (A - B))))
37	7, 11, 36	mpanl12 706	. . . . . . . . . . . . . . . 16 |- (((F` j) e. CC /\ (abs` (A - B)) e. RR) -> (((abs` (A - (F` j))) < ((abs` (A - B)) / 2) /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2)) -> (abs` (A - B)) < (abs` (A - B))))
38	13, 37	mpan2 694	. . . . . . . . . . . . . . 15 |- ((F` j) e. CC -> (((abs` (A - (F` j))) < ((abs` (A - B)) / 2) /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2)) -> (abs` (A - B)) < (abs` (A - B))))
39	35, 38	sylbid 203	. . . . . . . . . . . . . 14 |- ((F` j) e. CC -> (((abs` ((F` j) - A)) < ((abs` (A - B)) / 2) /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2)) -> (abs` (A - B)) < (abs` (A - B))))
40	39	imp 350	. . . . . . . . . . . . 13 |- (((F` j) e. CC /\ ((abs` ((F` j) - A)) < ((abs` (A - B)) / 2) /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2))) -> (abs` (A - B)) < (abs` (A - B)))
41	31, 40	sylbir 201	. . . . . . . . . . . 12 |- ((((F` j) e. CC /\ (abs` ((F` j) - A)) < ((abs` (A - B)) / 2)) /\ ((F` j) e. CC /\ (abs` ((F` j) - B)) < ((abs` (A - B)) / 2))) -> (abs` (A - B)) < (abs` (A - B