Theorem serzf0 7105

Description: If an infinite series converges, its underlying sequence converges to zero. Warning: The HTML proof page is 0.6 megabyte in size.

Hypotheses

Ref	Expression
serzf0.1	|- F e. V
serzf0.2	|- M e. ZZ
serzf0.3	|- (k e. (ZZ>` M) -> (F` k) e. CC)
serzf0.4	|- A e. V
serzf0.5	|- (<.M, + >. seq F) ~~> A

Assertion

Ref	Expression
serzf0	|- F ~~> 0

Distinct variable groups:   k,F   k,M

Proof of Theorem serzf0

Step	Hyp	Ref	Expression
1		serzf0.2	. . . 4 |- M e. ZZ
2		peano2z 6113	. . . 4 |- (M e. ZZ -> (M + 1) e. ZZ)
3	1, 2	ax-mp 7	. . 3 |- (M + 1) e. ZZ
4		0cn 5300	. . 3 |- 0 e. CC
5		uzidt 6359	. . . . . . . . 9 |- (M e. ZZ -> M e. (ZZ>` M))
6	1, 5	ax-mp 7	. . . . . . . 8 |- M e. (ZZ>` M)
7		peano2uz 6379	. . . . . . . 8 |- (M e. (ZZ>` M) -> (M + 1) e. (ZZ>` M))
8	6, 7	ax-mp 7	. . . . . . 7 |- (M + 1) e. (ZZ>` M)
9		uzss 6363	. . . . . . 7 |- ((M + 1) e. (ZZ>` M) -> (ZZ>` (M + 1)) (_ (ZZ>` M))
10	8, 9	ax-mp 7	. . . . . 6 |- (ZZ>` (M + 1)) (_ (ZZ>` M)
11	10	sseli 2055	. . . . 5 |- (h e. (ZZ>` (M + 1)) -> h e. (ZZ>` M))
12		fveq2 3709	. . . . . . 7 |- (k = h -> (F` k) = (F` h))
13	12	eleq1d 1532	. . . . . 6 |- (k = h -> ((F` k) e. CC <-> (F` h) e. CC))
14		serzf0.3	. . . . . 6 |- (k e. (ZZ>` M) -> (F` k) e. CC)
15	13, 14	vtoclga 1843	. . . . 5 |- (h e. (ZZ>` M) -> (F` h) e. CC)
16	11, 15	syl 10	. . . 4 |- (h e. (ZZ>` (M + 1)) -> (F` h) e. CC)
17	16	rgen 1690	. . 3 |- A.h e. (ZZ>` (M + 1))(F` h) e. CC
18		serzf0.1	. . . 4 |- F e. V
19	18	clm4at 7028	. . 3 |- (((M + 1) e. ZZ /\ 0 e. CC /\ A.h e. (ZZ>` (M + 1))(F` h) e. CC) -> (F ~~> 0 <-> A.x e. RR (0 < x -> E.j e. ZZ A.h e. (ZZ>` (M + 1))(j <_ h -> (abs` ((F` h) - 0)) < x))))
20	3, 4, 17, 19	mp3an 913	. 2 |- (F ~~> 0 <-> A.x e. RR (0 < x -> E.j e. ZZ A.h e. (ZZ>` (M + 1))(j <_ h -> (abs` ((F` h) - 0)) < x)))
21		serzf0.4	. . . . . 6 |- A e. V
22		serzf0.5	. . . . . 6 |- (<.M, + >. seq F) ~~> A
23		0z 6093	. . . . . . 7 |- 0 e. ZZ
24		uzssz 6362	. . . . . . 7 |- (ZZ>` 0) (_ ZZ
25		ssid 2070	. . . . . . 7 |- ZZ (_ ZZ
26	23, 24, 25	clmi2 7025	. . . . . 6 |- (((A e. V /\ (<.M, + >. seq F) ~~> A) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2)))
27	21, 22, 26	mpanl12 706	. . . . 5 |- (((x / 2) e. RR /\ 0 < (x / 2)) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2)))
28		rehalfclt 5981	. . . . . 6 |- (x e. RR -> (x / 2) e. RR)
29	28	adantr 389	. . . . 5 |- ((x e. RR /\ 0 < x) -> (x / 2) e. RR)
30		halfpos2t 5984	. . . . . 6 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
31	30	biimpa 416	. . . . 5 |- ((x e. RR /\ 0 < x) -> 0 < (x / 2))
32	27, 29, 31	sylanc 471	. . . 4 |- ((x e. RR /\ 0 < x) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2)))
33		breq1 2612	. . . . . . . . . . 11 |- (j = (m + 1) -> (j <_ h <-> (m + 1) <_ h))
34	33	imbi1d 611	. . . . . . . . . 10 |- (j = (m + 1) -> ((j <_ h -> (abs` ((F` h) - 0)) < x) <-> ((m + 1) <_ h -> (abs` ((F` h) - 0)) < x)))
35	34	ralbidv 1655	. . . . . . . . 9 |- (j = (m + 1) -> (A.h e. (ZZ>` (M + 1))(j <_ h -> (abs` ((F` h) - 0)) < x) <-> A.h e. (ZZ>` (M + 1))((m + 1) <_ h -> (abs` ((F` h) - 0)) < x)))
36	35	rcla4ev 1868	. . . . . . . 8 |- (((m + 1) e. ZZ /\ A.h e. (ZZ>` (M + 1))((m + 1) <_ h -> (abs` ((F` h) - 0)) < x)) -> E.j e. ZZ A.h e. (ZZ>` (M + 1))(j <_ h -> (abs` ((F` h) - 0)) < x))
37		peano2z 6113	. . . . . . . . 9 |- (m e. ZZ -> (m + 1) e. ZZ)
38	37	ad2antrl 406	. . . . . . . 8 |- ((x e. RR /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2)))) -> (m + 1) e. ZZ)
39		p1let 5773	. . . . . . . . . . . . . . . . . . 19 |- ((m e. RR /\ h e. RR /\ (m + 1) <_ h) -> m <_ h)
40	39	3expia 833	. . . . . . . . . . . . . . . . . 18 |- ((m e. RR /\ h e. RR) -> ((m + 1) <_ h -> m <_ h))
41		zret 6086	. . . . . . . . . . . . . . . . . 18 |- (m e. ZZ -> m e. RR)
42		zret 6086	. . . . . . . . . . . . . . . . . 18 |- (h e. ZZ -> h e. RR)
43	40, 41, 42	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((m e. ZZ /\ h e. ZZ) -> ((m + 1) <_ h -> m <_ h))
44	43	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((h e. ZZ /\ m e. ZZ) -> ((m + 1) <_ h -> m <_ h))
45	44	adantrr 395	. . . . . . . . . . . . . . 15 |- ((h e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2)))) -> ((m + 1) <_ h -> m <_ h))
46		breq2 2613	. . . . . . . . . . . . . . . . . 18 |- (n = h -> (m <_ n <-> m <_ h))
47		fveq2 3709	. . . . . . . . . . . . . . . . . . . . 21 |- (n = h -> ((<.M, + >. seq F)` n) = ((<.M, + >. seq F)` h))
48	47	opreq1d 3960	. . . . . . . . . . . . . . . . . . . 20 |- (n = h -> (((<.M, + >. seq F)` n) - A) = (((<.M, + >. seq F)` h) - A))
49	48	fveq2d 3713	. . . . . . . . . . . . . . . . . . 19 |- (n = h -> (abs` (((<.M, + >. seq F)` n) - A)) = (abs` (((<.M, + >. seq F)` h) - A)))
50	49	breq1d 2619	. . . . . . . . . . . . . . . . . 18 |- (n = h -> ((abs` (((<.M, + >. seq F)` n) - A)) < (x / 2) <-> (abs` (((<.M, + >. seq F)` h) - A)) < (x / 2)))
51	46, 50	imbi12d 624	. . . . . . . . . . . . . . . . 17 |- (n = h -> ((m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2)) <-> (m <_ h -> (abs` (((<.M, + >. seq F)` h) - A)) < (x / 2))))
52	51	rcla4va 1866	. . . . . . . . . . . . . . . 16 |- ((h e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2))) -> (m <_ h -> (abs` (((<.M, + >. seq F)` h) - A)) < (x / 2)))
53	52	adantrl 394	. . . . . . . . . . . . . . 15 |- ((h e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2)))) -> (m <_ h -> (abs` (((<.M, + >. seq F)` h) - A)) < (x / 2)))
54	45, 53	syld 27	. . . . . . . . . . . . . 14 |- ((h e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A)) < (x / 2)))) -> ((m + 1) <_ h -> (abs` (((<.M, + >. seq F)` h) - A)) < (x / 2)))
55		1re 5407	. . . . . . . . . . . . . . . . . . 19 |- 1 e. RR
56		leaddsubt 5607	. . . . . . . . . . . . . . . . . . 19 |- ((m e. RR /\ 1 e. RR /\ h e. RR) -> ((m + 1) <_ h <-> m <_ (h - 1)))
57	55, 56	mp3an2 901	. . . . . . . . . . . . . . . . . 18 |- ((m e. RR /\ h e. RR) -> ((m + 1) <_ h <-> m <_ (h - 1)))
58	57, 41, 42	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((m e. ZZ /\ h e. ZZ) -> ((m + 1) <_ h <-> m <_ (h - 1)))
59	58	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((h e. ZZ /\ m e. ZZ) -> ((m + 1) <_ h <-> m <_ (h - 1)))
60	59	adantrr 395	. . . . . . . . . . . . . . 15 |- ((h e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` (((<.M, + >. seq F)` n) - A