Theorem seqabs

Description: Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by Mario Carneiro, 26-Mar-2014) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	seqabs.1	|- ( ph -> N e. ( ZZ>= ` M ) )
	seqabs.2	|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
	seqabs.3	|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
Assertion	seqabs	|- ( ph -> ( abs ` ( seq M ( + , F ) ` N ) ) <_ ( seq M ( + , G ) ` N ) )

Proof

Step	Hyp	Ref	Expression
1		seqabs.1	|- ( ph -> N e. ( ZZ>= ` M ) )
2		seqabs.2	|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
3		seqabs.3	|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
4		fzfid	|- ( ph -> ( M ... N ) e. Fin )
5	4 2	fsumabs	|- ( ph -> ( abs ` sum_ k e. ( M ... N ) ( F ` k ) ) <_ sum_ k e. ( M ... N ) ( abs ` ( F ` k ) ) )
6		eqidd	|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( F ` k ) )
7	6 1 2	fsumser	|- ( ph -> sum_ k e. ( M ... N ) ( F ` k ) = ( seq M ( + , F ) ` N ) )
8	7	fveq2d	|- ( ph -> ( abs ` sum_ k e. ( M ... N ) ( F ` k ) ) = ( abs ` ( seq M ( + , F ) ` N ) ) )
9		abscl	|- ( ( F ` k ) e. CC -> ( abs ` ( F ` k ) ) e. RR )
10	9	recnd	|- ( ( F ` k ) e. CC -> ( abs ` ( F ` k ) ) e. CC )
11	2 10	syl	|- ( ( ph /\ k e. ( M ... N ) ) -> ( abs ` ( F ` k ) ) e. CC )
12	3 1 11	fsumser	|- ( ph -> sum_ k e. ( M ... N ) ( abs ` ( F ` k ) ) = ( seq M ( + , G ) ` N ) )
13	5 8 12	3brtr3d	|- ( ph -> ( abs ` ( seq M ( + , F ) ` N ) ) <_ ( seq M ( + , G ) ` N ) )