Metamath Proof Explorer

Theorem sermono

Description: The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 30-Jun-2013)

Ref Expression
Hypotheses sermono.1 
|- ( ph -> K e. ( ZZ>= ` M ) )
sermono.2 
|- ( ph -> N e. ( ZZ>= ` K ) )
sermono.3 
|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. RR )
sermono.4 
|- ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> 0 <_ ( F ` x ) )
Assertion sermono 
|- ( ph -> ( seq M ( + , F ) ` K ) <_ ( seq M ( + , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 sermono.1 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
2 sermono.2 
 |-  ( ph -> N e. ( ZZ>= ` K ) )
3 sermono.3 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. RR )
4 sermono.4 
 |-  ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> 0 <_ ( F ` x ) )
5 elfzuz 
 |-  ( k e. ( K ... N ) -> k e. ( ZZ>= ` K ) )
6 uztrn 
 |-  ( ( k e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` M ) ) -> k e. ( ZZ>= ` M ) )
7 5 1 6 syl2anr 
 |-  ( ( ph /\ k e. ( K ... N ) ) -> k e. ( ZZ>= ` M ) )
8 elfzuz3 
 |-  ( k e. ( K ... N ) -> N e. ( ZZ>= ` k ) )
9 8 adantl 
 |-  ( ( ph /\ k e. ( K ... N ) ) -> N e. ( ZZ>= ` k ) )
10 fzss2 
 |-  ( N e. ( ZZ>= ` k ) -> ( M ... k ) C_ ( M ... N ) )
11 9 10 syl 
 |-  ( ( ph /\ k e. ( K ... N ) ) -> ( M ... k ) C_ ( M ... N ) )
12 11 sselda 
 |-  ( ( ( ph /\ k e. ( K ... N ) ) /\ x e. ( M ... k ) ) -> x e. ( M ... N ) )
13 3 adantlr 
 |-  ( ( ( ph /\ k e. ( K ... N ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. RR )
14 12 13 syldan 
 |-  ( ( ( ph /\ k e. ( K ... N ) ) /\ x e. ( M ... k ) ) -> ( F ` x ) e. RR )
15 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
16 15 adantl 
 |-  ( ( ( ph /\ k e. ( K ... N ) ) /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
17 7 14 16 seqcl 
 |-  ( ( ph /\ k e. ( K ... N ) ) -> ( seq M ( + , F ) ` k ) e. RR )
18 fveq2 
 |-  ( x = ( k + 1 ) -> ( F ` x ) = ( F ` ( k + 1 ) ) )
19 18 breq2d 
 |-  ( x = ( k + 1 ) -> ( 0 <_ ( F ` x ) <-> 0 <_ ( F ` ( k + 1 ) ) ) )
20 4 ralrimiva 
 |-  ( ph -> A. x e. ( ( K + 1 ) ... N ) 0 <_ ( F ` x ) )
21 20 adantr 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> A. x e. ( ( K + 1 ) ... N ) 0 <_ ( F ` x ) )
22 simpr 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> k e. ( K ... ( N - 1 ) ) )
23 1 adantr 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> K e. ( ZZ>= ` M ) )
24 eluzelz 
 |-  ( K e. ( ZZ>= ` M ) -> K e. ZZ )
25 23 24 syl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> K e. ZZ )
26 2 adantr 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` K ) )
27 eluzelz 
 |-  ( N e. ( ZZ>= ` K ) -> N e. ZZ )
28 26 27 syl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> N e. ZZ )
29 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
30 28 29 syl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( N - 1 ) e. ZZ )
31 elfzelz 
 |-  ( k e. ( K ... ( N - 1 ) ) -> k e. ZZ )
32 31 adantl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> k e. ZZ )
33 1zzd 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> 1 e. ZZ )
34 fzaddel 
 |-  ( ( ( K e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( k e. ZZ /\ 1 e. ZZ ) ) -> ( k e. ( K ... ( N - 1 ) ) <-> ( k + 1 ) e. ( ( K + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
35 25 30 32 33 34 syl22anc 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( k e. ( K ... ( N - 1 ) ) <-> ( k + 1 ) e. ( ( K + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
36 22 35 mpbid 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( k + 1 ) e. ( ( K + 1 ) ... ( ( N - 1 ) + 1 ) ) )
37 zcn 
 |-  ( N e. ZZ -> N e. CC )
38 ax-1cn 
 |-  1 e. CC
39 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
40 37 38 39 sylancl 
 |-  ( N e. ZZ -> ( ( N - 1 ) + 1 ) = N )
41 28 40 syl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
42 41 oveq2d 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( ( K + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( K + 1 ) ... N ) )
43 36 42 eleqtrd 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( k + 1 ) e. ( ( K + 1 ) ... N ) )
44 19 21 43 rspcdva 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> 0 <_ ( F ` ( k + 1 ) ) )
45 fzelp1 
 |-  ( k e. ( K ... ( N - 1 ) ) -> k e. ( K ... ( ( N - 1 ) + 1 ) ) )
46 45 adantl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> k e. ( K ... ( ( N - 1 ) + 1 ) ) )
47 41 oveq2d 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( K ... ( ( N - 1 ) + 1 ) ) = ( K ... N ) )
48 46 47 eleqtrd 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> k e. ( K ... N ) )
49 48 17 syldan 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( seq M ( + , F ) ` k ) e. RR )
50 18 eleq1d 
 |-  ( x = ( k + 1 ) -> ( ( F ` x ) e. RR <-> ( F ` ( k + 1 ) ) e. RR ) )
51 3 ralrimiva 
 |-  ( ph -> A. x e. ( M ... N ) ( F ` x ) e. RR )
