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 = ( ZZ>= ` M )
iserabs.2 
|- ( ph -> seq M ( + , F ) ~~> A )
iserabs.3 
|- ( ph -> seq M ( + , G ) ~~> B )
iserabs.5 
|- ( ph -> M e. ZZ )
iserabs.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
iserabs.7 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
Assertion iserabs 
|- ( ph -> ( abs ` A ) <_ B )

Proof

Step Hyp Ref Expression
1 iserabs.1 
 |-  Z = ( ZZ>= ` M )
2 iserabs.2 
 |-  ( ph -> seq M ( + , F ) ~~> A )
3 iserabs.3 
 |-  ( ph -> seq M ( + , G ) ~~> B )
4 iserabs.5 
 |-  ( ph -> M e. ZZ )
5 iserabs.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6 iserabs.7 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
7 1 fvexi 
 |-  Z e. _V
8 7 mptex 
 |-  ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) ) e. _V
9 8 a1i 
 |-  ( ph -> ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) ) e. _V )
10 1 4 5 serf 
 |-  ( ph -> seq M ( + , F ) : Z --> CC )
11 10 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( seq M ( + , F ) ` n ) e. CC )
12 2fveq3 
 |-  ( m = n -> ( abs ` ( seq M ( + , F ) ` m ) ) = ( abs ` ( seq M ( + , F ) ` n ) ) )
13 eqid 
 |-  ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) ) = ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) )
14 fvex 
 |-  ( abs ` ( seq M ( + , F ) ` n ) ) e. _V
15 12 13 14 fvmpt 
 |-  ( n e. Z -> ( ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) ) ` n ) = ( abs ` ( seq M ( + , F ) ` n ) ) )
16 15 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) ) ` n ) = ( abs ` ( seq M ( + , F ) ` n ) ) )
17 1 2 9 4 11 16 climabs 
 |-  ( ph -> ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) ) ~~> ( abs ` A ) )
18 11 abscld 
 |-  ( ( ph /\ n e. Z ) -> ( abs ` ( seq M ( + , F ) ` n ) ) e. RR )
19 16 18 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> ( ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) ) ` n ) e. RR )
20 5 abscld 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( F ` k ) ) e. RR )
21 6 20 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
22 1 4 21 serfre 
 |-  ( ph -> seq M ( + , G ) : Z --> RR )
23 22 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( seq M ( + , G ) ` n ) e. RR )
24 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
25 24 1 eleqtrdi 
 |-  ( ( ph /\ n e. Z ) -> n e. ( ZZ>= ` M ) )
26 elfzuz 
 |-  ( k e. ( M ... n ) -> k e. ( ZZ>= ` M ) )
27 26 1 eleqtrrdi 
 |-  ( k e. ( M ... n ) -> k e. Z )
28 27 5 sylan2 
 |-  ( ( ph /\ k e. ( M ... n ) ) -> ( F ` k ) e. CC )
29 28 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> ( F ` k ) e. CC )
30 27 6 sylan2 
 |-  ( ( ph /\ k e. ( M ... n ) ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
31 30 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
32 25 29 31 seqabs 
 |-  ( ( ph /\ n e. Z ) -> ( abs ` ( seq M ( + , F ) ` n ) ) <_ ( seq M ( + , G ) ` n ) )
33 16 32 eqbrtrd 
 |-  ( ( ph /\ n e. Z ) -> ( ( m e. Z |-> ( abs ` ( seq M ( + , F ) ` m ) ) ) ` n ) <_ ( seq M ( + , G ) ` n ) )
34 1 4 17 3 19 23 33 climle 
 |-  ( ph -> ( abs ` A ) <_ B )