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 ⊢ Ⅎ _ k F
Assertion esumfsupre ⊢ F : ℕ ⟶ 0 +∞ → ∑ * k ∈ ℕ F ⁡ k = sup ran ⁡ seq 1 + F ℝ * <

Proof

Step Hyp Ref Expression
1 esumfsup.1 ⊢ Ⅎ _ k F
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 = sup ran ⁡ seq 1 + 𝑒 F ℝ * <
6 4 5 syl ⊢ F : ℕ ⟶ 0 +∞ → ∑ * k ∈ ℕ F ⁡ k = sup ran ⁡ seq 1 + 𝑒 F ℝ * <
7 1zzd ⊢ F : ℕ ⟶ 0 +∞ → 1 ∈ ℤ
8 elnnuz ⊢ x ∈ ℕ ↔ x ∈ ℤ ≥ 1
9 ffvelrn ⊢ 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 +∞ → seq 1 + F = seq 1 + 𝑒 F
22 21 rneqd ⊢ F : ℕ ⟶ 0 +∞ → ran ⁡ seq 1 + F = ran ⁡ seq 1 + 𝑒 F
23 22 supeq1d ⊢ F : ℕ ⟶ 0 +∞ → sup ran ⁡ seq 1 + F ℝ * < = sup ran ⁡ seq 1 + 𝑒 F ℝ * <
24 6 23 eqtr4d ⊢ F : ℕ ⟶ 0 +∞ → ∑ * k ∈ ℕ F ⁡ k = sup ran ⁡ seq 1 + F ℝ * <