Theorem climrecl 7055

Description: The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172.

Hypothesis

Ref	Expression
climrecl.1	|- A e. V

Assertion

Ref	Expression
climrecl	|- ((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)(F` k) e. RR) -> A e. RR)

Distinct variable groups:   k,F   k,M

Proof of Theorem climrecl

Step	Hyp	Ref	Expression
1		climrecl.1	. . . 4 |- A e. V
2		climcl 6924	. . . 4 |- ((A e. V /\ F ~~> A) -> A e. CC)
3	1, 2	mpan 694	. . 3 |- (F ~~> A -> A e. CC)
4	3	3ad2ant2 800	. 2 |- ((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)(F` k) e. RR) -> A e. CC)
5		imclt 6697	. . . . . . . . . 10 |- (A e. CC -> (Im` A) e. RR)
6	5	recnd 5295	. . . . . . . . 9 |- (A e. CC -> (Im` A) e. CC)
7		absge0t 6797	. . . . . . . . 9 |- ((Im` A) e. CC -> 0 <_ (abs` (Im` A)))
8	6, 7	syl 10	. . . . . . . 8 |- (A e. CC -> 0 <_ (abs` (Im` A)))
9	8	adantl 388	. . . . . . 7 |- (((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)(F` k) e. RR) /\ A e. CC) -> 0 <_ (abs` (Im` A)))
10		breq2 2618	. . . . . . . . . . . . . . . 16 |- (m = j -> (j <_ m <-> j <_ j))
11		fveq2 3715	. . . . . . . . . . . . . . . . . . . 20 |- (m = j -> (F` m) = (F` j))
12	11	opreq1d 3966	. . . . . . . . . . . . . . . . . . 19 |- (m = j -> ((F` m) - A) = ((F` j) - A))
13	12	fveq2d 3719	. . . . . . . . . . . . . . . . . 18 |- (m = j -> (abs` ((F` m) - A)) = (abs` ((F` j) - A)))
14	13	breq1d 2624	. . . . . . . . . . . . . . . . 17 |- (m = j -> ((abs` ((F` m) - A)) < (abs` (Im` A)) <-> (abs` ((F` j) - A)) < (abs` (Im` A))))
15	14	negbid 610	. . . . . . . . . . . . . . . 16 |- (m = j -> (-. (abs` ((F` m) - A)) < (abs` (Im` A)) <-> -. (abs` ((F` j) - A)) < (abs` (Im` A))))
16	10, 15	anbi12d 627	. . . . . . . . . . . . . . 15 |- (m = j -> ((j <_ m /\ -. (abs` ((F` m) - A)) < (abs` (Im` A))) <-> (j <_ j /\ -. (abs` ((F` j) - A)) < (abs` (Im` A)))))
17	16	rcla4ev 1873	. . . . . . . . . . . . . 14 |- ((j e. ZZ /\ (j <_ j /\ -. (abs` ((F` j) - A)) < (abs` (Im` A)))) -> E.m e. ZZ (j <_ m /\ -. (abs` ((F` m) - A)) < (abs` (Im` A))))
18		eluzelz 6363	. . . . . . . . . . . . . . 15 |- (j e. (ZZ>` M) -> j e. ZZ)
19	18	ad2antlr 405	. . . . . . . . . . . . . 14 |- ((((F` j) e. RR /\ j e. (ZZ>` M)) /\ A e. CC) -> j e. ZZ)
20		zret 6094	. . . . . . . . . . . . . . . . 17 |- (j e. ZZ -> j e. RR)
21		leidt 5512	. . . . . . . . . . . . . . . . 17 |- (j e. RR -> j <_ j)
22	18, 20, 21	3syl 20	. . . . . . . . . . . . . . . 16 |- (j e. (ZZ>` M) -> j <_ j)
23	22	ad2antlr 405	. . . . . . . . . . . . . . 15 |- ((((F` j) e. RR /\ j e. (ZZ>` M)) /\ A e. CC) -> j <_ j)
24		absnegt 6775	. . . . . . . . . . . . . . . . . . . . 21 |- ((Im` A) e. CC -> (abs` -u(Im` A)) = (abs` (Im` A)))
25	6, 24	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (A e. CC -> (abs` -u(Im` A)) = (abs` (Im` A)))
26	25	adantl 388	. . . . . . . . . . . . . . . . . . 19 |- (((F` j) e. RR /\ A e. CC) -> (abs` -u(Im` A)) = (abs` (Im` A)))
27		reim0t 6719	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` j) e. RR -> (Im` (F` j)) = 0)
28	27	opreq1d 3966	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F` j) e. RR -> ((Im` (F` j)) - (Im` A)) = (0 - (Im` A)))
29		df-neg 5338	. . . . . . . . . . . . . . . . . . . . . . 23 |- -u(Im` A) = (0 - (Im` A))
30	28, 29	syl6reqr 1523	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` j) e. RR -> -u(Im` A) = ((Im` (F` j)) - (Im` A)))
31	30	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` j) e. RR /\ A e. CC) -> -u(Im` A) = ((Im` (F` j)) - (Im` A)))
32		imsubt 6752	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` j) e. CC /\ A e. CC) -> (Im` ((F` j) - A)) = ((Im` (F` j)) - (Im` A)))
33		recnt 5293	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` j) e. RR -> (F` j) e. CC)
34	32, 33	sylan 448	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` j) e. RR /\ A e. CC) -> (Im` ((F` j) - A)) = ((Im` (F` j)) - (Im` A)))
35	31, 34	eqtr4d 1507	. . . . . . . . . . . . . . . . . . . 20 |- (((F` j) e. RR /\ A e. CC) -> -u(Im` A) = (Im` ((F` j) - A)))
36	35	fveq2d 3719	. . . . . . . . . . . . . . . . . . 19 |- (((F` j) e. RR /\ A e. CC) -> (abs` -u(Im` A)) = (abs` (Im` ((F` j) - A))))
37	26, 36	eqtr3d 1506	. . . . . . . . . . . . . . . . . 18 |- (((F` j) e. RR /\ A e. CC) -> (abs` (Im` A)) = (abs` (Im` ((F` j) - A))))
38		subclt 5347	. . . . . . . . . . . . . . . . . . . 20 |- (((F` j) e. CC /\ A e. CC) -> ((F` j) - A) e. CC)
39	38, 33	sylan 448	. . . . . . . . . . . . . . . . . . 19 |- (((F` j) e. RR /\ A e. CC) -> ((F` j) - A) e. CC)
40		absimlet 6813	. . . . . . . . . . . . . . . . . . 19 |- (((F` j) - A) e. CC -> (abs` (Im` ((F` j) - A))) <_ (abs` ((F` j) - A)))
41	39, 40	syl 10	. . . . . . . . . . . . . . . . . 18 |- (((F` j) e. RR /\ A e. CC) -> (abs` (Im` ((F` j) - A))) <_ (abs` ((F` j) - A)))
42	37, 41	eqbrtrd 2630	. . . . . . . . . . . . . . . . 17 |- (((F` j) e. RR /\ A e. CC) -> (abs` (Im` A)) <_ (abs` ((F` j) - A)))
43		lenltt 5490	. . . . . . . . . . . . . . . . . 18 |- (((abs` (Im` A)) e. RR /\ (abs` ((F` j) - A)) e. RR) -> ((abs` (Im` A)) <_ (abs` ((F` j) - A)) <-> -. (abs` ((F` j) - A)) < (abs` (Im` A))))
44		absclt 6776	. . . . . . . . . . . . . . . . . . . 20 |- ((Im` A) e. CC -> (abs` (Im` A)) e. RR)
45	6, 44	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (A e. CC -> (abs` (Im` A)) e. RR)
46	45	adantl 388	. . . . . . . . . . . . . . . . . 18 |- (((F` j) e. RR /\ A e. CC) -> (abs` (Im` A)) e. RR)
47		absclt 6776	. . . . . . . . . . . . . . . . . . 19 |- (((F` j) - A) e. CC -> (abs` ((F` j) - A)) e. RR)
48	39, 47	syl 10	. . . . . . . . . . . . . . . . . 18 |- (((F` j) e. RR /\ A e. CC) -> (abs` ((F` j) - A)) e. RR)
49	43, 46, 48	sylanc 471	. . . . . . . . . . . . . . . . 17 |- (((F` j) e. RR /\ A e. CC) -> ((abs` (Im` A)) <_ (abs` ((F` j) - A)) <-> -. (abs` ((F` j) - A)) < (abs` (Im` A))))
50	42, 49	mpbid 195	. . . . . . . . . . . . . . . 16 |- (((F` j) e. RR /\ A e. CC) -> -. (abs` ((F` j) - A)) < (abs` (Im` A)))
51	50	adantlr 393	. . . . . . . . . . . . . . 15 |- ((((F` j) e. RR /\ j e. (ZZ>` M)) /\ A e. CC) -> -. (abs` ((F` j) - A)) < (abs` (Im` A)))
52	23, 51	jca 288	. . . . . . . . . . . . . 14 |- ((((F` j) e. RR /\ j e. (ZZ>` M)) /\ A e. CC) -> (j <_ j /\ -. (abs` ((F` j) - A)) < (abs` (Im` A))))
53	17, 19, 52	sylanc 471	. . . . . . . . . . . . 13 |- ((((F` j) e. RR /\ j e. (ZZ>` M)) /\ A e. CC) -> E.m e. ZZ (j <_ m /\ -. (abs` ((F` m) - A)) < (abs` (Im` A))))
54		rexanali 1681	. . . . . . . . . . . . 13 |- (E.m e. ZZ (j <_ m /\ -. (abs` ((F` m) - A)) < (abs` (Im` A))) <-> -. A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < (abs` (Im` A))))
55	53, 54	sylib 198	. . . . . . . . . . . 12 |- ((((F` j) e. RR /\ j e. (ZZ>` M)) /\ A e. CC) -> -. A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < (abs` (Im` A))))
56		fveq2 3715	. . . . . . . . . . . . . . 15 |- (k = j -> (F` k) = (F` j))
57	56	eleq1d 1537	. . . . . . . . . . . . . 14 |- (k = j -> (