Metamath Proof Explorer

Theorem sge0p1

Description: The addition of the next term in a finite sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0p1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
sge0p1.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
sge0p1.3 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
Assertion sge0p1 ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↦ 𝐴 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ) +𝑒 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sge0p1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 sge0p1.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
3 sge0p1.3 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
4 fzsuc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
5 1 4 syl ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
6 5 mpteq1d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↦ 𝐴 ) = ( 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ↦ 𝐴 ) )
7 6 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↦ 𝐴 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ↦ 𝐴 ) ) )
8 nfv ⊢ Ⅎ 𝑘 𝜑
9 ovex ⊢ ( 𝑀 ... 𝑁 ) ∈ V
10 9 a1i ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ V )
11 snex ⊢ { ( 𝑁 + 1 ) } ∈ V
12 11 a1i ⊢ ( 𝜑 → { ( 𝑁 + 1 ) } ∈ V )
13 fzp1disj ⊢ ( ( 𝑀 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅
14 13 a1i ⊢ ( 𝜑 → ( ( 𝑀 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅ )
15 0xr ⊢ 0 ∈ ℝ*
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 0 ∈ ℝ* )
17 pnfxr ⊢ +∞ ∈ ℝ*
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → +∞ ∈ ℝ* )
19 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
20 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝜑 )
21 fzelp1 ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
23 20 22 2 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
24 19 23 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℝ* )
25 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐴 )
26 16 18 23 25 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 0 ≤ 𝐴 )
27 iccleub ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 ∈ ( 0 [,] +∞ ) ) → 𝐴 ≤ +∞ )
28 16 18 23 27 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ≤ +∞ )
29 16 18 24 26 28 eliccxrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
30 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ( 𝑁 + 1 ) } ) → 𝜑 )
31 elsni ⊢ ( 𝑘 ∈ { ( 𝑁 + 1 ) } → 𝑘 = ( 𝑁 + 1 ) )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ( 𝑁 + 1 ) } ) → 𝑘 = ( 𝑁 + 1 ) )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑘 = ( 𝑁 + 1 ) ) → 𝑘 = ( 𝑁 + 1 ) )
34 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
35 eluzfz2 ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
36 1 34 35 3syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
38 33 37 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 = ( 𝑁 + 1 ) ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
39 30 32 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ( 𝑁 + 1 ) } ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
40 30 39 2 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ( 𝑁 + 1 ) } ) → 𝐴 ∈ ( 0 [,] +∞ ) )
41 8 10 12 14 29 40 sge0splitmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ↦ 𝐴 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ 𝐴 ) ) ) )
42 ovex ⊢ ( 𝑁 + 1 ) ∈ V
43 42 a1i ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ V )
44 id ⊢ ( 𝜑 → 𝜑 )
45 eleq1 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) )
46 45 anbi2d ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) ↔ ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) ) )
47 3 eleq1d ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ 𝐵 ∈ ( 0 [,] +∞ ) ) )
48 46 47 imbi12d ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ ( 0 [,] +∞ ) ) ) )
49 48 2 vtoclg ⊢ ( ( 𝑁 + 1 ) ∈ V → ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ ( 0 [,] +∞ ) ) )
50 42 49 ax-mp ⊢ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
51 44 36 50 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
52 43 51 3 sge0snmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ 𝐴 ) ) = 𝐵 )
53 52 oveq2d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ 𝐴 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ) +𝑒 𝐵 ) )
54 7 41 53 3eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↦ 𝐴 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ) +𝑒 𝐵 ) )