Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem climserzle 7083

Description: The partial sums of a converging infinite series with nonnegative terms are bounded by its limit.

Hypotheses

Ref	Expression
climserzle.1
climserzle.2
climserzle.3
climserzle.4

Assertion

Ref	Expression
climserzle

Distinct variable groups:   ,   ,   ,

---

Proof of Theorem climserzle

Step	Hyp	Ref	Expression
1		oprex 3968	. . . 4
2	1	climge0 7049	. . 3
3		eluzelz 6355	. . . . 5
4	3	peano2zd 6114	. . . 4
5	4	adantr 389	. . 3
6		climserzle.1	. . . . 5
7		climserzle.2	. . . . 5
8		climserzle.3	. . . . 5
9		climserzle.4	. . . . . 6
10		axresscn 5240	. . . . . 6
11		fss 3620	. . . . . 6
12	9, 10, 11	mp2an 695	. . . . 5
13	6, 7, 8, 12	clim2serz 7081	. . . 4
14	13	adantr 389	. . 3
15	6	serzreclt 6988	. . . . . . 7
16		pm3.27 323	. . . . . . 7
17		uztrn 6360	. . . . . . . . . . . 12
18	17	ancoms 436	. . . . . . . . . . 11
19		peano2uz 6379	. . . . . . . . . . 11
20		elfzuzt 6420	. . . . . . . . . . 11
21	18, 19, 20	syl2an 454	. . . . . . . . . 10
22	9	ffvelrni 3800	. . . . . . . . . 10
23	21, 22	syl 10	. . . . . . . . 9
24	23	r19.21aiva 1706	. . . . . . . 8
25	24	adantr 389	. . . . . . 7
26	15, 16, 25	sylanc 471	. . . . . 6
27	26	adantlr 393	. . . . 5
28	6	serzcmp0 6993	. . . . . . 7
29		pm3.2 283	. . . . . . . . . . . . . 14
30	22, 29	syl 10	. . . . . . . . . . . . 13
31	30	a2i 9	. . . . . . . . . . . 12
32	17, 20, 19	syl2an 454	. . . . . . . . . . . 12
33	31, 32	syl5 21	. . . . . . . . . . 11
34	33	exp3a 375	. . . . . . . . . 10
35	34	com3r 35	. . . . . . . . 9
36	35	r19.20dv2 1703	. . . . . . . 8
37	36	imp 350	. . . . . . 7
38	28, 37	sylan2 451	. . . . . 6
39	38	ancoms 436	. . . . 5
40	27, 39	jca 288	. . . 4
41	40	r19.21aiva 1706	. . 3
42	2, 5, 14, 41	syl3anc 856	. 2
43		subge0t 5647	. . . 4
44		eluzel2 6356	. . . . 5
45		elfzuzt 6420	. . . . . . . . . 10
46	45, 22	syl 10	. . . . . . . . 9
47	46	rgen 1690	. . . . . . . 8
48	6	serzreclt 6988	. . . . . . . 8
49	47, 48	mpan2 694	. . . . . . 7
50	49	rgen 1690	. . . . . 6
51	7	climrecl 7047	. . . . . 6