Theorem climge0 7112

Description: A nonnegative sequence converges to a nonnegative number.

Hypothesis

Ref	Expression
climge0.1	|- A e. V

Assertion

Ref	Expression
climge0	|- ((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 <_ (F` k))) -> 0 <_ A)

Distinct variable groups:   k,F   k,M

Proof of Theorem climge0

Step	Hyp	Ref	Expression
1		climge0.1	. . . 4 |- A e. V
2	1	climrecl 7110	. . 3 |- ((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)(F` k) e. RR) -> A e. RR)
3		pm3.26 319	. . . 4 |- (((F` k) e. RR /\ 0 <_ (F` k)) -> (F` k) e. RR)
4	3	r19.20si 1709	. . 3 |- (A.k e. (ZZ>` M)((F` k) e. RR /\ 0 <_ (F` k)) -> A.k e. (ZZ>` M)(F` k) e. RR)
5	2, 4	syl3an3 863	. 2 |- ((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 <_ (F` k))) -> A e. RR)
6		lt0neg1t 5680	. . . . . . 7 |- (A e. RR -> (A < 0 <-> 0 < -uA))
7	6	adantl 390	. . . . . 6 |- (((M e. ZZ /\ F ~~> A) /\ A e. RR) -> (A < 0 <-> 0 < -uA))
8		clmi2at 7091	. . . . . . . . . . 11 |- ((M e. ZZ /\ ((A e. V /\ F ~~> A) /\ (-uA e. RR /\ 0 < -uA))) -> E.j e. (ZZ>` M)A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < -uA))
9	1	jctl 290	. . . . . . . . . . 11 |- (F ~~> A -> (A e. V /\ F ~~> A))
10	8, 9	sylanr1 464	. . . . . . . . . 10 |- ((M e. ZZ /\ (F ~~> A /\ (-uA e. RR /\ 0 < -uA))) -> E.j e. (ZZ>` M)A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < -uA))
11	10	anassrs 443	. . . . . . . . 9 |- (((M e. ZZ /\ F ~~> A) /\ (-uA e. RR /\ 0 < -uA)) -> E.j e. (ZZ>` M)A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < -uA))
12	11	anassrs 443	. . . . . . . 8 |- ((((M e. ZZ /\ F ~~> A) /\ -uA e. RR) /\ 0 < -uA) -> E.j e. (ZZ>` M)A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < -uA))
13	12	ex 373	. . . . . . 7 |- (((M e. ZZ /\ F ~~> A) /\ -uA e. RR) -> (0 < -uA -> E.j e. (ZZ>` M)A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < -uA)))
14		renegclt 5449	. . . . . . 7 |- (A e. RR -> -uA e. RR)
15	13, 14	sylan2 453	. . . . . 6 |- (((M e. ZZ /\ F ~~> A) /\ A e. RR) -> (0 < -uA -> E.j e. (ZZ>` M)A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < -uA)))
16	7, 15	sylbid 203	. . . . 5 |- (((M e. ZZ /\ F ~~> A) /\ A e. RR) -> (A < 0 -> E.j e. (ZZ>` M)A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < -uA)))
17	16	3adantl3 807	. . . 4 |- (((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 <_ (F` k))) /\ A e. RR) -> (A < 0 -> E.j e. (ZZ>` M)A.m e. ZZ (j <_ m -> (abs` ((F` m) - A)) < -uA)))
18		breq2 2628	. . . . . . . . . . . 12 |- (m = j -> (j <_ m <-> j <_ j))
19		fveq2 3730	. . . . . . . . . . . . . . . 16 |- (m = j -> (F` m) = (F` j))
20	19	opreq1d 3981	. . . . . . . . . . . . . . 15 |- (m = j -> ((F` m) - A) = ((F` j) - A))
21	20	fveq2d 3734	. . . . . . . . . . . . . 14 |- (m = j -> (abs` ((F` m) - A)) = (abs` ((F` j) - A)))
22	21	breq1d 2634	. . . . . . . . . . . . 13 |- (m = j -> ((abs` ((F` m) - A)) < -uA <-> (abs` ((F` j) - A)) < -uA))
23	22	negbid 613	. . . . . . . . . . . 12 |- (m = j -> (-. (abs` ((F` m) - A)) < -uA <-> -. (abs` ((F` j) - A)) < -uA))
24	18, 23	anbi12d 630	. . . . . . . . . . 11 |- (m = j -> ((j <_ m /\ -. (abs` ((F` m) - A)) < -uA) <-> (j <_ j /\ -. (abs` ((F` j) - A)) < -uA)))
25	24	rcla4ev 1880	. . . . . . . . . 10 |- ((j e. ZZ /\ (j <_ j /\ -. (abs` ((F` j) - A)) < -uA)) -> E.m e. ZZ (j <_ m /\ -. (abs` ((F` m) - A)) < -uA))
26		eluzelz 6424	. . . . . . . . . . 11 |- (j e. (ZZ>` M) -> j e. ZZ)
27	26	adantl 390	. . . . . . . . . 10 |- (((A.k e. (ZZ>` M)((F` k) e. RR /\ 0 <_ (F` k)) /\ (A e. RR /\ A < 0)) /\ j e. (ZZ>` M)) -> j e. ZZ)
28		zret 6141	. . . . . . . . . . . . 13 |- (j e. ZZ -> j e. RR)
29		leidt 5543	. . . . . . . . . . . . 13 |- (j e. RR -> j <_ j)
30	26, 28, 29	3syl 20	. . . . . . . . . . . 12 |- (j e. (ZZ>` M) -> j <_ j)
31	30	adantl 390	. . . . . . . . . . 11 |- (((A.k e. (ZZ>` M)((F` k) e. RR /\ 0 <_ (F` k)) /\ (A e. RR /\ A < 0)) /\ j e. (ZZ>` M)) -> j <_ j)
32		addge02t 5685	. . . . . . . . . . . . . . . . . . . 20 |- ((-uA e. RR /\ (F` j) e. RR) -> (0 <_ (F` j) <-> -uA <_ ((F` j) + -uA)))
33	32, 14	sylan 450	. . . . . . . . . . . . . . . . . . 19 |- ((A e. RR /\ (F` j) e. RR) -> (0 <_ (F` j) <-> -uA <_ ((F` j) + -uA)))
34	33	biimpa 418	. . . . . . . . . . . . . . . . . 18 |- (((A e. RR /\ (F` j) e. RR) /\ 0 <_ (F` j)) -> -uA <_ ((F` j) + -uA))
35	34	anasss 442	. . . . . . . . . . . . . . . . 17 |- ((A e. RR /\ ((F` j) e. RR /\ 0 <_ (F` j))) -> -uA <_ ((F` j) + -uA))
36	35	ancoms 438	. . . . . . . . . . . . . . . 16 |- ((((F` j) e. RR /\ 0 <_ (F` j)) /\ A e. RR) -> -uA <_ ((F` j) + -uA))
37	36	adantrr 397	. . . . . . . . . . . . . . 15 |- ((((F` j) e. RR /\ 0 <_ (F` j)) /\ (A e. RR /\ A < 0)) -> -uA <_ ((F` j) + -uA))
38		absidt 6862	. . . . . . . . . . . . . . . . 17 |- ((((F` j) + -uA) e. RR /\ 0 <_ ((F` j) + -uA)) -> (abs` ((F` j) + -uA)) = ((F` j) + -uA))
39		axaddrcl 5284	. . . . . . . . . . . . . . . . . . 19 |- (((F` j) e. RR /\ -uA e. RR) -> ((F` j) + -uA) e. RR)
40	39, 14	sylan2 453	. . . . . . . . . . . . . . . . . 18 |- (((F` j) e. RR /\ A e. RR) -> ((F` j) + -uA) e. RR)
41	40	ad2ant2r 411	. . . . . . . . . . . . . . . . 17 |- ((((F` j) e. RR /\ 0 <_ (F` j)) /\ (A e. RR /\ A < 0)) -> ((F` j) + -uA) e. RR)
42		addge0t 5662	. . . . . . . . . . . . . . . . . . 19 |- ((((F` j) e. RR /\ -uA e. RR) /\ (0 <_ (F` j) /\ 0 <_ -uA)) -> 0 <_ ((F` j) + -uA))
43	42	an4s 510	. . . . . . . . . . . . . . . . . 18 |- ((((F` j) e. RR /\ 0 <_ (F` j)) /\ (-uA e. RR /\ 0 <_ -uA)) -> 0 <_ ((F` j) + -uA))
44	14	adantr 391	. . . . . . . . . . . . . . . . . . 19 |- ((A e. RR /\ A < 0) -> -uA e. RR)
45		0re 5452	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. RR
46		ltlet 5532	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ 0 e. RR) -> (A < 0 -> A <_ 0))
47	45, 46	mpan2 698	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. RR -> (A < 0 -> A <_ 0))
48		le0neg1t 5682	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. RR -> (A <_ 0 <-> 0 <_ -uA))
49	47, 48	sylibd 202	. . . . . . . . . . . . . . . . . . . 20 |- (A e. RR -> (A < 0 -> 0 <_ -uA))
50	49	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((A e. RR /\ A < 0) -> 0 <_ -uA)
51	44, 50	jca 288	. . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ A < 0) -> (-uA e. RR /\ 0 <_ -uA))
52	43, 51	sylan2 453	. . . . . . . . . . . . . . . . 17 |- ((((F` j) e. RR /\ 0 <_ (F` j)) /\ (A e. RR /\ A < 0)) -> 0 <_ ((F` j) + -uA))
53	38, 41, 52	sylanc 473	. . . . . . . . . . . . . . . 16 |- ((((F` j) e. RR /\ 0 <_ (F` j)) /\ (A e. RR /\ A < 0)) -> (abs` ((F` j) + -uA)) = ((F` j) + -uA))
54		negsubt 5394	. . . . . . . . . . . . . . . . . . 19 |- (((F` j) e. CC /\ A e. CC) -> ((F` j) + -uA) = ((F