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 ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
sermono.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
sermono.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
sermono.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
Assertion sermono ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 sermono.1 ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 sermono.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
3 sermono.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
4 sermono.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
5 elfzuz ⊢ ( 𝑘 ∈ ( 𝐾 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) )
6 uztrn ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
7 5 1 6 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 elfzuz3 ⊢ ( 𝑘 ∈ ( 𝐾 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
10 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) → ( 𝑀 ... 𝑘 ) ⊆ ( 𝑀 ... 𝑁 ) )
11 9 10 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝑀 ... 𝑘 ) ⊆ ( 𝑀 ... 𝑁 ) )
12 11 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
13 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
14 12 13 syldan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
15 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
16 15 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
17 7 14 16 seqcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
18 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
19 18 breq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ 0 ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
20 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) 0 ≤ ( 𝐹 ‘ 𝑥 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ∀ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) 0 ≤ ( 𝐹 ‘ 𝑥 ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
24 eluzelz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℤ )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝐾 ∈ ℤ )
26 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
27 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ℤ )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
29 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
30 28 29 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℤ )
31 elfzelz ⊢ ( 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℤ )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℤ )
33 1zzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℤ )
34 fzaddel ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( ( 𝐾 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) )
35 25 30 32 33 34 syl22anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( ( 𝐾 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) )
36 22 35 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( ( 𝐾 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) )
37 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
38 ax-1cn ⊢ 1 ∈ ℂ
39 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
40 37 38 39 sylancl ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
41 28 40 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
42 41 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐾 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝐾 + 1 ) ... 𝑁 ) )
43 36 42 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) )
44 19 21 43 rspcdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 0 ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
45 fzelp1 ⊢ ( 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( 𝐾 ... ( ( 𝑁 − 1 ) + 1 ) ) )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝐾 ... ( ( 𝑁 − 1 ) + 1 ) ) )
47 41 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝐾 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐾 ... 𝑁 ) )
48 46 47 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝐾 ... 𝑁 ) )
49 48 17 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
50 18 eleq1d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) )
51 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ∀ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
53 fzss1 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
54 23 53 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝐾 ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
55 fzp1elp1 ⊢ ( 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) → ( 𝑘 + 1 ) ∈ ( 𝐾 ... ( ( 𝑁 − 1 ) + 1 ) ) )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( 𝐾 ... ( ( 𝑁 − 1 ) + 1 ) ) )
57 56 47 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( 𝐾 ... 𝑁 ) )
58 54 57 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
59 50 52 58 rspcdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
60 49 59 addge01d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( 0 ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) + ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
61 44 60 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) + ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
62 48 7 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
63 seqp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) + ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
64 62 63 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) + ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
65 61 64 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... ( 𝑁 − 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 + 1 ) ) )
66 2 17 65 monoord ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )