Theorem isumle

Description: Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007) (Revised by Mario Carneiro, 24-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		isumle.1	|- Z = ( ZZ>= ` M )
2		isumle.2	|- ( ph -> M e. ZZ )
3		isumle.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4		isumle.4	|- ( ( ph /\ k e. Z ) -> A e. RR )
5		isumle.5	|- ( ( ph /\ k e. Z ) -> ( G ` k ) = B )
6		isumle.6	|- ( ( ph /\ k e. Z ) -> B e. RR )
7		isumle.7	|- ( ( ph /\ k e. Z ) -> A <_ B )
8		isumle.8	|- ( ph -> seq M ( + , F ) e. dom ~~> )
9		isumle.9	|- ( ph -> seq M ( + , G ) e. dom ~~> )
10		climdm	|- ( seq M ( + , F ) e. dom ~~> <-> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
11	8 10	sylib	|- ( ph -> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
12		climdm	|- ( seq M ( + , G ) e. dom ~~> <-> seq M ( + , G ) ~~> ( ~~> ` seq M ( + , G ) ) )
13	9 12	sylib	|- ( ph -> seq M ( + , G ) ~~> ( ~~> ` seq M ( + , G ) ) )
14	3 4	eqeltrd	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
15	5 6	eqeltrd	|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
16	7 3 5	3brtr4d	|- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )
17	1 2 11 13 14 15 16	iserle	|- ( ph -> ( ~~> ` seq M ( + , F ) ) <_ ( ~~> ` seq M ( + , G ) ) )
18	4	recnd	|- ( ( ph /\ k e. Z ) -> A e. CC )
19	1 2 3 18	isum	|- ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , F ) ) )
20	6	recnd	|- ( ( ph /\ k e. Z ) -> B e. CC )
21	1 2 5 20	isum	|- ( ph -> sum_ k e. Z B = ( ~~> ` seq M ( + , G ) ) )
22	17 19 21	3brtr4d	|- ( ph -> sum_ k e. Z A <_ sum_ k e. Z B )