Theorem ser1f0 7057

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

Hypotheses

Ref	Expression
ser1f0.1	|- F:NN-->CC
ser1f0.2	|- A e. CC
ser1f0.3	|- ( + seq1 F) ~~> A

Assertion

Ref	Expression
ser1f0	|- F ~~> 0

Proof of Theorem ser1f0

Step	Hyp	Ref	Expression
1		0cn 5251	. . 3 |- 0 e. CC
2		inss2 2202	. . . . . . 7 |- (ZZ i^i (ZZ>` 2)) (_ (ZZ>` 2)
3		1z 6057	. . . . . . . . . . 11 |- 1 e. ZZ
4	3	eluz1 6305	. . . . . . . . . 10 |- (2 e. (ZZ>` 1) <-> (2 e. ZZ /\ 1 <_ 2))
5		2z 6058	. . . . . . . . . 10 |- 2 e. ZZ
6		1re 5358	. . . . . . . . . . 11 |- 1 e. RR
7		2re 5877	. . . . . . . . . . 11 |- 2 e. RR
8		1lt2 5926	. . . . . . . . . . 11 |- 1 < 2
9	6, 7, 8	ltlei 5505	. . . . . . . . . 10 |- 1 <_ 2
10	4, 5, 9	mpbir2an 727	. . . . . . . . 9 |- 2 e. (ZZ>` 1)
11		uzss 6314	. . . . . . . . 9 |- (2 e. (ZZ>` 1) -> (ZZ>` 2) (_ (ZZ>` 1))
12	10, 11	ax-mp 7	. . . . . . . 8 |- (ZZ>` 2) (_ (ZZ>` 1)
13		nnuz 6322	. . . . . . . 8 |- NN = (ZZ>` 1)
14	12, 13	sseqtr4 2065	. . . . . . 7 |- (ZZ>` 2) (_ NN
15	2, 14	sstri 2044	. . . . . 6 |- (ZZ i^i (ZZ>` 2)) (_ NN
16	15	sseli 2036	. . . . 5 |- (k e. (ZZ i^i (ZZ>` 2)) -> k e. NN)
17		ser1f0.1	. . . . . 6 |- F:NN-->CC
18	17	ffvelrni 3754	. . . . 5 |- (k e. NN -> (F` k) e. CC)
19	16, 18	syl 10	. . . 4 |- (k e. (ZZ i^i (ZZ>` 2)) -> (F` k) e. CC)
20	19	rgen 1674	. . 3 |- A.k e. (ZZ i^i (ZZ>` 2))(F` k) e. CC
21		uzssz 6313	. . . 4 |- (ZZ>` 2) (_ ZZ
22		ssid 2051	. . . 4 |- ZZ (_ ZZ
23		ssid 2051	. . . 4 |- (ZZ>` 2) (_ (ZZ>` 2)
24		nnex 5832	. . . . 5 |- NN e. V
25		fex 3591	. . . . 5 |- ((F:NN-->CC /\ NN e. V) -> F e. V)
26	17, 24, 25	mp2an 694	. . . 4 |- F e. V
27	5, 21, 22, 5, 23, 21, 26	clm4 6969	. . 3 |- ((0 e. CC /\ A.k e. (ZZ i^i (ZZ>` 2))(F` k) e. CC) -> (F ~~> 0 <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. (ZZ>` 2)(j <_ k -> (abs` ((F` k) - 0)) < x))))
28	1, 20, 27	mp2an 694	. 2 |- (F ~~> 0 <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. (ZZ>` 2)(j <_ k -> (abs` ((F` k) - 0)) < x)))
29		ser1f0.2	. . . . . 6 |- A e. CC
30		ser1f0.3	. . . . . 6 |- ( + seq1 F) ~~> A
31		0z 6044	. . . . . . 7 |- 0 e. ZZ
32		uzssz 6313	. . . . . . 7 |- (ZZ>` 0) (_ ZZ
33	31, 32, 22	clmi2 6976	. . . . . 6 |- (((A e. CC /\ ( + seq1 F) ~~> A) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))
34	29, 30, 33	mpanl12 705	. . . . 5 |- (((x / 2) e. RR /\ 0 < (x / 2)) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))
35		rehalfclt 5932	. . . . . 6 |- (x e. RR -> (x / 2) e. RR)
36	35	adantr 389	. . . . 5 |- ((x e. RR /\ 0 < x) -> (x / 2) e. RR)
37		halfpos2t 5935	. . . . . 6 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
38	37	biimpa 416	. . . . 5 |- ((x e. RR /\ 0 < x) -> 0 < (x / 2))
39	34, 36, 38	sylanc 471	. . . 4 |- ((x e. RR /\ 0 < x) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))
40		breq1 2590	. . . . . . . . . . 11 |- (j = (m + 1) -> (j <_ k <-> (m + 1) <_ k))
41	40	imbi1d 611	. . . . . . . . . 10 |- (j = (m + 1) -> ((j <_ k -> (abs` ((F` k) - 0)) < x) <-> ((m + 1) <_ k -> (abs` ((F` k) - 0)) < x)))
42	41	ralbidv 1639	. . . . . . . . 9 |- (j = (m + 1) -> (A.k e. (ZZ>` 2)(j <_ k -> (abs` ((F` k) - 0)) < x) <-> A.k e. (ZZ>` 2)((m + 1) <_ k -> (abs` ((F` k) - 0)) < x)))
43	42	rcla4ev 1850	. . . . . . . 8 |- (((m + 1) e. ZZ /\ A.k e. (ZZ>` 2)((m + 1) <_ k -> (abs` ((F` k) - 0)) < x)) -> E.j e. ZZ A.k e. (ZZ>` 2)(j <_ k -> (abs` ((F` k) - 0)) < x))
44		peano2z 6064	. . . . . . . . 9 |- (m e. ZZ -> (m + 1) e. ZZ)
45	44	ad2antrl 406	. . . . . . . 8 |- ((x e. RR /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> (m + 1) e. ZZ)
46		p1let 5724	. . . . . . . . . . . . . . . . . . 19 |- ((m e. RR /\ k e. RR /\ (m + 1) <_ k) -> m <_ k)
47	46	3expia 832	. . . . . . . . . . . . . . . . . 18 |- ((m e. RR /\ k e. RR) -> ((m + 1) <_ k -> m <_ k))
48		zret 6037	. . . . . . . . . . . . . . . . . 18 |- (m e. ZZ -> m e. RR)
49		zret 6037	. . . . . . . . . . . . . . . . . 18 |- (k e. ZZ -> k e. RR)
50	47, 48, 49	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((m e. ZZ /\ k e. ZZ) -> ((m + 1) <_ k -> m <_ k))
51	50	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((k e. ZZ /\ m e. ZZ) -> ((m + 1) <_ k -> m <_ k))
52	51	adantrr 395	. . . . . . . . . . . . . . 15 |- ((k e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> ((m + 1) <_ k -> m <_ k))
53		breq2 2591	. . . . . . . . . . . . . . . . . 18 |- (n = k -> (m <_ n <-> m <_ k))
54		fveq2 3663	. . . . . . . . . . . . . . . . . . . . 21 |- (n = k -> (( + seq1 F)` n) = (( + seq1 F)` k))
55	54	opreq1d 3914	. . . . . . . . . . . . . . . . . . . 20 |- (n = k -> ((( + seq1 F)` n) - A) = ((( + seq1 F)` k) - A))
56	55	fveq2d 3667	. . . . . . . . . . . . . . . . . . 19 |- (n = k -> (abs` ((( + seq1 F)` n) - A)) = (abs` ((( + seq1 F)` k) - A)))
57	56	breq1d 2597	. . . . . . . . . . . . . . . . . 18 |- (n = k -> ((abs` ((( + seq1 F)` n) - A)) < (x / 2) <-> (abs` ((( + seq1 F)` k) - A)) < (x / 2)))
58	53, 57	imbi12d 624	. . . . . . . . . . . . . . . . 17 |- (n = k -> ((m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)) <-> (m <_ k -> (abs` ((( + seq1 F)` k) - A)) < (x / 2))))
59	58	rcla4va 1848	. . . . . . . . . . . . . . . 16 |- ((k e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2))) -> (m <_ k -> (abs` ((( + seq1 F)` k) - A)) < (x / 2)))
60	59	adantrl 394	. . . . . . . . . . . . . . 15 |- ((k e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> (m <_ k -> (abs` ((( + seq1 F)` k) - A)) < (x / 2)))
61	52, 60	syld 27	. . . . . . . . . . . . . 14 |- ((k e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> ((m + 1) <_ k -> (abs` ((( + seq1 F)` k) - A)) < (x / 2)))
62		leaddsubt 5558	. . . . . . . . . . . . . . . . . . 19 |- ((m e. RR /\ 1 e. RR /\ k e. RR) -> ((m + 1) <_ k <-> m <_ (k - 1)))
63	6, 62	mp3an2 900	. . . . . . . . . . . . . . . . . 18 |- ((m e. RR /\ k e. RR) -> ((m + 1) <_ k <-> m <_ (k - 1)))
64	63, 48, 49	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((m e. ZZ /\ k e. ZZ) -> ((m + 1) <_ k <-> m <_ (k - 1)))
65	64	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((k e. ZZ /\ m e. ZZ) -> ((m + 1) <_ k <-> m <_ (k - 1)))
66	65	adantrr 395	. . . . . . . . . . . . . . 15 |- ((k e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> ((m + 1) <_ k <-> m <_ (k - 1)))
67		peano2zm 6067	. . . . . . . . . . . . . . . . . 18 |- (k e. ZZ -> (k - 1) e. ZZ)
68		breq2 2591	. . . . . . . . . . . . . . . . . . . 20 |- (n = (k - 1) -> (m <_ n <-> m <_ (k - 1)))
69		fveq2 3663	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n = (k - 1) -> (( + seq1 F)` n) = (( + seq1 F)` (k - 1)))
70	69	opreq1d 3914	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = (k - 1) -> ((( + seq1 F)` n) - A) = ((( + seq1 F)` (k - 1)<