Metamath Proof Explorer

Theorem esumfsupre

Description: Formulating an extended sum over integers using the recursive sequence builder. This version is limited to real-valued functions. (Contributed by Thierry Arnoux, 19-Oct-2017)

Ref Expression
Hypothesis esumfsup.1 ⊢ Ⅎ 𝑘 𝐹
Assertion esumfsupre ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = sup ( ran seq 1 ( + , 𝐹 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 esumfsup.1 ⊢ Ⅎ 𝑘 𝐹
2 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
3 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
4 2 3 mpan2 ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
5 1 esumfsup ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = sup ( ran seq 1 ( +𝑒 , 𝐹 ) , ℝ* , < ) )
6 4 5 syl ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = sup ( ran seq 1 ( +𝑒 , 𝐹 ) , ℝ* , < ) )
7 1zzd ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → 1 ∈ ℤ )
8 elnnuz ⊢ ( 𝑥 ∈ ℕ ↔ 𝑥 ∈ ( ℤ≥ ‘ 1 ) )
9 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑥 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
10 8 9 sylan2br ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 1 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
11 ge0addcl ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
12 11 adantl ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
13 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
14 simprl ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 𝑥 ∈ ( 0 [,) +∞ ) )
15 13 14 sselid ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 𝑥 ∈ ℝ )
16 simprr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 𝑦 ∈ ( 0 [,) +∞ ) )
17 13 16 sselid ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 𝑦 ∈ ℝ )
18 rexadd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 +𝑒 𝑦 ) = ( 𝑥 + 𝑦 ) )
19 18 eqcomd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) = ( 𝑥 +𝑒 𝑦 ) )
20 15 17 19 syl2anc ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 +𝑒 𝑦 ) )
21 7 10 12 20 seqfeq3 ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → seq 1 ( + , 𝐹 ) = seq 1 ( +𝑒 , 𝐹 ) )
22 21 rneqd ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → ran seq 1 ( + , 𝐹 ) = ran seq 1 ( +𝑒 , 𝐹 ) )
23 22 supeq1d ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → sup ( ran seq 1 ( + , 𝐹 ) , ℝ* , < ) = sup ( ran seq 1 ( +𝑒 , 𝐹 ) , ℝ* , < ) )
24 6 23 eqtr4d ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = sup ( ran seq 1 ( + , 𝐹 ) , ℝ* , < ) )