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 ⊢φ→seqM+F⇝A
iserabs.3 ⊢φ→seqM+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 ⊢φ→seqM+F⇝A
3 iserabs.3 ⊢φ→seqM+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⟼seqM+F⁡m∈V
9 8 a1i ⊢φ→m∈Z⟼seqM+F⁡m∈V
10 1 4 5 serf ⊢φ→seqM+F:Z⟶ℂ
11 10 ffvelcdmda ⊢φ∧n∈Z→seqM+F⁡n∈ℂ
12 2fveq3 ⊢m=n→seqM+F⁡m=seqM+F⁡n
13 eqid ⊢m∈Z⟼seqM+F⁡m=m∈Z⟼seqM+F⁡m
14 fvex ⊢seqM+F⁡n∈V
15 12 13 14 fvmpt ⊢n∈Z→m∈Z⟼seqM+F⁡m⁡n=seqM+F⁡n
16 15 adantl ⊢φ∧n∈Z→m∈Z⟼seqM+F⁡m⁡n=seqM+F⁡n
17 1 2 9 4 11 16 climabs ⊢φ→m∈Z⟼seqM+F⁡m⇝A
18 11 abscld ⊢φ∧n∈Z→seqM+F⁡n∈ℝ
19 16 18 eqeltrd ⊢φ∧n∈Z→m∈Z⟼seqM+F⁡m⁡n∈ℝ
20 5 abscld ⊢φ∧k∈Z→F⁡k∈ℝ
21 6 20 eqeltrd ⊢φ∧k∈Z→G⁡k∈ℝ
22 1 4 21 serfre ⊢φ→seqM+G:Z⟶ℝ
23 22 ffvelcdmda ⊢φ∧n∈Z→seqM+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→seqM+F⁡n≤seqM+G⁡n
33 16 32 eqbrtrd ⊢φ∧n∈Z→m∈Z⟼seqM+F⁡m⁡n≤seqM+G⁡n
34 1 4 17 3 19 23 33 climle ⊢φ→A≤B