Metamath Proof Explorer

Theorem serle

Description: Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses serge0.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
serge0.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
serle.3 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. RR )
serle.4 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) <_ ( G ` k ) )
Assertion serle 
|- ( ph -> ( seq M ( + , F ) ` N ) <_ ( seq M ( + , G ) ` N ) )

Proof

Step Hyp Ref Expression
1 serge0.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 serge0.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
3 serle.3 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. RR )
4 serle.4 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) <_ ( G ` k ) )
5 fveq2 
 |-  ( x = k -> ( G ` x ) = ( G ` k ) )
6 fveq2 
 |-  ( x = k -> ( F ` x ) = ( F ` k ) )
7 5 6 oveq12d 
 |-  ( x = k -> ( ( G ` x ) - ( F ` x ) ) = ( ( G ` k ) - ( F ` k ) ) )
8 eqid 
 |-  ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) ) = ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) )
9 ovex 
 |-  ( ( G ` k ) - ( F ` k ) ) e. _V
10 7 8 9 fvmpt 
 |-  ( k e. _V -> ( ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) ) ` k ) = ( ( G ` k ) - ( F ` k ) ) )
11 10 elv 
 |-  ( ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) ) ` k ) = ( ( G ` k ) - ( F ` k ) )
12 3 2 resubcld 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( ( G ` k ) - ( F ` k ) ) e. RR )
13 11 12 eqeltrid 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) ) ` k ) e. RR )
14 3 2 subge0d 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( 0 <_ ( ( G ` k ) - ( F ` k ) ) <-> ( F ` k ) <_ ( G ` k ) ) )
15 4 14 mpbird 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> 0 <_ ( ( G ` k ) - ( F ` k ) ) )
16 15 11 breqtrrdi 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> 0 <_ ( ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) ) ` k ) )
17 1 13 16 serge0 
 |-  ( ph -> 0 <_ ( seq M ( + , ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) ) ) ` N ) )
18 3 recnd 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )
19 2 recnd 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
20 11 a1i 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) ) ` k ) = ( ( G ` k ) - ( F ` k ) ) )
21 1 18 19 20 sersub 
 |-  ( ph -> ( seq M ( + , ( x e. _V |-> ( ( G ` x ) - ( F ` x ) ) ) ) ` N ) = ( ( seq M ( + , G ) ` N ) - ( seq M ( + , F ) ` N ) ) )
22 17 21 breqtrd 
 |-  ( ph -> 0 <_ ( ( seq M ( + , G ) ` N ) - ( seq M ( + , F ) ` N ) ) )
23 readdcl 
 |-  ( ( k e. RR /\ x e. RR ) -> ( k + x ) e. RR )
24 23 adantl 
 |-  ( ( ph /\ ( k e. RR /\ x e. RR ) ) -> ( k + x ) e. RR )
25 1 3 24 seqcl 
 |-  ( ph -> ( seq M ( + , G ) ` N ) e. RR )
26 1 2 24 seqcl 
 |-  ( ph -> ( seq M ( + , F ) ` N ) e. RR )
27 25 26 subge0d 
 |-  ( ph -> ( 0 <_ ( ( seq M ( + , G ) ` N ) - ( seq M ( + , F ) ` N ) ) <-> ( seq M ( + , F ) ` N ) <_ ( seq M ( + , G ) ` N ) ) )
28 22 27 mpbid 
 |-  ( ph -> ( seq M ( + , F ) ` N ) <_ ( seq M ( + , G ) ` N ) )