Theorem cvgcmpub

Description: An upper bound for the limit of a real infinite series. This theorem can also be used to compare two infinite series. (Contributed by Mario Carneiro, 24-Mar-2014)

	Ref	Expression
Hypotheses	cvgcmp.1	|- Z = ( ZZ>= ` M )
	cvgcmp.2	|- ( ph -> N e. Z )
	cvgcmp.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
	cvgcmp.4	|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
	cvgcmpub.5	|- ( ph -> seq M ( + , F ) ~~> A )
	cvgcmpub.6	|- ( ph -> seq M ( + , G ) ~~> B )
	cvgcmpub.7	|- ( ( ph /\ k e. Z ) -> ( G ` k ) <_ ( F ` k ) )
Assertion	cvgcmpub	|- ( ph -> B <_ A )

Proof

Step	Hyp	Ref	Expression
1		cvgcmp.1	|- Z = ( ZZ>= ` M )
2		cvgcmp.2	|- ( ph -> N e. Z )
3		cvgcmp.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
4		cvgcmp.4	|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
5		cvgcmpub.5	|- ( ph -> seq M ( + , F ) ~~> A )
6		cvgcmpub.6	|- ( ph -> seq M ( + , G ) ~~> B )
7		cvgcmpub.7	|- ( ( ph /\ k e. Z ) -> ( G ` k ) <_ ( F ` k ) )
8	2 1	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` M ) )
9		eluzel2	|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
10	8 9	syl	|- ( ph -> M e. ZZ )
11	1 10 4	serfre	|- ( ph -> seq M ( + , G ) : Z --> RR )
12	11	ffvelrnda	|- ( ( ph /\ n e. Z ) -> ( seq M ( + , G ) ` n ) e. RR )
13	1 10 3	serfre	|- ( ph -> seq M ( + , F ) : Z --> RR )
14	13	ffvelrnda	|- ( ( ph /\ n e. Z ) -> ( seq M ( + , F ) ` n ) e. RR )
15		simpr	|- ( ( ph /\ n e. Z ) -> n e. Z )
16	15 1	eleqtrdi	|- ( ( ph /\ n e. Z ) -> n e. ( ZZ>= ` M ) )
17		simpl	|- ( ( ph /\ n e. Z ) -> ph )
18		elfzuz	|- ( k e. ( M ... n ) -> k e. ( ZZ>= ` M ) )
19	18 1	eleqtrrdi	|- ( k e. ( M ... n ) -> k e. Z )
20	17 19 4	syl2an	|- ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> ( G ` k ) e. RR )
21	17 19 3	syl2an	|- ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> ( F ` k ) e. RR )
22	17 19 7	syl2an	|- ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> ( G ` k ) <_ ( F ` k ) )
23	16 20 21 22	serle	|- ( ( ph /\ n e. Z ) -> ( seq M ( + , G ) ` n ) <_ ( seq M ( + , F ) ` n ) )
24	1 10 6 5 12 14 23	climle	|- ( ph -> B <_ A )