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 ⊢ Z = ℤ ≥ M
iserabs.2 ⊢ φ → seq M + F ⇝ A
iserabs.3 ⊢ φ → seq M + G ⇝ B
iserabs.5 ⊢ φ → M ∈ ℤ
iserabs.6 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
iserabs.7 ⊢ φ ∧ k ∈ Z → G ⁡ k = F ⁡ k
Assertion iserabs ⊢ φ → A ≤ B

Proof

Step Hyp Ref Expression
1 iserabs.1 ⊢ Z = ℤ ≥ M
2 iserabs.2 ⊢ φ → seq M + F ⇝ A
3 iserabs.3 ⊢ φ → seq M + G ⇝ B
4 iserabs.5 ⊢ φ → M ∈ ℤ
5 iserabs.6 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
6 iserabs.7 ⊢ φ ∧ k ∈ Z → G ⁡ k = F ⁡ k
7 1 fvexi ⊢ Z ∈ V
8 7 mptex ⊢ m ∈ Z ⟼ seq M + F ⁡ m ∈ V
9 8 a1i ⊢ φ → m ∈ Z ⟼ seq M + F ⁡ m ∈ V
10 1 4 5 serf ⊢ φ → seq M + F : Z ⟶ ℂ
11 10 ffvelcdmda ⊢ φ ∧ n ∈ Z → seq M + F ⁡ n ∈ ℂ
12 2fveq3 ⊢ m = n → seq M + F ⁡ m = seq M + F ⁡ n
13 eqid ⊢ m ∈ Z ⟼ seq M + F ⁡ m = m ∈ Z ⟼ seq M + F ⁡ m
14 fvex ⊢ seq M + F ⁡ n ∈ V
15 12 13 14 fvmpt ⊢ n ∈ Z → m ∈ Z ⟼ seq M + F ⁡ m ⁡ n = seq M + F ⁡ n
16 15 adantl ⊢ φ ∧ n ∈ Z → m ∈ Z ⟼ seq M + F ⁡ m ⁡ n = seq M + F ⁡ n
17 1 2 9 4 11 16 climabs ⊢ φ → m ∈ Z ⟼ seq M + F ⁡ m ⇝ A
18 11 abscld ⊢ φ ∧ n ∈ Z → seq M + F ⁡ n ∈ ℝ
19 16 18 eqeltrd ⊢ φ ∧ n ∈ Z → m ∈ Z ⟼ seq M + F ⁡ m ⁡ n ∈ ℝ
20 5 abscld ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
21 6 20 eqeltrd ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℝ
22 1 4 21 serfre ⊢ φ → seq M + G : Z ⟶ ℝ
23 22 ffvelcdmda ⊢ φ ∧ n ∈ Z → seq M + G ⁡ n ∈ ℝ
24 simpr ⊢ φ ∧ n ∈ Z → n ∈ Z
25 24 1 eleqtrdi ⊢ φ ∧ n ∈ Z → n ∈ ℤ ≥ M
26 elfzuz ⊢ k ∈ M … n → k ∈ ℤ ≥ M
27 26 1 eleqtrrdi ⊢ k ∈ M … n → k ∈ Z
28 27 5 sylan2 ⊢ φ ∧ k ∈ M … n → F ⁡ k ∈ ℂ
29 28 adantlr ⊢ φ ∧ n ∈ Z ∧ k ∈ M … n → F ⁡ k ∈ ℂ
30 27 6 sylan2 ⊢ φ ∧ k ∈ M … n → G ⁡ k = F ⁡ k
31 30 adantlr ⊢ φ ∧ n ∈ Z ∧ k ∈ M … n → G ⁡ k = F ⁡ k
32 25 29 31 seqabs ⊢ φ ∧ n ∈ Z → seq M + F ⁡ n ≤ seq M + G ⁡ n
33 16 32 eqbrtrd ⊢ φ ∧ n ∈ Z → m ∈ Z ⟼ seq M + F ⁡ m ⁡ n ≤ seq M + G ⁡ n
34 1 4 17 3 19 23 33 climle ⊢ φ → A ≤ B