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 ⊢Ⅎ_kF
Assertion esumfsupre ⊢F:ℕ⟶0+∞→∑*k∈ℕF⁡k=supran⁡seq1+Fℝ*<

Proof

Step Hyp Ref Expression
1 esumfsup.1 ⊢Ⅎ_kF
2 icossicc ⊢0+∞⊆0+∞
3 fss ⊢F:ℕ⟶0+∞∧0+∞⊆0+∞→F:ℕ⟶0+∞
4 2 3 mpan2 ⊢F:ℕ⟶0+∞→F:ℕ⟶0+∞
5 1 esumfsup ⊢F:ℕ⟶0+∞→∑*k∈ℕF⁡k=supran⁡seq1+𝑒Fℝ*<
6 4 5 syl ⊢F:ℕ⟶0+∞→∑*k∈ℕF⁡k=supran⁡seq1+𝑒Fℝ*<
7 1zzd ⊢F:ℕ⟶0+∞→1∈ℤ
8 elnnuz ⊢x∈ℕ↔x∈ℤ≥1
9 ffvelcdm ⊢F:ℕ⟶0+∞∧x∈ℕ→F⁡x∈0+∞
10 8 9 sylan2br ⊢F:ℕ⟶0+∞∧x∈ℤ≥1→F⁡x∈0+∞
11 ge0addcl ⊢x∈0+∞∧y∈0+∞→x+y∈0+∞
12 11 adantl ⊢F:ℕ⟶0+∞∧x∈0+∞∧y∈0+∞→x+y∈0+∞
13 rge0ssre ⊢0+∞⊆ℝ
14 simprl ⊢F:ℕ⟶0+∞∧x∈0+∞∧y∈0+∞→x∈0+∞
15 13 14 sselid ⊢F:ℕ⟶0+∞∧x∈0+∞∧y∈0+∞→x∈ℝ
16 simprr ⊢F:ℕ⟶0+∞∧x∈0+∞∧y∈0+∞→y∈0+∞
17 13 16 sselid ⊢F:ℕ⟶0+∞∧x∈0+∞∧y∈0+∞→y∈ℝ
18 rexadd ⊢x∈ℝ∧y∈ℝ→x+𝑒y=x+y
19 18 eqcomd ⊢x∈ℝ∧y∈ℝ→x+y=x+𝑒y
20 15 17 19 syl2anc ⊢F:ℕ⟶0+∞∧x∈0+∞∧y∈0+∞→x+y=x+𝑒y
21 7 10 12 20 seqfeq3 ⊢F:ℕ⟶0+∞→seq1+F=seq1+𝑒F
22 21 rneqd ⊢F:ℕ⟶0+∞→ran⁡seq1+F=ran⁡seq1+𝑒F
23 22 supeq1d ⊢F:ℕ⟶0+∞→supran⁡seq1+Fℝ*<=supran⁡seq1+𝑒Fℝ*<
24 6 23 eqtr4d ⊢F:ℕ⟶0+∞→∑*k∈ℕF⁡k=supran⁡seq1+Fℝ*<