Metamath Proof Explorer

Theorem esumel

Description: The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017)

Ref Expression
Hypotheses esumel.1 ⊢ Ⅎ k φ
esumel.2 ⊢ Ⅎ _ k A
esumel.3 ⊢ φ → A ∈ V
esumel.4 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
Assertion esumel ⊢ φ → ∑ * k ∈ A B ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B

Proof

Step Hyp Ref Expression
1 esumel.1 ⊢ Ⅎ k φ
2 esumel.2 ⊢ Ⅎ _ k A
3 esumel.3 ⊢ φ → A ∈ V
4 esumel.4 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
5 4 ex ⊢ φ → k ∈ A → B ∈ 0 +∞
6 1 5 ralrimi ⊢ φ → ∀ k ∈ A B ∈ 0 +∞
7 2 esumcl ⊢ A ∈ V ∧ ∀ k ∈ A B ∈ 0 +∞ → ∑ * k ∈ A B ∈ 0 +∞
8 3 6 7 syl2anc ⊢ φ → ∑ * k ∈ A B ∈ 0 +∞
9 snidg ⊢ ∑ * k ∈ A B ∈ 0 +∞ → ∑ * k ∈ A B ∈ ∑ * k ∈ A B
10 8 9 syl ⊢ φ → ∑ * k ∈ A B ∈ ∑ * k ∈ A B
11 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
12 nfcv ⊢ Ⅎ _ k 0 +∞
13 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
14 1 2 12 4 13 fmptdf2 ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
15 inss1 ⊢ 𝒫 A ∩ Fin ⊆ 𝒫 A
16 simpr ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → x ∈ 𝒫 A ∩ Fin
17 15 16 sselid ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → x ∈ 𝒫 A
18 17 elpwid ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → x ⊆ A
19 nfcv ⊢ Ⅎ _ k x
20 2 19 resmptf ⊢ x ⊆ A → k ∈ A ⟼ B ↾ x = k ∈ x ⟼ B
21 18 20 syl ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → k ∈ A ⟼ B ↾ x = k ∈ x ⟼ B
22 21 eqcomd ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → k ∈ x ⟼ B = k ∈ A ⟼ B ↾ x
23 22 oveq2d ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ x B = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A ⟼ B ↾ x
24 1 2 3 4 23 esumval ⊢ φ → ∑ * k ∈ A B = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ k ∈ A ⟼ B ↾ x ℝ * <
25 11 3 14 24 xrge0tsmsd ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B = ∑ * k ∈ A B
26 10 25 eleqtrrd ⊢ φ → ∑ * k ∈ A B ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B