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	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	seqabs.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	seqabs.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
Assertion	seqabs	⊢ ( 𝜑 → ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		seqabs.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		seqabs.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
3		seqabs.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
4		fzfid	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
5	4 2	fsumabs	⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
6		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
7	6 1 2	fsumser	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
8	7	fveq2d	⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) = ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
9		abscl	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
10	9	recnd	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
11	2 10	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
12	3 1 11	fsumser	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )
13	5 8 12	3brtr3d	⊢ ( 𝜑 → ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )