Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

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
serzf0.2
serzf0.3
serzf0.4
serzf0.5

Assertion

Ref	Expression
serzf0

Distinct variable groups:   ,   ,

---

Proof of Theorem serzf0

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