climserle

Description: The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by NM, 27-Dec-2005) (Revised by Mario Carneiro, 9-Feb-2014)

	Ref	Expression
Hypotheses	clim2ser.1	\|- Z = ( ZZ>= ` M )
	climserle.2	\|- ( ph -> N e. Z )
	climserle.3	\|- ( ph -> seq M ( + , F ) ~~> A )
	climserle.4	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
	climserle.5	\|- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
Assertion	climserle	\|- ( ph -> ( seq M ( + , F ) ` N ) <_ A )

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	\|- Z = ( ZZ>= ` M )
2		climserle.2	\|- ( ph -> N e. Z )
3		climserle.3	\|- ( ph -> seq M ( + , F ) ~~> A )
4		climserle.4	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
5		climserle.5	\|- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
6	2 1	eleqtrdi	\|- ( ph -> N e. ( ZZ>= ` M ) )
7		eluzel2	\|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
8	6 7	syl	\|- ( ph -> M e. ZZ )
9	1 8 4	serfre	\|- ( ph -> seq M ( + , F ) : Z --> RR )
10	9	ffvelrnda	\|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. RR )
11	1	peano2uzs	\|- ( j e. Z -> ( j + 1 ) e. Z )
12		fveq2	\|- ( k = ( j + 1 ) -> ( F ` k ) = ( F ` ( j + 1 ) ) )
13	12	breq2d	\|- ( k = ( j + 1 ) -> ( 0 <_ ( F ` k ) <-> 0 <_ ( F ` ( j + 1 ) ) ) )
14	13	imbi2d	\|- ( k = ( j + 1 ) -> ( ( ph -> 0 <_ ( F ` k ) ) <-> ( ph -> 0 <_ ( F ` ( j + 1 ) ) ) ) )
15	5	expcom	\|- ( k e. Z -> ( ph -> 0 <_ ( F ` k ) ) )
16	14 15	vtoclga	\|- ( ( j + 1 ) e. Z -> ( ph -> 0 <_ ( F ` ( j + 1 ) ) ) )
17	16	impcom	\|- ( ( ph /\ ( j + 1 ) e. Z ) -> 0 <_ ( F ` ( j + 1 ) ) )
18	11 17	sylan2	\|- ( ( ph /\ j e. Z ) -> 0 <_ ( F ` ( j + 1 ) ) )
19	12	eleq1d	\|- ( k = ( j + 1 ) -> ( ( F ` k ) e. RR <-> ( F ` ( j + 1 ) ) e. RR ) )
20	19	imbi2d	\|- ( k = ( j + 1 ) -> ( ( ph -> ( F ` k ) e. RR ) <-> ( ph -> ( F ` ( j + 1 ) ) e. RR ) ) )
21	4	expcom	\|- ( k e. Z -> ( ph -> ( F ` k ) e. RR ) )
22	20 21	vtoclga	\|- ( ( j + 1 ) e. Z -> ( ph -> ( F ` ( j + 1 ) ) e. RR ) )
23	22	impcom	\|- ( ( ph /\ ( j + 1 ) e. Z ) -> ( F ` ( j + 1 ) ) e. RR )
24	11 23	sylan2	\|- ( ( ph /\ j e. Z ) -> ( F ` ( j + 1 ) ) e. RR )
25	10 24	addge01d	\|- ( ( ph /\ j e. Z ) -> ( 0 <_ ( F ` ( j + 1 ) ) <-> ( seq M ( + , F ) ` j ) <_ ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) ) )
26	18 25	mpbid	\|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) <_ ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) )
27		simpr	\|- ( ( ph /\ j e. Z ) -> j e. Z )
28	27 1	eleqtrdi	\|- ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
29		seqp1	\|- ( j e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( j + 1 ) ) = ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) )
30	28 29	syl	\|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` ( j + 1 ) ) = ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) )
31	26 30	breqtrrd	\|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) <_ ( seq M ( + , F ) ` ( j + 1 ) ) )
32	1 2 3 10 31	climub	\|- ( ph -> ( seq M ( + , F ) ` N ) <_ A )

Metamath Proof Explorer

Theorem climserle

Proof