Metamath Proof Explorer

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	$⊢ φ \to N \in ℤ_{\geq M}$
		seqabs.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℂ$
		seqabs.3	$⊢ (φ \land k \in (M \dots N)) \to G (k) = \|F (k)\|$
	Assertion	seqabs	$⊢ φ \to \|seq M (+ F) (N)\| \leq seq M (+ G) (N)$

Proof

Step	Hyp	Ref	Expression
1		seqabs.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		seqabs.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℂ$
3		seqabs.3	$⊢ (φ \land k \in (M \dots N)) \to G (k) = \|F (k)\|$
4		fzfid	$⊢ φ \to (M \dots N) \in Fin$
5	4 2	fsumabs	$⊢ φ \to \|\sum_{k = M}^{N} F (k)\| \leq \sum_{k = M}^{N} \|F (k)\|$
6		eqidd	$⊢ (φ \land k \in (M \dots N)) \to F (k) = F (k)$
7	6 1 2	fsumser	$⊢ φ \to \sum_{k = M}^{N} F (k) = seq M (+ F) (N)$
8	7	fveq2d	$⊢ φ \to \|\sum_{k = M}^{N} F (k)\| = \|seq M (+ F) (N)\|$
9		abscl	$⊢ F (k) \in ℂ \to \|F (k)\| \in ℝ$
10	9	recnd	$⊢ F (k) \in ℂ \to \|F (k)\| \in ℂ$
11	2 10	syl	$⊢ (φ \land k \in (M \dots N)) \to \|F (k)\| \in ℂ$
12	3 1 11	fsumser	$⊢ φ \to \sum_{k = M}^{N} \|F (k)\| = seq M (+ G) (N)$
13	5 8 12	3brtr3d	$⊢ φ \to \|seq M (+ F) (N)\| \leq seq M (+ G) (N)$