Metamath Proof Explorer

Theorem esumpmono

Description: The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017)

Ref Expression
Hypotheses esumpmono.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
esumpmono.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
esumpmono.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
Assertion esumpmono ( 𝜑 → Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ≤ Σ* 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 )

Proof

Step Hyp Ref Expression
1 esumpmono.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 esumpmono.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 esumpmono.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
4 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
5 ovexd ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ V )
6 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 𝑘 ∈ ℕ )
7 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
8 7 3 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
9 6 8 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
10 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∈ ( 0 [,] +∞ ) )
11 nfcv ⊢ Ⅎ 𝑘 ( 1 ... 𝑀 )
12 11 esumcl ⊢ ( ( ( 1 ... 𝑀 ) ∈ V ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∈ ( 0 [,] +∞ ) )
13 5 10 12 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∈ ( 0 [,] +∞ ) )
14 4 13 sselid ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∈ ℝ* )
15 14 xrleidd ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ≤ Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 )
16 ovexd ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) ∈ V )
17 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑀 ∈ ℕ )
18 peano2nn ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ℕ )
19 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
20 18 19 eleqtrdi ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
21 fzss1 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
22 17 20 21 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
24 22 23 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( 1 ... 𝑁 ) )
25 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
26 24 25 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℕ )
27 26 8 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
28 27 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ( 0 [,] +∞ ) )
29 nfcv ⊢ Ⅎ 𝑘 ( ( 𝑀 + 1 ) ... 𝑁 )
30 29 esumcl ⊢ ( ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∈ V ∧ ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ( 0 [,] +∞ ) )
31 16 28 30 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ( 0 [,] +∞ ) )
32 elxrge0 ⊢ ( Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ℝ* ∧ 0 ≤ Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) )
33 32 simprbi ⊢ ( Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ( 0 [,] +∞ ) → 0 ≤ Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 )
34 31 33 syl ⊢ ( 𝜑 → 0 ≤ Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 )
35 0xr ⊢ 0 ∈ ℝ*
36 35 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
37 4 31 sselid ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ℝ* )
38 xle2add ⊢ ( ( ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ) ∧ ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∈ ℝ* ∧ Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ∈ ℝ* ) ) → ( ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ≤ Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∧ 0 ≤ Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 0 ) ≤ ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) ) )
39 14 36 14 37 38 syl22anc ⊢ ( 𝜑 → ( ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ≤ Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∧ 0 ≤ Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 0 ) ≤ ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) ) )
40 15 34 39 mp2and ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 0 ) ≤ ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) )
41 xaddrid ⊢ ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ∈ ℝ* → ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 0 ) = Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 )
42 14 41 syl ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 0 ) = Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 )
43 42 eqcomd ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 = ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 0 ) )
44 1 19 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
45 eluzfz ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
46 44 2 45 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑁 ) )
47 fzsplit ⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
48 esumeq1 ⊢ ( ( 1 ... 𝑁 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 = Σ* 𝑘 ∈ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) 𝐴 )
49 46 47 48 3syl ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 = Σ* 𝑘 ∈ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) 𝐴 )
50 nfv ⊢ Ⅎ 𝑘 𝜑
51 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
52 51 ltp1d ⊢ ( 𝑀 ∈ ℕ → 𝑀 < ( 𝑀 + 1 ) )
53 fzdisj ⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
54 1 52 53 3syl ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
55 50 11 29 5 16 54 9 27 esumsplit ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) 𝐴 = ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) )
56 49 55 eqtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 = ( Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 +𝑒 Σ* 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) )
57 40 43 56 3brtr4d ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 1 ... 𝑀 ) 𝐴 ≤ Σ* 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 )