Theorem iserabs

Description: Generalized triangle inequality: the absolute value of an infinite sum is less than or equal to the sum of absolute values. (Contributed by Paul Chapman, 10-Sep-2007) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	iserabs.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	iserabs.2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
	iserabs.3	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ 𝐵 )
	iserabs.5	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	iserabs.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	iserabs.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
Assertion	iserabs	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		iserabs.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iserabs.2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
3		iserabs.3	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ 𝐵 )
4		iserabs.5	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		iserabs.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
6		iserabs.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
7	1	fvexi	⊢ 𝑍 ∈ V
8	7	mptex	⊢ ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) ∈ V
9	8	a1i	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) ∈ V )
10	1 4 5	serf	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
11	10	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
12		2fveq3	⊢ ( 𝑚 = 𝑛 → ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) = ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
13		eqid	⊢ ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) )
14		fvex	⊢ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ∈ V
15	12 13 14	fvmpt	⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) = ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) = ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
17	1 2 9 4 11 16	climabs	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) ⇝ ( abs ‘ 𝐴 ) )
18	11	abscld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ∈ ℝ )
19	16 18	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) ∈ ℝ )
20	5	abscld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
21	6 20	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
22	1 4 21	serfre	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) : 𝑍 ⟶ ℝ )
23	22	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
25	24 1	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
26		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
27	26 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ 𝑍 )
28	27 5	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
29	28	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
30	27 6	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
31	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
32	25 29 31	seqabs	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) )
33	16 32	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) )
34	1 4 17 3 19 23 33	climle	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 𝐵 )