This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) ≤ 𝐵 )