52 51 adantr 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> A. x e. ( M ... N ) ( F ` x ) e. RR )
53 fzss1 
 |-  ( K e. ( ZZ>= ` M ) -> ( K ... N ) C_ ( M ... N ) )
54 23 53 syl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( K ... N ) C_ ( M ... N ) )
55 fzp1elp1 
 |-  ( k e. ( K ... ( N - 1 ) ) -> ( k + 1 ) e. ( K ... ( ( N - 1 ) + 1 ) ) )
56 55 adantl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( k + 1 ) e. ( K ... ( ( N - 1 ) + 1 ) ) )
57 56 47 eleqtrd 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( k + 1 ) e. ( K ... N ) )
58 54 57 sseldd 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( k + 1 ) e. ( M ... N ) )
59 50 52 58 rspcdva 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( F ` ( k + 1 ) ) e. RR )
60 49 59 addge01d 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( 0 <_ ( F ` ( k + 1 ) ) <-> ( seq M ( + , F ) ` k ) <_ ( ( seq M ( + , F ) ` k ) + ( F ` ( k + 1 ) ) ) ) )
61 44 60 mpbid 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( seq M ( + , F ) ` k ) <_ ( ( seq M ( + , F ) ` k ) + ( F ` ( k + 1 ) ) ) )
62 48 7 syldan 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> k e. ( ZZ>= ` M ) )
63 seqp1 
 |-  ( k e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( k + 1 ) ) = ( ( seq M ( + , F ) ` k ) + ( F ` ( k + 1 ) ) ) )
64 62 63 syl 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( seq M ( + , F ) ` ( k + 1 ) ) = ( ( seq M ( + , F ) ` k ) + ( F ` ( k + 1 ) ) ) )
65 61 64 breqtrrd 
 |-  ( ( ph /\ k e. ( K ... ( N - 1 ) ) ) -> ( seq M ( + , F ) ` k ) <_ ( seq M ( + , F ) ` ( k + 1 ) ) )
66 2 17 65 monoord 
 |-  ( ph -> ( seq M ( + , F ) ` K ) <_ ( seq M ( + , F ) ` N ) )